Согласование спецификаций автоматов, представленных в языке L
Рассмотрены два метода согласования спецификаций взаимодействующих автоматов. Спецификации представлены множествами дизъюнктов в языке L. Оба метода основаны на методе согласования автоматов, использующем их параллельную композицию. Приведены два способа определения семантики языка L, принятые в опи...
Збережено в:
| Дата: | 2016 |
|---|---|
| Автор: | |
| Формат: | Стаття |
| Мова: | Russian |
| Опубліковано: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2016
|
| Назва видання: | Кибернетика и системный анализ |
| Теми: | |
| Онлайн доступ: | https://nasplib.isofts.kiev.ua/handle/123456789/133677 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Цитувати: | Согласование спецификаций автоматов, представленных в языке L / А.Н. Чеботарев // Кибернетика и системный анализ. — 2016. — Т. 52, № 3. — С. 3-15. — Бібліогр.: 6 назв. — рос. |
Репозитарії
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
nasplib_isofts_kiev_ua-123456789-133677 |
|---|---|
| record_format |
dspace |
| spelling |
nasplib_isofts_kiev_ua-123456789-1336772025-02-09T22:25:37Z Согласование спецификаций автоматов, представленных в языке L Узгодження специфікацій автоматів, що подані мовою L Harmonization of automata specifications represented in the language L Чеботарев, А.Н. Кибернетика Рассмотрены два метода согласования спецификаций взаимодействующих автоматов. Спецификации представлены множествами дизъюнктов в языке L. Оба метода основаны на методе согласования автоматов, использующем их параллельную композицию. Приведены два способа определения семантики языка L, принятые в описанных методах согласования спецификаций. Розглянуто два методи узгодження специфікацій автоматів, що взаємодіють. Специфікації подані у вигляді множин диз’юнктів у мові L. Обидва методи базуються на методі узгодження автоматів, який використовує їхню паралельну композицію. Наведено два способи визначення семантики мови L, прийняті у розглянутих методах узгодження специфікацій. The author considers two methods for harmonization of automata specifications represented as sets of clauses in the language L. Both methods are based on the automata harmonization technique, which uses their parallel composition. Two ways to determine language L semantics that are used in the harmonization methods are described. 2016 Article Согласование спецификаций автоматов, представленных в языке L / А.Н. Чеботарев // Кибернетика и системный анализ. — 2016. — Т. 52, № 3. — С. 3-15. — Бібліогр.: 6 назв. — рос. 0023-1274 https://nasplib.isofts.kiev.ua/handle/123456789/133677 519.713.1 ru Кибернетика и системный анализ application/pdf Інститут кібернетики ім. В.М. Глушкова НАН України |
| institution |
Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| collection |
DSpace DC |
| language |
Russian |
| topic |
Кибернетика Кибернетика |
| spellingShingle |
Кибернетика Кибернетика Чеботарев, А.Н. Согласование спецификаций автоматов, представленных в языке L Кибернетика и системный анализ |
| description |
Рассмотрены два метода согласования спецификаций взаимодействующих автоматов. Спецификации представлены множествами дизъюнктов в языке L. Оба метода основаны на методе согласования автоматов, использующем их параллельную композицию. Приведены два способа определения семантики языка L, принятые в описанных методах согласования спецификаций. |
| format |
Article |
| author |
Чеботарев, А.Н. |
| author_facet |
Чеботарев, А.Н. |
| author_sort |
Чеботарев, А.Н. |
| title |
Согласование спецификаций автоматов, представленных в языке L |
| title_short |
Согласование спецификаций автоматов, представленных в языке L |
| title_full |
Согласование спецификаций автоматов, представленных в языке L |
| title_fullStr |
Согласование спецификаций автоматов, представленных в языке L |
| title_full_unstemmed |
Согласование спецификаций автоматов, представленных в языке L |
| title_sort |
согласование спецификаций автоматов, представленных в языке l |
| publisher |
Інститут кібернетики ім. В.М. Глушкова НАН України |
| publishDate |
2016 |
| topic_facet |
Кибернетика |
| url |
https://nasplib.isofts.kiev.ua/handle/123456789/133677 |
| citation_txt |
Согласование спецификаций автоматов, представленных в языке L / А.Н. Чеботарев // Кибернетика и системный анализ. — 2016. — Т. 52, № 3. — С. 3-15. — Бібліогр.: 6 назв. — рос. |
| series |
Кибернетика и системный анализ |
| work_keys_str_mv |
AT čebotarevan soglasovaniespecifikaciiavtomatovpredstavlennyhvâzykel AT čebotarevan uzgodžennâspecifíkacíiavtomatívŝopodanímovoûl AT čebotarevan harmonizationofautomataspecificationsrepresentedinthelanguagel |
| first_indexed |
2025-12-01T10:07:43Z |
| last_indexed |
2025-12-01T10:07:43Z |
| _version_ |
1850300081571364864 |
| fulltext |
À.Í. ×ÅÁÎÒÀÐÅÂ
ÓÄÊ 519.713.1 ÑÎÃËÀÑÎÂÀÍÈÅ ÑÏÅÖÈÔÈÊÀÖÈÉ ÀÂÒÎÌÀÒÎÂ,
ÏÐÅÄÑÒÀÂËÅÍÍÛÕ Â ßÇÛÊÅ L
Àííîòàöèÿ. Ðàññìîòðåíû äâà ìåòîäà ñîãëàñîâàíèÿ ñïåöèôèêàöèé âçàèìî-
äåéñòâóþùèõ àâòîìàòîâ. Ñïåöèôèêàöèè ïðåäñòàâëåíû ìíîæåñòâàìè äèçú-
þíêòîâ â ÿçûêå L. Îáà ìåòîäà îñíîâàíû íà ìåòîäå ñîãëàñîâàíèÿ àâòîìàòîâ,
èñïîëüçóþùåì èõ ïàðàëëåëüíóþ êîìïîçèöèþ. Ïðèâåäåíû äâà ñïîñîáà îïðå-
äåëåíèÿ ñåìàíòèêè ÿçûêà L, ïðèíÿòûå â îïèñàííûõ ìåòîäàõ ñîãëàñîâàíèÿ
ñïåöèôèêàöèé.
Êëþ÷åâûå ñëîâà: ñïåöèôèêàöèÿ àâòîìàòà, ÿçûê L, ñîãëàñîâàíèå ñïåöèôè-
êàöèé, êîìïîçèöèÿ ñïåöèôèêàöèé, êîððåêòíîñòü êîìïîçèöèè.
ÂÂÅÄÅÍÈÅ
Òåîðåòèêî-àâòîìàòíûé ïîäõîä, ò.å. ïîäõîä, èñïîëüçóþùèé àâòîìàòíûå ìîäå-
ëè, øèðîêî ïðèìåíÿåòñÿ ïðè ïðîåêòèðîâàíèè ðåàêòèâíûõ ñèñòåì. Îäíàêî èñ-
õîäíûå òðåáîâàíèÿ ê ôóíêöèîíèðîâàíèþ ñèñòåìû ãîðàçäî óäîáíåå çàäàâàòü
â âèäå óòâåðæäåíèé ëîãè÷åñêîãî ÿçûêà, õàðàêòåðèçóþùèõ íåîáõîäèìûå ñâîé-
ñòâà ïðîåêòèðóåìîé ñèñòåìû. Êëàññ ñâîéñòâ, êîòîðûå ìîæíî ôîðìóëèðîâàòü
â ëîãè÷åñêîì ÿçûêå, îïðåäåëÿåò åãî âûðàçèòåëüíîñòü. Ðàñøèðåíèå âûðàçèòåëü-
íûõ âîçìîæíîñòåé ëîãè÷åñêîãî ÿçûêà, êàê ïðàâèëî, ñîïðÿæåíî ñ óâåëè÷åíèåì
âû÷èñëèòåëüíîé ñëîæíîñòè èñïîëüçóþùèõ åãî àëãîðèòìîâ ïðîåêòèðîâàíèÿ.
Ïîýòîìó ïðèõîäèòñÿ èñêàòü êîìïðîìèññ ìåæäó âûðàçèòåëüíûìè âîçìîæíîñòÿ-
ìè ÿçûêà è ýôôåêòèâíîñòüþ ìåòîäîâ îáðàáîòêè ïðåäñòàâëåííîé â íåì èíôîð-
ìàöèè. Ñ öåëüþ óìåíüøåíèÿ ñëîæíîñòè òàêèõ ìåòîäîâ îãðàíè÷èâàþò âûðàçè-
òåëüíûå âîçìîæíîñòè ÿçûêà, êîòîðûé â äàëüíåéøåì áóäåì íàçûâàòü ÿçûêîì
èñõîäíîé ñïåöèôèêàöèè. Â ñòàòüå ïðåäïîëàãàåòñÿ, ÷òî äëÿ èñõîäíîé ñïåöèôè-
êàöèè èñïîëüçóåòñÿ ÿçûê L [1], âûðàçèòåëüíûå âîçìîæíîñòè êîòîðîãî îãðàíè-
÷åíû ñâîéñòâàìè áåçîïàñíîñòè (safety). Ýòè ñâîéñòâà ïðåäñòàâèìû X Y/ -àâòî-
ìàòîì (X Y/ -òðàíñäüþñåðîì) — àâòîìàòíîé ìîäåëüþ, øèðîêî ðàñïðîñòðàíåí-
íîé â òåîðèè ïðîåêòèðîâàíèÿ ðåàêòèâíûõ ñèñòåì.
Ïîñêîëüêó ïðè ïåðåõîäå îò íåôîðìàëüíûõ òðåáîâàíèé ê ôîðìàëüíîé ñïåöè-
ôèêàöèè ñèñòåìû ìîãóò áûòü äîïóùåíû îøèáêè, íåîáõîäèìî èìåòü ñðåäñòâî
ïðîâåðêè (äîêàçàòåëüñòâà) íåêîòîðûõ ñóùåñòâåííûõ ñâîéñòâ ñïåöèôèêàöèè.
 ÷àñòíîñòè, íåïðîòèâîðå÷èâîñòü ñïåöèôèêàöèè, ñîñòîÿùåé èç áîëüøîãî êîëè-
÷åñòâà óòâåðæäåíèé ôîðìàëüíîãî ÿçûêà, äàëåêî íå î÷åâèäíà. Ïîýòîìó ïåðåä èñ-
ïîëüçîâàíèåì ñïåöèôèêàöèè äëÿ ñèíòåçà àâòîìàòíûõ ìîäåëåé æåëàòåëüíî ïðîâå-
ðèòü åå íà íåïðîòèâîðå÷èâîñòü, ÷òî ìîæåò îêàçàòüñÿ ïðîùå, ÷åì ñèíòåç ïóñòîãî
àâòîìàòà ïî ïðîòèâîðå÷èâîé ñïåöèôèêàöèè. Âçàèìîäåéñòâèå ïðîåêòèðóåìîé
ñèñòåìû ñ îïðåäåëåííîé ñðåäîé, êàê ïðàâèëî, íàëàãàåò íà ñèñòåìó äîïîëíèòåëü-
íûå îãðàíè÷åíèÿ, òàê ÷òî îòäåëüíî âçÿòàÿ íåïðîòèâîðå÷èâàÿ ñïåöèôèêàöèÿ ìî-
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2016, òîì 52, ¹ 3 3
� À.Í. ×åáîòàðåâ, 2016
æåò îêàçàòüñÿ ïðîòèâîðå÷èâîé ñ ó÷åòîì âçàèìîäåéñòâèÿ ñïåöèôèöèðóåìîé ñèñ-
òåìû ñî ñðåäîé. Ïðîâåðêà âîçìîæíîñòè òàêîé ñèòóàöèè îñóùåñòâëÿåòñÿ ìåòîäàìè
ñîãëàñîâàíèÿ ñïåöèôèêàöèè ñèñòåìû ñî ñïåöèôèêàöèåé ñðåäû. Ðàññìîòðåíèþ
ýòèõ ìåòîäîâ ïîñâÿùåíà íàñòîÿùàÿ ñòàòüÿ, êîòîðàÿ ïðîäîëæàåò òåìàòèêó ðàáî-
òû [2]. Ïðåäëîæåííûå çäåñü ìåòîäû áàçèðóþòñÿ íà ìåòîäàõ ñîãëàñîâàíèÿ àâòî-
ìàòíûõ ìîäåëåé, èçëîæåííûõ â [2]. Çàäà÷à ñîãëàñîâàíèÿ ñïåöèôèêàöèé ôîðìó-
ëèðóåòñÿ èñõîäÿ èç òîãî, ÷òî àâòîìàò, ñèíòåçèðîâàííûé ïî ñîãëàñîâàííîé ñî ñðå-
äîé ñïåöèôèêàöèè, äîëæåí áûòü ñîãëàñîâàí ñ àâòîìàòîì, ñèíòåçèðîâàííûì ïî
ñïåöèôèêàöèè ñðåäû. Îïèñàíèÿ èñïîëüçóåìûõ â ñòàòüå ïîíÿòèé X Y/ -àâòîìàòà,
�-àâòîìàòà, öèêëè÷åñêîãî àâòîìàòà è ïàðàëëåëüíîé êîìïîçèöèè àâòîìàòîâ, à òàê-
æå ññûëêè íà ðàáîòû çàðóáåæíûõ àâòîðîâ, îòíîñÿùèåñÿ ê ýòîé òåìàòèêå,
ñîäåðæàòñÿ â [2].
ßÇÛÊ L: ÑÈÍÒÀÊÑÈÑ È ÑÅÌÀÍÒÈÊÀ
Ïðåæäå ÷åì ïåðåéòè ê ðàññìîòðåíèþ ìåòîäîâ ñîãëàñîâàíèÿ ñïåöèôèêàöèé, äà-
äèì òî÷íîå îïèñàíèå ñèíòàêñèñà ñïåöèôèêàöèè â ÿçûêå L, åå ïðåäñòàâëåíèå
ïðè ðåøåíèè çàäà÷ ñîãëàñîâàíèÿ è àâòîìàòíóþ ñåìàíòèêó, îïðåäåëÿþùóþ
êëàññ ýêâèâàëåíòíûõ àâòîìàòîâ, çàäàâàåìûé ñïåöèôèêàöèåé.
ßçûê L [1] ïðåäñòàâëÿåò ñîáîé ôðàãìåíò ëîãèêè ïðåäèêàòîâ ïåðâîãî ïîðÿäêà
ñ îäíîìåñòíûìè ïðåäèêàòàìè è ôèêñèðîâàííîé îáëàñòüþ èíòåðïðåòàöèè, â êà-
÷åñòâå êîòîðîé âûñòóïàåò ìíîæåñòâî Z öåëûõ ÷èñåë (ìîìåíòîâ âðåìåíè). Ñïåöè-
ôèêàöèÿ â ÿçûêå L èìååò âèä ôîðìóëû � t f t( ). Çäåñü f t( ) — ôîðìóëà, ïîñòðîåí-
íàÿ ñ ïîìîùüþ ëîãè÷åñêèõ ñâÿçîê èç àòîìàðíûõ ôîðìóë (àòîìîâ) âèäà p t k( )� ,
ãäå p — îäíîìåñòíûé ïðåäèêàòíûé ñèìâîë, t — ïåðåìåííàÿ, ïðèíèìàþùàÿ çíà-
÷åíèÿ èç ìíîæåñòâà öåëûõ ÷èñåë, k — öåëîå ÷èñëî, íàçûâàåìîå ðàíãîì àòîìà.
Ðàçíîñòü ìåæäó ìàêñèìàëüíûì è ìèíèìàëüíûì çíà÷åíèÿìè ðàíãîâ àòîìîâ,
âñòðå÷àþùèõñÿ â ôîðìóëå, íàçûâàåòñÿ åå ãëóáèíîé. Êàê ïîêàçàíî â [1], ìîæíî
îãðàíè÷èòüñÿ ðàññìîòðåíèåì òîëüêî òàêèõ ôîðìóë f t( ), ó êîòîðûõ ìàêñèìàëü-
íûé ðàíã àòîìîâ ðàâåí 0. Ïðè îïðåäåëåíèè àâòîìàòíîé ñåìàíòèêè ÿçûêîâ ñïåöè-
ôèêàöèè ýòè ÿçûêè è àâòîìàòû ðàññìàòðèâàþòñÿ êàê ôîðìàëèçìû äëÿ çàäàíèÿ
ìíîæåñòâ ñâåðõñëîâ (áåñêîíå÷íûõ ñëîâ) â àëôàâèòå � �( ), ãäå � � {p pm1, , )� —
íàáîð ïðåäèêàòíûõ ñèìâîëîâ (ñèãíàòóðà) ñïåöèôèêàöèè. Ñèìâîëû àëôàâèòà
� �( ) ïðåäñòàâëÿþò ñîáîé äâîè÷íûå âåêòîðû äëèíû m.
Ïóñòü � — ñèãíàòóðà ôîðìóëû f t( ), à r — åå ãëóáèíà. Ïîñëåäîâàòåëüíîñòü
� � � �0 1, , ,� r âåêòîðîâ èç � �( ) íàçîâåì ñîñòîÿíèåì ãëóáèíû r, à ìíîæåñòâî
Q r( , )� âñåõ òàêèõ ïîñëåäîâàòåëüíîñòåé — ïðîñòðàíñòâîì ñîñòîÿíèé ãëóáèíû r
äëÿ ôîðìóëû f t( ). Ôîðìóëó f t( ) èíîãäà áóäåì ðàññìàòðèâàòü êàê ïðîïîçèöèî-
íàëüíóþ ôîðìóëó, ïîñòðîåííóþ èç àòîìîâ p t p t p tm1 1 1( ), , ( ), ( ),� �
� � �, ( ), , ( ), , ( )p t p t r p t rm m
1 1 . Åñëè êîìïîíåíòû âåêòîðà � i â ñîñòîÿíèè
q r� � � � �0 1, , ,� ðàññìàòðèâàòü êàê èñòèííîñòíûå çíà÷åíèÿ ñîîòâåòñòâóþùèõ
àòîìîâ ðàíãà i r
ïðè îïðåäåëåííîì óïîðÿäî÷åíèè ìíîæåñòâà �, òî ìîæíî ãîâî-
ðèòü î çíà÷åíèè ôîðìóëû f t( ) íà ñîñòîÿíèè q. Òàêèì îáðàçîì, áóäåì ñ÷èòàòü,
÷òî âñÿêàÿ ïðîïîçèöèîíàëüíàÿ ôîðìóëà ñ ýòèìè ïðîïîçèöèîíàëüíûìè ïåðåìåí-
íûìè çàäàåò ïîäìíîæåñòâî ñîñòîÿíèé ïðîñòðàíñòâà Q r( , )� , à èìåííî òå ñîñòîÿ-
íèÿ, íà êîòîðûõ îíà èñòèííà. Ïîëîæèì, ÷òî ôîðìóëà f t( ) èñòèííà íà ìíîæåñòâå
ñîñòîÿíèé Q Q r1 � ( , )� , åñëè îíà èñòèííà õîòÿ áû íà îäíîì èç ýòèõ ñîñòîÿíèé,
è ëîæíà íà ìíîæåñòâå Q1, åñëè îíà ëîæíà íà âñåõ ñîñòîÿíèÿõ èç Q1.
Íà ìíîæåñòâå Q r( , )� îïðåäåëèì îòíîøåíèå N íåïîñðåäñòâåííîãî ñëåäîâà-
íèÿ òàê, ÷òî çà êàæäûì ñîñòîÿíèåì q r� � � � �0 1, , ,� íåïîñðåäñòâåííî ñëåäóþò
2| |� ñîñòîÿíèé âèäà � � � �1, , ,� r , ãäå � �� �( ). Ìíîæåñòâî âñåõ ñîñòîÿíèé, êîòî-
4 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2016, òîì 52, ¹ 3
ðûå íåïîñðåäñòâåííî ñëåäóþò çà q, íàçûâàåòñÿ îáëàñòüþ ïåðåõîäîâ äëÿ ñîñòîÿ-
íèÿ q è îáîçíà÷àåòñÿ N q( ). Àíàëîãè÷íî îïðåäåëÿåòñÿ îòíîøåíèå P íåïîñðåä-
ñòâåííîãî ïðåäøåñòâîâàíèÿ òàê, ÷òî êàæäîìó ñîñòîÿíèþ q r� � � � �0 1, , ,� íå-
ïîñðåäñòâåííî ïðåäøåñòâóþò 2| |� ñîñòîÿíèé âèäà �
� � �, , ,1 1� r , ãäå � �� �( ).
Ïðè èñïîëüçîâàíèè ÿçûêà L äëÿ ñïåöèôèêàöèè X Y/ -àâòîìàòîâ ïðåäèêàòíûå
ñèìâîëû ñòàâÿòñÿ â ñîîòâåòñòâèå âõîäíûì è âûõîäíûì äâîè÷íûì êàíàëàì àâòîìà-
òà, à ìíîæåñòâî ïðåäèêàòíûõ ñèìâîëîâ � ðàçáèâàåòñÿ íà äâà êëàññà: âõîäíûå è âû-
õîäíûå, êîòîðûå îáîçíà÷èì ñîîòâåòñòâåííîU è W. Âõîäíîé àëôàâèò ñïåöèôèöèðó-
åìîãî �-àâòîìàòà ðàâåí � �( ), à âõîäíîé è âûõîäíîé àëôàâèòû ñîîòâåòñòâóþùåãî
X Y/ -àâòîìàòà èìåþò âèä X U� �( ) è Y W� �( ). Òàêèì îáðàçîì, âñÿêèé âåêòîð
� �� �( ) ìîæíî ðàññìàòðèâàòü êàê ïàðó
�x y, , ãäå x X� , y Y� . Ïîýòîìó íàðÿäó
ñ îáîçíà÷åíèåì � � � �0 1, , ,� r äëÿ ñîñòîÿíèÿ ãëóáèíû r áóäåì èñïîëüçîâàòü
îáîçíà÷åíèå �
�
� x y x yr r0 0, , , ,� . Äëÿ òàêîãî ïðåäñòàâëåíèÿ ñîñòîÿíèÿ
q Q r� ( , )� îïðåäåëèì åùå îäíó îáëàñòü ïðîñòðàíñòâà ñîñòîÿíèé, ñâÿçàííóþ ñ ñî-
ñòîÿíèåì q. Âî ìíîæåñòâå N q x y x yr r( ) , , , , ,� �
�
�{ 1 1 �
� � �x y x X y Y, | , }
âûäåëèì ïîäìíîæåñòâî ñîñòîÿíèé, çàôèêñèðîâàâ x ðàâíûì �x . Íàçîâåì ýòî ïîä-
ìíîæåñòâî îáëàñòüþ ïåðåõîäà èç ñîñòîÿíèÿ q ïîä äåéñòâèåì ñèìâîëà �x è îáî-
çíà÷èì N q x( , )� .
Èìååòñÿ íåñêîëüêî ñïîñîáîâ îïðåäåëåíèÿ àâòîìàòíîé ñåìàíòèêè ñïåöèôè-
êàöèè â ÿçûêå L. Ðàññìîòðèì äâà èç íèõ, èñïîëüçóåìûå â ñòàòüå äëÿ óñòàíîâëå-
íèÿ ñîîòâåòñòâèÿ ìåæäó ñâîéñòâàìè ñïåöèôèêàöèé è ñïåöèôèöèðóåìûõ èìè àâ-
òîìàòîâ. Ýòè ñïîñîáû îñíîâàíû íà ïîíÿòèè ïðîñòðàíñòâà ñîñòîÿíèé äëÿ ôîðìó-
ëû f t( ) â ñïåöèôèêàöèè F tf t� � ( ) è ðàçëè÷àþòñÿ äëèíîé ñëîâà, èñïîëüçóåìîãî
â êà÷åñòâå ñîñòîÿíèÿ ñïåöèôèöèðóåìîãî àâòîìàòà. Ïðè ïåðâîì ñïîñîáå ñîñòîÿ-
íèÿ àâòîìàòà îòîæäåñòâëÿþòñÿ ñ ñîñòîÿíèÿìè èç Q r( , )� , ò.å. ñî ñëîâàìè äëèíû
r �1 â àëôàâèòå � �( ). Ñíà÷àëà îïðåäåëÿåòñÿ �-àâòîìàò A f tr�
� �
1 ( ( )) ( ),� �
Q r r� �
1 1, � , ãäå ìíîæåñòâî ñîñòîÿíèé Q r�1 — âñå òå ñîñòîÿíèÿ èç Q r( , )� , íà êî-
òîðûõ f t( ) èñòèííà. Ôóíêöèÿ ïåðåõîäîâ �r�1 îïðåäåëÿåòñÿ ñëåäóþùèì îáðàçîì.
Ïóñòü ñîñòîÿíèå q Q r
�
�1 èìååò âèä � � � �0 1, , ,� r è � �� �( ), òîãäà çíà÷åíèå
� � � � �r
rq�
� �
1
1( , ) , , ,� , åñëè � � � �1, , ,� r ïðèíàäëåæèò Q r�1, è íå îïðåäåëå-
íî â ïðîòèâíîì ñëó÷àå. Àâòîìàò A Fr�1 ( ), îïðåäåëÿþùèé ñåìàíòèêó ñïåöèôèêà-
öèè F tf t� � ( ), — ìàêñèìàëüíûé öèêëè÷åñêèé ïîäàâòîìàò àâòîìàòà A f tr�1 ( ( )),
íàçûâàåìûé òàêæå ÿäðîì ýòîãî àâòîìàòà.
Ïðè âòîðîì ñïîñîáå îïðåäåëåíèÿ ñåìàíòèêè ñîñòîÿíèÿ àâòîìàòà îòîæäå-
ñòâëÿþòñÿ ñî ñëîâàìè äëèíû r â àëôàâèòå � �( ). Ñíà÷àëà ðàññìàòðèâàåòñÿ �-àâòî-
ìàò A f t Qr r r( ( )) ( ), ,� � � � � , ãäå ñîñòîÿíèÿ èç Q r ñîîòâåòñòâóþò îáëàñòÿì ïåðå-
õîäîâ äëÿ ñîñòîÿíèé ïðîñòðàíñòâà Q r( , )� , íà êîòîðûõ ôîðìóëà f t( ) èñòèííà.
Ïóñòü îáëàñòü ïåðåõîäîâ çàäàåòñÿ ôîðìóëîé S t( )
1 (êîíñòèòóýíòîé åäèíèöû îò
âñåõ àòîìîâ, ðàíã êîòîðûõ ìåíüøå íóëÿ), òîãäà ñîîòâåòñòâóþùåå åé ñîñòîÿíèå
q r� � � �1, ,� îïðåäåëÿåò íàáîð çíà÷åíèé àòîìîâ p t p tm1 1 1( ), , ( ),
� �
..., ( ), , ( )p t r p t rm1
� , íà êîòîðîì èñòèííà ýòà ôîðìóëà.
Ïóñòü ñîñòîÿíèå q r� � � �1, ,� ïðèíàäëåæèò Q r è � �� �( ). Òîãäà çíà÷åíèå
� �r q( , ) îïðåäåëåíî è ðàâíî � � � �2 , , ,� r , åñëè � �
�� � �1
1, , ,� r
rQ , â ïðîòèâ-
íîì ñëó÷àå çíà÷åíèå � �r q( , ) íå îïðåäåëåíî. Àâòîìàò A Fr ( ), îïðåäåëÿþùèé ñå-
ìàíòèêó ñïåöèôèêàöèè F tf t� � ( ), — ìàêñèìàëüíûé öèêëè÷åñêèé ïîäàâòîìàò
(ÿäðî) àâòîìàòà A f tr ( ( )).
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2016, òîì 52, ¹ 3 5
Ïîêàæåì ýêâèâàëåíòíîñòü îïèñàííûõ ñïîñîáîâ îïðåäåëåíèÿ ñåìàíòèêè.
Äëÿ ýòîãî îïðåäåëèì îòîáðàæåíèå �: Q Qr r�
�
1 ñëåäóþùèì îáðàçîì:
� � � � � �( , , , ) , ,� � � 0 1 1� �r r .
Èç îïðåäåëåíèé îòîáðàæåíèÿ � è ôóíêöèè ïåðåõîäîâ �r ñëåäóåò, ÷òî åñëè
äëÿ � �
�� � �0 1
1, , ,� r
rQ çíà÷åíèå � � � � �r
r
�
�
1
0 1( , , , , )� îïðåäåëåíî, òî
� � � � � �r
r( ( , , , ), )� 0 1 � òàêæå îïðåäåëåíî è ðàâíî � � � �2 , , ,� r , ò.å.
� � � � � �( ( , , , , ))r
r
�
� �
1
0 1 � � � � � � �r
r( ( , , , ), )� 0 1 � . Òàêèì îáðàçîì, � — ãîìî-
ìîðôèçì ìíîæåñòâà ñîñòîÿíèé àâòîìàòà A f tr�1 ( ( )) âî ìíîæåñòâî ñîñòîÿíèé àâ-
òîìàòà A f tr ( ( )), ñîõðàíÿþùèé ôóíêöèþ ïåðåõîäîâ àâòîìàòîâ. Çàìåòèì, ÷òî ñî-
ñòîÿíèÿ èç Q r , íå ïðèíàäëåæàùèå � ( )Q r�1 , ò.å. íå èìåþùèå ïðîîáðàçà, íå ìîãóò
áûòü ñîñòîÿíèÿìè öèêëè÷åñêîãî àâòîìàòà A Fr ( ). Îòñþäà ñëåäóåò, ÷òî àâòîìàòû
A Fr�1 ( ) è A Fr ( ) ýêâèâàëåíòíû (ñòðîãî ýêâèâàëåíòíû).
ÏÐÅÄÑÒÀÂËÅÍÈÅ ÑÏÅÖÈÔÈÊÀÖÈÉ È ÏÐÎÖÅÄÓÐÀ ÐÅÇÎËÜÂÈÐÎÂÀÍÈß
Ðàññìàòðèâàåìûå íèæå ìåòîäû ñîãëàñîâàíèÿ ñïåöèôèêàöèé àâòîìàòîâ îñíîâà-
íû íà ïðåäñòàâëåíèè ñïåöèôèêàöèé â âèäå ìíîæåñòâà äèçúþíêòîâ. Äèçúþíê-
òîì â ÿçûêå L íàçûâàåòñÿ äèçúþíêöèÿ ëèòåð âèäà ~( )p t k
, ãäå ~ ,p p p� �{ },
k �N . Äèçúþíêò, íå ñîäåðæàùèé ëèòåð, íàçûâàåòñÿ ïóñòûì. Ìíîæåñòâî äèçú-
þíêòîâ C ðàññìàòðèâàåòñÿ êàê çàäàíèå ôîðìóëû �tf t( ), ãäå f t( ) — êîíúþíê-
öèÿ âñåõ äèçúþíêòîâ èç C. Äèçúþíêò íàçûâàåòñÿ íîðìàëèçîâàííûì âïðàâî,
åñëè ìàêñèìàëüíûé ðàíã åãî àòîìîâ ðàâåí íóëþ. Äèçúþíêò, ïîëó÷àþùèéñÿ èç
äèçúþíêòà c t( ) ïóòåì óâåëè÷åíèÿ ðàíãà âñåõ åãî àòîìîâ íà k �N , íàçîâåì
k-ñäâèãîì c t( ) âïðàâî è îáîçíà÷èì c t k( )� . Óìåíüøåíèå ðàíãà âñåõ àòîìîâ
â äèçúþíêòå íàçûâàåòñÿ ñäâèãîì åãî âëåâî. Çàìåíà íåíîðìàëèçîâàííîãî
äèçúþíêòà c t( ), ò.å. äèçúþíêòà, â êîòîðîì ìàêñèìàëüíûé ðàíã àòîìîâ ìåíüøå
íóëÿ, åãî ñäâèãîì âïðàâî, èìåþùèì ìàêñèìàëüíûé ðàíã àòîìîâ, ðàâíûé íóëþ,
íàçûâàåòñÿ íîðìàëèçàöèåé äèçúþíêòà.  äàëüíåéøåì â êà÷åñòâå ñïåöèôèêàöèé
àâòîìàòîâ ðàññìàòðèâàþòñÿ ìíîæåñòâà íîðìàëèçîâàííûõ âïðàâî äèçúþíêòîâ.
Ïðè çàäàíèè ôîðìóëû f t( ) â ñïåöèôèêàöèè F tf t� � ( ) ìíîæåñòâîì äèçúþíêòîâ
C àâòîìàò A f t( ( )), îïðåäåëÿåìûé ôîðìóëîé f t( ) â ïðîñòðàíñòâå ñîñòîÿíèé Q r( , )� ,
ãäå r — ãëóáèíà ôîðìóëû f t( ), îáîçíà÷èì A r C( , ). Äëÿ óòî÷íåíèÿ òèïà ñåìàíòèêè
â îáîçíà÷åíèÿõ àâòîìàòîâ èíîãäà áóäóò äîáàâëÿòüñÿ âåðõíèå èíäåêñû r �1 èëè r.
Ïóñòü c1 è c2 — íîðìàëèçîâàííûå âïðàâî äèçúþíêòû, p t( ) — àòîì íóëåâîãî
ðàíãà è c c p t1 1� � � ( ), à c c p t2 2� � � � ( ) . Äèçúþíêò c c c� � � �1 2 íàçûâàåòñÿ R-ðåçîëü-
âåíòîé äèçúþíêòîâ c1 è c2 ïî àòîìó p t( ). Îïåðàöèþ ïîëó÷åíèÿ R-ðåçîëüâåíòû
äâóõ äèçúþíêòîâ áóäåì íàçûâàòü ðåçîëüâèðîâàíèåì. R-âûâîäîì äèçúþíêòà c èç
ìíîæåñòâà äèçúþíêòîâ C íàçûâàåòñÿ òàêàÿ êîíå÷íàÿ ïîñëåäîâàòåëüíîñòü äèçú-
þíêòîâ c ck1, ,� , ÷òî c ck � è êàæäûé äèçúþíêò ci (i k�1, ,� ) ëèáî ïðèíàäëå-
æèò C, ëèáî ÿâëÿåòñÿ R-ðåçîëüâåíòîé äâóõ ïðåäøåñòâóþùèõ äèçúþíêòîâ, ëèáî
åñòü ðåçóëüòàò íîðìàëèçàöèè âïðàâî äèçúþíêòà ci
1.
Ñïðàâåäëèâî ñëåäóþùåå óòâåðæäåíèå. Ôîðìóëà �tf t( ), çàäàâàåìàÿ ìíî-
æåñòâîì C íîðìàëèçîâàííûõ âïðàâî äèçúþíêòîâ, ïðîòèâîðå÷èâà òîãäà è òîëüêî
òîãäà, êîãäà ñóùåñòâóåò R-âûâîä ïóñòîãî äèçúþíêòà èç C.
Äèçúþíêò c t1 ( ) ïîãëîùàåò äèçúþíêò c t2 ( ), åñëè ñóùåñòâóåò òàêîå k �Z, ÷òî
âñå ëèòåðû äèçúþíêòà c t k1 ( )� èìåþòñÿ â äèçúþíêòå c t2 ( ). Óäàëåíèå èç ìíîæåñòâà
äèçúþíêòîâ, ïðåäñòàâëÿþùåãî ôîðìóëó � tf t( ), äèçúþíêòîâ, ïîãëîùàåìûõ äðóãè-
ìè äèçúþíêòàìè ýòîãî ìíîæåñòâà, ïðèâîäèò ê ìíîæåñòâó äèçúþíêòîâ, çàäàþùèõ
ýêâèâàëåíòíóþ ôîðìóëó (ò.å. ôîðìóëó, èìåþùóþ òî æå ìíîæåñòâî ìîäåëåé).
6 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2016, òîì 52, ¹ 3
Ìíîæåñòâî C íîðìàëèçîâàííûõ âïðàâî äèçúþíêòîâ íàçûâàåòñÿ R-ïîëíûì,
åñëè äëÿ ëþáîé R-ðåçîëüâåíòû äèçúþíêòîâ c1 è c2 èç C â íåì ñîäåðæèòñÿ äèçú-
þíêò, ïîãëîùàþùèé ýòó ðåçîëüâåíòó. Äðóãèìè ñëîâàìè, ìíîæåñòâî C çàìêíóòî
îòíîñèòåëüíî ðåçîëüâèðîâàíèÿ. Ïðîöåäóðà ïîñòðîåíèÿ äëÿ çàäàííîãî ìíîæåñòâà
äèçúþíêòîâ C ýêâèâàëåíòíîãî åìó R-ïîëíîãî ìíîæåñòâà íàçûâàåòñÿ R-ïîïîëíå-
íèåì ìíîæåñòâà äèçúþíêòîâ C. Ýòî îäíà èç îñíîâíûõ ïðîöåäóð, èñïîëüçóåìûõ
ïðè ñîãëàñîâàíèè ñïåöèôèêàöèé àâòîìàòîâ.
Ðàññìîòðèì îäíî ñâîéñòâî R-ïîëíîãî ìíîæåñòâà äèçúþíêòîâ, êîòîðîå áóäåò
èñïîëüçîâàòüñÿ â äàëüíåéøåì. Ïóñòü f t( ) — ôîðìóëà, îïðåäåëÿåìàÿ ìíîæåñ-
òâîì äèçúþíêòîâ C. Îáîçíà÷èì P f t( ( )) ôîðìóëó, çàäàþùóþ ìíîæåñòâî âñåõ ñî-
ñòîÿíèé èç Q r( , )� , íåïîñðåäñòâåííî ïðåäøåñòâóþùèõ ñîñòîÿíèÿì, çàäàâàåìûì
ôîðìóëîé f t( ). Óäàëåíèå âñåõ òóïèêîâûõ ñîñòîÿíèé â àâòîìàòå A f tr�1 ( ( )) ñîîò-
âåòñòâóåò ïîñòðîåíèþ àâòîìàòà A f t P f tr�1 ( ( )& ( ( ))). Çàìåòèì, ÷òî â àâòîìàòå
A f t P f tr�1 ( ( )& ( ( ))) ìîãóò ïîÿâèòüñÿ íîâûå òóïèêîâûå ñîñòîÿíèÿ. Êàê ïîêàçàíî
â [5], ìíîæåñòâî äèçúþíêòîâ, çàäàþùåå ôîðìóëó f t P f t( )& ( ( )), ïîëó÷àåòñÿ ïó-
òåì çàìûêàíèÿ ìíîæåñòâà äèçúþíêòîâ C îòíîñèòåëüíî ðåçîëüâèðîâàíèÿ (ïî àòî-
ìàì íóëåâîãî ðàíãà) è äîáàâëåíèÿ äèçúþíêòîâ, ïîëó÷åííûõ â ðåçóëüòàòå íîðìà-
ëèçàöèè âñåõ èìåþùèõñÿ íåíîðìàëèçîâàííûõ äèçúþíêòîâ. Èòåðàòèâíîå âûïîë-
íåíèå ýòîé ïðîöåäóðû ïðèâîäèò ê ìíîæåñòâó äèçúþíêòîâ, çàäàþùåìó ôîðìóëó
f t* ( ) òàêóþ, ÷òî ôîðìóëà � tf t*( ) ýêâèâàëåíòíà ôîðìóëå � tf t( ) è àâòîìàò
A f tr�1 ( ( ))* íå ñîäåðæèò òóïèêîâûõ ñîñòîÿíèé.
R-ïîïîëíåíèå õàðàêòåðèçóåòñÿ òåì, ÷òî ïðè êàæäîé èòåðàöèè óäàëÿþòñÿ
(ïîãëîùàþòñÿ) äèçúþíêòû, íå ñîäåðæàùèå ëèòåð íóëåâîãî ðàíãà. Ïðè ýòîì íà íå-
êîòîðûõ ñîñòîÿíèÿõ îáëàñòè, çàäàâàåìîé îòðèöàíèåì óäàëåííîãî äèçúþíêòà (íà
êîòîðîé èñõîäíàÿ ôîðìóëà f t( ) ëîæíà), ïîëó÷åííàÿ ôîðìóëà ìîæåò ñòàòü èñòèí-
íîé. Ïóñòü c t( ) — äèçúþíêò, íå ñîäåðæàùèé ëèòåð íóëåâîãî ðàíãà, à c t k( )� — ñî-
îòâåòñòâóþùèé íîðìàëèçîâàííûé äèçúþíêò. Îòðèöàíèå ýòîãî äèçúþíêòà çàäàåò
ìíîæåñòâî ñîñòîÿíèé ïðîñòðàíñòâà ñîñòîÿíèé, èç êîòîðûõ äîñòèæèìà çà k øàãîâ
îáëàñòü, çàäàâàåìàÿ �c t( ). Ïîëó÷åííàÿ â ðåçóëüòàòå ïîãëîùåíèÿ äèçúþíêòà c t( )
ôîðìóëà ëîæíà íà ñîñòîÿíèÿõ èç � �c t k( ), è, ñëåäîâàòåëüíî, äîáàâëåííûå âñëåä-
ñòâèå ýòîãî ïîãëîùåíèÿ ñîñòîÿíèÿ â àâòîìàò A r C( , ) íå äîñòèæèìû èç ÿäðà ýòîãî
àâòîìàòà. Òàêèì îáðàçîì, ñïðàâåäëèâî ñëåäóþùåå ñâîéñòâî R-ïîïîëíåííîãî ìíî-
æåñòâà äèçúþíêòîâ.
Óòâåðæäåíèå 1. Ìíîæåñòâî ñîñòîÿíèé, çàäàâàåìîå R-ïîëíûì ìíîæåñòâîì
äèçúþíêòîâ â ñîîòâåòñòâóþùåì ïðîñòðàíñòâå ñîñòîÿíèé, ñîñòîèò èç ÿäðà (öèê-
ëè÷åñêîãî àâòîìàòà) è, âîçìîæíî, ñîñòîÿíèé, èç íåãî íå äîñòèæèìûõ.
ÑÎÃËÀÑÎÂÀÍÈÅ ÑÏÅÖÈÔÈÊÀÖÈÉ
Ïðè ðàññìîòðåíèè ñîãëàñîâàíèÿ àâòîìàòîâ íàèáîëåå óäîáíûì âèäîì èõ êîìïîçè-
öèè ÿâëÿåòñÿ ïàðàëëåëüíàÿ êîìïîçèöèÿ, êîòîðîé ñîîòâåòñòâóåò êîíúþíêöèÿ ñïå-
öèôèêàöèé, ò.å. îáúåäèíåíèå ìíîæåñòâ äèçúþíêòîâ. Íàïîìíèì îñíîâíóþ èäåþ
ñîãëàñîâàíèÿ àâòîìàòîâ, èñïîëüçóþùåãî ïàðàëëåëüíóþ êîìïîçèöèþ. Â ýòîì ñëó-
÷àå â êîìïîçèöèè âìåñòî àâòîìàòà B, ñ êîòîðûì ñîãëàñóåòñÿ àâòîìàò A, èñïîëü-
çóåòñÿ åãî ëåâûé ñäâèã ïî âõîäó
~
B [2]. Ñïåöèôèêàöèÿ àâòîìàòà
~
B ïîëó÷àåòñÿ èç
ñïåöèôèêàöèè àâòîìàòà B ïóòåì óìåíüøåíèÿ ðàíãîâ âñåõ âûõîäíûõ àòîìîâ, ò.å.
àòîìîâ, îáðàçîâàííûõ âûõîäíûìè (äëÿ àâòîìàòà A) ïðåäèêàòíûìè ñèìâîëàìè, íà
åäèíèöó. ×àñòî ñïåöèôèêàöèÿ àâòîìàòà B ñðàçó çàäàåòñÿ â òàêîì âèäå.
Äëÿ �-àâòîìàòà, ñîîòâåòñòâóþùåãî ïàðàëëåëüíîé öèêëè÷åñêîé êîìïîçèöèè
X Y/ -àâòîìàòà A è Y X/ -àâòîìàòà B, ðàññìàòðèâàåìûõ êàê �-àâòîìàòû, óñëîâèå
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2016, òîì 52, ¹ 3 7
ñîãëàñîâàííîñòè âûïîëíÿåòñÿ, åñëè â êàæäîì åãî ñîñòîÿíèè ( , )q s ïðîåêöèÿ íà X
ìíîæåñòâà óñëîâèé âñåõ ïåðåõîäîâ èç ýòîãî ñîñòîÿíèÿ ñîâïàäàåò ñ ïðîåêöèåé íà X
ìíîæåñòâà óñëîâèé âñåõ ïåðåõîäîâ â �-àâòîìàòå B èç ñîñòîÿíèÿ s. Ýòî óñëîâèå äëÿ ñî-
ñòîÿíèÿ ( , )q s íàçûâàåòñÿ óñëîâèåì êîððåêòíîñòè êîìïîçèöèè â ñîñòîÿíèè ( , )q s [2].
Îïèñàííûé â [2] ïðîöåññ ñîãëàñîâàíèÿ àâòîìàòà A ñ àâòîìàòîì B îñóùåñòâëÿ-
åòñÿ ñëåäóþùèì îáðàçîì. Ñòðîèòñÿ ïàðàëëåëüíàÿ öèêëè÷åñêàÿ êîìïîçèöèÿ �-àâòî-
ìàòîâ A è
~
B . Çàòåì äëÿ ñîñòîÿíèé ýòîé êîìïîçèöèè ïðîâåðÿåòñÿ óñëîâèå êîððåêò-
íîñòè. Âñå ñîñòîÿíèÿ êîìïîçèöèè, íå óäîâëåòâîðÿþùèå óñëîâèþ êîððåêòíîñòè
(íåêîððåêòíûå ñîñòîÿíèÿ), óäàëÿþòñÿ.  ïîëó÷åííîì àâòîìàòå ñíîâà âûäåëÿåòñÿ
ìàêñèìàëüíûé öèêëè÷åñêèé ïîäàâòîìàò, äëÿ ñîñòîÿíèé êîòîðîãî ïðîâåðÿåòñÿ
óñëîâèå êîððåêòíîñòè. Ýòîò ïðîöåññ ïðîäîëæàåòñÿ äî òåõ ïîð, ïîêà íå áóäåò ïîëó-
÷åí öèêëè÷åñêèé ïîäàâòîìàò, âñå ñîñòîÿíèÿ êîòîðîãî óäîâëåòâîðÿþò óñëîâèþ
êîððåêòíîñòè, ëèáî âñå ñîñòîÿíèÿ êîìïîçèöèè íå áóäóò óäàëåíû. Ïîñëåäíåå ñâè-
äåòåëüñòâóåò î íåâîçìîæíîñòè ñîãëàñîâàíèÿ àâòîìàòà A ñ àâòîìàòîì B.
Ðàññìîòðèì, êàê ýòîò ïðîöåññ ìîæåò áûòü ðåàëèçîâàí ïðè ñîãëàñîâàíèè ñïåöè-
ôèêàöèé �-àâòîìàòîâ A è
~
B , ïðåäñòàâëåííûõ ìíîæåñòâàìè äèçúþíêòîâ CA è C
B
~
ñ îäíèì è òåì æå ìíîæåñòâîì ïðåäèêàòíûõ ñèìâîëîâ �. Ïîëàãàÿ ìíîæåñòâî �
óïîðÿäî÷åííûì äëÿ îáåèõ ñïåöèôèêàöèé îäíèì è òåì æå ñïîñîáîì, àâòîìàòû
A r CA A( , ), A r C
B B
( , )~ ~ è ïàðàëëåëüíóþ öèêëè÷åñêóþ êîìïîçèöèþ àâòîìàòîâ A è
~
B áóäåì ðàññìàòðèâàòü â îäíîì è òîì æå ïðîñòðàíñòâå ñîñòîÿíèé Q r( , )� , ãäå
r r rA B
� max ( , )~ . Íåòðóäíî ïîêàçàòü, ÷òî åñëè ñîñòîÿíèå ( , )q s ïðèíàäëåæèò ïàðàë-
ëåëüíîé öèêëè÷åñêîé êîìïîçèöèè àâòîìàòîâ A è
~
B (ò.å. öèêëè÷åñêîìó àâòîìàòó),
òî ñîñòîÿíèÿì q, s è ( , )q s ñîîòâåòñòâóåò îäíî è òî æå ñîñòîÿíèå ðàññìàòðèâàåìî-
ãî ïðîñòðàíñòâà ñîñòîÿíèé. Èñòèííîñòü èëè ëîæíîñòü óñëîâèÿ êîððåêòíîñòè ñî-
ñòîÿíèÿ ( , )q s îïðåäåëÿåòñÿ ñâîéñòâàìè îáëàñòè ïåðåõîäîâ N q s(( , )) äëÿ ýòîãî ñî-
ñòîÿíèÿ. Òàê êàê ñîñòîÿíèå ( , )q s ïðèíàäëåæèò öèêëè÷åñêîìó àâòîìàòó, ôóíêöèè
f tA ( ) è f t
B
~ ( ), çàäàâàåìûå ñîîòâåòñòâåííî ìíîæåñòâàìè äèçúþíêòîâ CA è C
B
~,
èñòèííû íà îáëàñòè ïåðåõîäîâ N q s(( , )). Ñîñòîÿíèå ( , )q s íåêîððåêòíî òîãäà
è òîëüêî òîãäà, êîãäà N q s(( , )) ñîäåðæèò îáëàñòü ïåðåõîäà, ñîîòâåòñòâóþùóþ íå-
êîòîðîìó x X� , íà êîòîðîé ôóíêöèÿ, çàäàâàåìàÿ ìíîæåñòâîì äèçúþíêòîâ
C CA B
� ~, ëîæíà, à f t
B
~ ( ) èñòèííà. Îòñþäà ñëåäóåò, ÷òî ñîñòîÿíèå ( , )q s íåêîð-
ðåêòíî òîëüêî òîãäà, êîãäà ñîñòîÿíèå ( , )q s àâòîìàòà A r C CA B
( , )~� , ðàññìàòðèâà-
åìîãî êàê X Y/ -àâòîìàò, ÷àñòè÷íîå, ò.å. ïåðåõîä èç ( , )q s ïîä äåéñòâèåì x íå
îïðåäåëåí. Ïîýòîìó ïðîöåññ ñîãëàñîâàíèÿ ñïåöèôèêàöèé ìîæåò îñóùåñòâëÿòüñÿ
ñëåäóþùèì îáðàçîì. Âûïîëíÿåòñÿ ïðåîáðàçîâàíèå ìíîæåñòâà äèçúþíêòîâ
C CA B
� ~, ñîîòâåòñòâóþùåå âûäåëåíèþ ìàêñèìàëüíîãî öèêëè÷åñêîãî ïîäàâòîìà-
òà àâòîìàòà A r C C
A B
( , )~� , êîòîðûé ñîâïàäàåò ñ ïàðàëëåëüíîé öèêëè÷åñêîé êîì-
ïîçèöèåé àâòîìàòîâ A è
~
B . Çàòåì îïðåäåëÿþòñÿ ÷àñòè÷íûå ñîñòîÿíèÿ ýòîãî àâòî-
ìàòà, ðàññìàòðèâàåìîãî êàê X Y/ -àâòîìàò, ò.å. íàõîäÿòñÿ îáëàñòè ïåðåõîäà, íà
êîòîðûõ ôîðìóëà, çàäàâàåìàÿ ìíîæåñòâîì äèçúþíêòîâ C CA B
� ~, ëîæíà. Íà ýòèõ
îáëàñòÿõ ïåðåõîäà îïðåäåëÿåòñÿ èñòèííîñòíîå çíà÷åíèå ôîðìóëû f t
B
~ ( ). Åñëè
ïðè ýòîì îáíàðóæèâàþòñÿ íåêîððåêòíûå ñîñòîÿíèÿ, âûïîëíÿåòñÿ ïðåîáðàçîâà-
íèå ñïåöèôèêàöèè C CA B
� ~, ñîîòâåòñòâóþùåå èõ óäàëåíèþ. Â àâòîìàòå, çàäàâà-
åìîì ïîëó÷åííûì ìíîæåñòâîì äèçúþíêòîâ, ñíîâà âûäåëÿåòñÿ ìàêñèìàëüíûé
öèêëè÷åñêèé ïîäàâòîìàò è ò.ä. Çàìåòèì, ÷òî â îïèñàííîì ïðîöåññå ñîãëàñîâàíèÿ
äîñòàòî÷íî îãðàíè÷èòüñÿ âûäåëåíèåì ìàêñèìàëüíîãî êâàçèöèêëè÷åñêîãî ïîäàâ-
òîìàòà, ÷òî îñóùåñòâëÿåòñÿ ïðîöåäóðîé ïîïîëíåíèÿ ñîîòâåòñòâóþùåãî ìíîæåñò-
âà äèçúþíêòîâ. Êàê áóäåò ïîêàçàíî íèæå, ýòà æå ïðîöåäóðà èñïîëüçóåòñÿ äëÿ íà-
õîæäåíèÿ ÷àñòè÷íûõ ñîñòîÿíèé. Ïðè ýòîì ìîãóò àíàëèçèðîâàòüñÿ ÷àñòè÷íûå ñî-
8 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2016, òîì 52, ¹ 3
ñòîÿíèÿ, íå ïðèíàäëåæàùèå ÿäðó àâòîìàòà A r C CA B
( , )~� , ÷òî íå ñêàçûâàåòñÿ íà
ðåçóëüòàòå ðàáîòû àëãîðèòìà.
×ÀÑÒÈ×ÍÎÑÒÜ
Óñëîâèå óäàëåíèÿ ñîñòîÿíèé ñôîðìóëèðóåì â òåðìèíàõ ñâîéñòâ ìíîæåñòâ
äèçúþíêòîâ. Äëÿ ýòîãî ââåäåì ñëåäóþùèå ïîíÿòèÿ. Ïðè ðàçáèåíèè ìíîæåñòâà
ïðåäèêàòíûõ ñèìâîëîâ � íà âõîäíûå è âûõîäíûå íîðìàëèçîâàííûå âïðàâî
äèçúþíêòû, ñîäåðæàùèå âûõîäíûå ëèòåðû íóëåâîãî ðàíãà, íàçîâåì äèçúþí-
êòàìè ïåðâîãî ðîäà, à äèçúþíêòû, íå ñîäåðæàùèå âûõîäíûõ ëèòåð íóëåâîãî
ðàíãà, — äèçúþíêòàìè âòîðîãî ðîäà.
Ïóñòü � � { }p pm1, ,� . Îáîçíà÷èì S t k� ( )
ìíîæåñòâî âñåõ ýëåìåíòàðíûõ
êîíúþíêöèé âèäà ~ ( )& & ~ ( )p t k p t km1
�
, ãäå k �N, ~ ,p p pi i i� �{ }, pi ��
( , , )i m�1 � . Ñîñòîÿíèå q r� � � � �0 1, , ,� èç Q r( , )� çàäàåòñÿ ôîðìóëîé
f t s t r s tq r( ) ( )& & ( )�
0 � , ãäå s t r i S t r ii ( ) ( )
� �
�� è ïðèíèìàåò çíà÷åíèå 1
íà âåêòîðå � i (i r� �0, , ). Îáëàñòü ïåðåõîäîâ â ïðîñòðàíñòâå ñîñòîÿíèé Q r( , )�
çàäàåòñÿ êîíúþíêöèåé âèäà s t r s tr0 1 1( )& & ( )
�
, ãäå s t r ii ( )
� �
�
�S t r i� ( ).
Ïóñòü d t( )
1 — êîíúþíêöèÿ, çàäàþùàÿ îáëàñòü ïåðåõîäîâ, à d t0 ( ) — íå
ðàâíàÿ òîæäåñòâåííî íóëþ êîíúþíêöèÿ ëèòåð, îáðàçîâàííûõ àòîìàìè
p t p ti ik1
( ), , ( )� , k m� , ïðèíàäëåæàùèìè ìíîæåñòâó � 0 1( ) ( ), , ( )t p t p tm� { }� .
Ïóñòü f t( ) — ôîðìóëà ñèãíàòóðû �, çàäàâàåìàÿ ìíîæåñòâîì äèçúþíêòîâ
C c t c t c tn� { }1 2( ), ( ), , ( )� .
Óòâåðæäåíèå 2. Åëè f t( ) ëîæíà íà îáëàñòè, çàäàâàåìîé ôîðìóëîé
d t d t( )& ( )
1 0 , ò.å. d t d t f t( )& ( )& ( )
�1 00 , òî çàìûêàíèå C îòíîñèòåëüíî ðå-
çîëüâèðîâàíèÿ ïî àòîìàì íóëåâîãî ðàíãà èç � 0 1
( ) \ ( ), , ( )t p t p ti ik
{ }� ñîäåðæèò
äèçúþíêò c t( ), ëîæíûé íà ýòîé îáëàñòè.
Äîêàçàòåëüñòâî. Ïðåäñòàâèì êîíúþíêöèþ d t d t f t d t( )& ( )& ( ) ( )&
�
1 10
& ( )& ( )d t c t
i
n
i0
1
�
�
â âèäå d t d t c t c tg( )& ( )& ( )& & ( )* *
1 0 1 � , ãäå êàæäûé äèçúþíêò
c tj
* ( ), j g�1, ,� , ÿâëÿåòñÿ ÷àñòüþ íåêîòîðîãî c t Ci ( ) � , ñîñòîÿùåé èç âñåõ åãî ëè-
òåð, îáðàçîâàííûõ àòîìàìè èç ìíîæåñòâà � 0 1
( ) \ ( ), , ( )t p t p ti ik
{ }� . Ìíîæåñòâî
äèçúþíêòîâ C c t c tg
* * *( ), , ( )� { }1 � ñòðîèòñÿ ñëåäóþùèì îáðàçîì. Ñíà÷àëà èç C
óäàëÿþòñÿ âñå äèçúþíêòû, ñîäåðæàùèå ëèòåðû, èìåþùèåñÿ â d t d t( )& ( )
1 0 .
Âñÿêèé òàêîé äèçúþíêò c ti ( ) ìîæíî óäàëèòü èç C, ïîñêîëüêó d t d t( )& ( )&
1 0
& ( ) ( )& ( )c t d t d ti �
1 0 . Çàòåì â îñòàâøèõñÿ äèçúþíêòàõ óäàëÿþòñÿ âñå ëèòåðû,
îòðèöàíèÿ êîòîðûõ ñîäåðæàòñÿ â d t d t( )& ( )
1 0 .  ðåçóëüòàòå ïîëó÷àåòñÿ ìíîæåñò-
âî C *, äèçúþíêòû êîòîðîãî ñîäåðæàò òîëüêî ëèòåðû èç � 0 1
( ) \ ( ), , ( )t p t p ti ik
{ }� .
Ôîðìóëà d t d t c t c tg( )& ( )& ( )& ...& ( )* *
1 0 1 ïðîòèâîðå÷èâà (òîæäåñòâåííî
ðàâíà íóëþ) òîãäà è òîëüêî òîãäà, êîãäà ïðîòèâîðå÷èâà c t c tg1
* *( )& & ( )� , ÷òî,
â ñâîþ î÷åðåäü, âîçìîæíî òîãäà è òîëüêî òîãäà, êîãäà èç C * âûâîäèòñÿ ïóñòîé
äèçúþíêò [4]. Òàê êàê êàæäîìó äèçúþíêòó èç C *ñîîòâåòñòâóåò äèçúþíêò èç C,
÷àñòüþ êîòîðîãî îí ÿâëÿåòñÿ, òî âûâîäó ïóñòîãî äèçúþíêòà èç C * ñîîòâåòñòâóåò
âûâîä èç C äèçúþíêòà, íå ñîäåðæàùåãî àòîìîâ èç � 0 1
( ) \ ( ), , ( )t p t p ti ik
{ }� è âñå
ëèòåðû êîòîðîãî ÿâëÿþòñÿ îòðèöàíèÿìè ëèòåð, âõîäÿùèõ â êîíúþíêöèþ
d t d t( )& ( )
1 0 . Òàêîé äèçúþíêò ëîæåí íà îáëàñòè d t d t( )& ( )
1 0 è ïðèíàäëåæèò
çàìûêàíèþ C îòíîñèòåëüíî ðåçîëüâèðîâàíèÿ ïî àòîìàì íóëåâîãî ðàíãà èç
� 0 1
( ) \ ( ), , ( )t p t p ti ik
{ }� .
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2016, òîì 52, ¹ 3 9
Ñëåäñòâèå. Åñëè C çàìêíóòî îòíîñèòåëüíî ðåçîëüâèðîâàíèÿ ïî âûõîäíûì
àòîìàì íóëåâîãî ðàíãà, òî íåîáõîäèìûì óñëîâèåì ÷àñòè÷íîñòè àâòîìàòà A r C( , )
ÿâëÿåòñÿ íàëè÷èå â C äèçúþíêòîâ âòîðîãî ðîäà.
Äåéñòâèòåëüíî, ñîñòîÿíèå q ÷àñòè÷íî òîãäà è òîëüêî òîãäà, êîãäà äëÿ íåãî
ñóùåñòâóåò îáëàñòü ïåðåõîäà, íà êîòîðîé ôîðìóëà f t( ) ëîæíà. Ïóñòü d t0 ( ) —
ýëåìåíòàðíàÿ êîíúþíêöèÿ, çàäàþùàÿ òàêóþ îáëàñòü ïåðåõîäà. Î÷åâèäíî, ÷òî
d t0 ( ) íå ñîäåðæèò âûõîäíûõ ëèòåð íóëåâîãî ðàíãà, ñëåäîâàòåëüíî, è äèçúþíêò
c t C( ) � , òàêîé ÷òî d t c t0 0( )& ( ) � , òàêæå èõ íå ñîäåðæèò, ò.å. ÿâëÿåòñÿ äèçúþí-
êòîì âòîðîãî ðîäà. Óñëîâèå íå ÿâëÿåòñÿ äîñòàòî÷íûì, ïîñêîëüêó îáëàñòü ïåðåõî-
äà, íà êîòîðîé ëîæíà ôîðìóëà f t( ), ìîæåò íå áûòü îáëàñòüþ ïåðåõîäà äëÿ
ñîñòîÿíèÿ àâòîìàòà A r C( , ).
Çàìåòèì, ÷òî óñëîâèå ÷àñòè÷íîñòè ñîñòîÿíèé àâòîìàòà A f tr ( ( )) òî æå, ÷òî è
äëÿ àâòîìàòà A f tr�1 ( ( )) (íàëè÷èå îáëàñòè ïåðåõîäà, íà êîòîðîé f t( ) ëîæíà).
Îäíàêî åñëè äëÿ àâòîìàòà A f tr�1 ( ( )) ÷àñòè÷íîñòü îòíîñèòñÿ ê ñîñòîÿíèÿì, èç
êîòîðûõ èìååòñÿ ïåðåõîä â ñîîòâåòñòâóþùóþ îáëàñòü ïåðåõîäîâ, òî äëÿ àâòîìà-
òà A f tr ( ( )) ÷àñòè÷íîñòü îòíîñèòñÿ ê ñîñòîÿíèþ, ñîîòâåòñòâóþùåìó ýòîé
îáëàñòè ïåðåõîäîâ.
ÏÐÎÖÅÄÓÐÛ ÑÎÃËÀÑÎÂÀÍÈß
Äëÿ ñîãëàñîâàíèÿ àâòîìàòà A ñ àâòîìàòîì B ìîæíî íå âûäåëÿòü â àâòîìàòå
A r C CA B
( , )~� ìàêñèìàëüíûé öèêëè÷åñêèé ïîäàâòîìàò, à âûïîëíÿòü ïîñëåäî-
âàòåëüíîå óäàëåíèå èç íåãî íåêîððåêòíûõ ñîñòîÿíèé. Îäíàêî äëÿ ýòîãî íåîá-
õîäèìî, ÷òîáû äëÿ âñåõ ñîñòîÿíèé, äîñòèæèìûõ èç ÿäðà äàííîãî àâòîìàòà,
ôóíêöèÿ ïåðåõîäîâ áûëà îïðåäåëåíà. Êàê ñëåäóåò èç óòâåðæäåíèÿ 1, ýòîãî
ìîæíî äîñòè÷ü, âûïîëíèâ ïîïîëíåíèå ìíîæåñòâà äèçúþíêòîâ C CA B
� ~. Ïðî-
öåäóðà ñîãëàñîâàíèÿ âûãëÿäèò ñëåäóþùèì îáðàçîì. Ìíîæåñòâî C CA B
� ~
R-ïîïîëíÿåòñÿ. Îäíîâðåìåííî ñ ýòèì ôîðìèðóåòñÿ ìíîæåñòâî äèçúþíêòîâ �C
B
~
ïóòåì äîáàâëåíèÿ ê C
B
~ âñåõ âûâîäèìûõ èç C CA B
� ~ äèçúþíêòîâ, íå ñîäåð-
æàùèõ ëèòåð íóëåâîãî ðàíãà. Ïðèâåäåì íåêîòîðûå ïîÿñíåíèÿ, êàñàþùèåñÿ
ìíîæåñòâà �C
B
~. Â ïðîöåññå ñîãëàñîâàíèÿ âàæíî ïîâåäåíèå àâòîìàòà A r C
B
( , )~
òîëüêî â ñîñòîÿíèÿõ, ñîîòâåòñòâóþùèõ ÿäðó àâòîìàòà A r C CA B
( , )~� . Íàïîì-
íèì, ÷òî â ðàññìàòðèâàåìîì ïðîñòðàíñòâå ñîñòîÿíèé ýòî îäíè è òå æå ñîñòîÿ-
íèÿ. Èç òàêèõ ñîñòîÿíèé âîçìîæíû ïåðåõîäû òîëüêî â îáëàñòè ïåðåõîäîâ, ñîîò-
âåòñòâóþùèå r-ñîñòîÿíèÿì ÿäðà àâòîìàòà A r C Cr
A B
( , )~� . Òàêèì îáðàçîì, â C
B
~
ìîæíî äîáàâëÿòü ëþáîé äèçúþíêò, îòðèöàíèå êîòîðîãî çàäàåò îáëàñòü, íå ïå-
ðåñåêàþùóþñÿ ñ îáëàñòÿìè ïåðåõîäîâ äëÿ ( )r �1 -ñîñòîÿíèé ÿäðà àâòîìàòà
A r C CA B
( , )~� , õîòÿ ïðè ýòîì ñïåöèôèöèðóåìûé àâòîìàò A F
B
( )~ ìîæåò èçìå-
íèòüñÿ. Òàêîå äîáàâëåíèå ìîæåò óìåíüøèòü êîëè÷åñòâî ïîðîæäàåìûõ äèçúþí-
êòîâ ïðè àíàëèçå îáëàñòåé ïåðåõîäà, ñîîòâåòñòâóþùèõ âûâîäèìûì èç
C CA B
� ~ äèçúþíêòàì âòîðîãî ðîäà. Èñõîäÿ èç ýòèõ æå ñîîáðàæåíèé, â C
B
~
ìîæíî äîáàâëÿòü òàêèå ñäâèãè âëåâî ëþáîãî äèçúþíêòà, âûâîäèìîãî èç
C CA B
� ~, â êîòîðûõ ìèíèìàëüíûé ðàíã àòîìîâ íå ìåíüøå
r.
Îòðèöàíèå êàæäîãî ïîëó÷åííîãî ïðè ïîïîëíåíèè C CA B
� ~ äèçúþíêòà âòî-
ðîãî ðîäà c çàäàåò ìíîæåñòâî îáëàñòåé ïåðåõîäà, íà êîòîðûõ ôîðìóëà, îïðåäåëÿ-
åìàÿ ìíîæåñòâîì äèçúþíêòîâ C CA B
� ~, ëîæíà. Äëÿ âûÿñíåíèÿ, êàêèå èç íèõ ñî-
îòâåòñòâóþò íåêîððåêòíûì ñîñòîÿíèÿì, � c óìíîæàåòñÿ íà êîíúþíêöèþ äèçúþí-
êòîâ èç �C
B
~ . Çäåñü óìåñòíî èñïîëüçîâàòü òîò æå ïðèåì, ÷òî è ïðè ïîñòðîåíèè
ìíîæåñòâà C * â äîêàçàòåëüñòâå óòâåðæäåíèÿ 2. Ñíà÷àëà èç �C
B
~ óäàëÿþòñÿ äèçú-
10 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2016, òîì 52, ¹ 3
þíêòû, ñîäåðæàùèå ëèòåðó, âõîäÿùóþ â � c, â îñòàâøèõñÿ äèçúþíêòàõ óäàëÿþò-
ñÿ ëèòåðû, ÿâëÿþùèåñÿ îòðèöàíèÿìè ëèòåð èç � c, ïîñëå ÷åãî âûïîëíÿåòñÿ ïåðå-
ìíîæåíèå �c è îñòàâøèõñÿ äèçúþíêòîâ. Åñëè â êàêîì-ëèáî äèçúþíêòå áóäóò
óäàëåíû âñå ëèòåðû, òî âû÷èñëÿåìîå ïðîèçâåäåíèå ðàâíî òîæäåñòâåííî íóëþ.
Ïîëó÷åííîå ïðîèçâåäåíèå çàäàåò ìíîæåñòâî âñåõ òåõ ñîñòîÿíèé èç ðàññìàòðèâà-
åìûõ îáëàñòåé ïåðåõîäà, íà êîòîðûõ ôîðìóëà f t
B
~ ( ) èñòèííà. Òàêèì îáðàçîì
îïðåäåëÿþòñÿ îáëàñòè ïåðåõîäà äëÿ íåêîððåêòíûõ ñîñòîÿíèé. ×òîáû ïîëó÷èòü
ôîðìóëó, çàäàþùóþ ñîñòîÿíèÿ, äëÿ êîòîðûõ ýòè îáëàñòè ÿâëÿþòñÿ îáëàñòÿìè
ïåðåõîäà, íåîáõîäèìî â ïðîèçâîëüíîé ä.í.ô. ïîëó÷åííîãî ïðîèçâåäåíèÿ óäàëèòü
âñå ëèòåðû íóëåâîãî ðàíãà, à çàòåì ðàíãè âñåõ îñòàâøèõñÿ ëèòåð óâåëè÷èòü íà
åäèíèöó. Îáîçíà÷èì ýòó ôîðìóëó f tc ( ). Óäàëåíèþ èç àâòîìàòà A r C CA B
( , )~�
ñîñòîÿíèé, çàäàâàåìûõ ôîðìóëîé f tc ( ), ñîîòâåòñòâóåò äîáàâëåíèå ê C CA B
� ~
ìíîæåñòâà äèçúþíêòîâ, îïðåäåëÿåìîãî ïðîèçâîëüíîé ê.í.ô. ôîðìóëû � f tc ( ).
Åñëè íåêîòîðûå èç äîáàâëÿåìûõ äèçúþíêòîâ íå íîðìàëèçîâàíû âïðàâî, òî èõ
ñëåäóåò íîðìàëèçîâàòü.
Ïîñëå òîãî êàê îïèñàííàÿ ïðîöåäóðà óäàëåíèÿ íåêîððåêòíûõ ñîñòîÿíèé áó-
äåò âûïîëíåíà äëÿ âñåõ äèçúþíêòîâ âòîðîãî ðîäà, â ðåçóëüòàòå ÷åãî ê ìíîæåñòâó
C CA B
� ~, âîçìîæíî, áóäóò äîáàâëåíû íîâûå äèçúþíêòû, ïîëó÷åííîå ìíîæåñòâî
äèçúþíêòîâ R-ïîïîëíÿåòñÿ. Åñëè â ðåçóëüòàòå ïîïîëíåíèÿ ïîÿâÿòñÿ íîâûå äèçú-
þíêòû âòîðîãî ðîäà, òî ïðîöåññ ïîâòîðÿåòñÿ äî òåõ ïîð, ïîêà ïðè î÷åðåäíîì
R-ïîïîëíåíèè ëèáî áóäåò ïîëó÷åí ïóñòîé äèçúþíêò, ÷òî ñâèäåòåëüñòâóåò î íå-
ñîãëàñîâàííîñòè àâòîìàòà A ñ àâòîìàòîì B, ëèáî âñå âíîâü ïîëó÷åííûå äèçúþí-
êòû âòîðîãî ðîäà áóäóò ïîãëîùàòüñÿ ðàíåå èìåâøèìèñÿ äèçúþíêòàìè. Íà ýòîì
ïðîöåññ óäàëåíèÿ íåêîððåêòíûõ ñîñòîÿíèé, à ñëåäîâàòåëüíî, è ñîãëàñîâàíèÿ, çà-
êàí÷èâàåòñÿ. Ðåçóëüòàòîì ñîãëàñîâàíèÿ ÿâëÿåòñÿ X Y/ -àâòîìàò, ñïåöèôèöèðóå-
ìûé ïîëó÷åííûì ìíîæåñòâîì äèçúþíêòîâ.
Ïðèìåð 1. Ñïåöèôèêàöèÿ àâòîìàòà A çàäàíà ìíîæåñòâîì äèçúþíêòîâ CA
ñëåäóþùåãî âèäà:
#1 ( ( ) ( ))�
� �u t w t1 ,
#2 ( ( ) ( ))u t w t� � ,
3 ( ( ) ( ))u t u t
�1 ,
#4 ( ( ) ( ) ( ))�
� �
� �u t w t u t1 1 ,
ãäå u — âõîäíîé ïðåäèêàòíûé ñèìâîë, à w — âûõîäíîé. Ìíîæåñòâî äèçúþí-
êòîâ C
B
~, ñïåöèôèöèðóþùåå àâòîìàò
~
B , èìååò âèä
5 ( ( ) ( ) ( ))�
�
�u t w t u t1 1 ,
6 ( ( ) ( ) ( ))w t w t u t
�
�2 1 ,
7 ( ( ) ( ) ( ))w t u t u t
� �
�2 1 ,
#8 ( ( ) ( ) ( ) ( ))�
�
�
� �w t u t w t u t2 1 1 ,
#9 ( ( ) ( ) ( ) ( ))w t u t w t u t
�
� �
� �2 1 1 .
Ïðèâåäåì îïèñàíèå ïðîöåññà ïîïîëíåíèÿ ìíîæåñòâà C CA B
� ~.
Äèçúþíêò 9 ïîãëîùàåòñÿ äèçúþíêòîì 2. Ïîãëîùàåìûå äèçúþíêòû îòìå÷à-
þòñÿ ñèìâîëîì #. Äèçúþíêò 2, ðåçîëüâèðóÿñü ïî àòîìó u t( ) ñ äèçúþíêòàìè 4, 8,
äàåò ñîîòâåòñòâåííî äèçúþíêòû
#10 ( ( ) ( ) ( ))�
� �
� �u t w t w t1 1 , ïîãëîùàåòñÿ äèçúþíêòîì 1,
#11 ( ( ) ( ) ( ) ( ))�
�
�
� �w t u t w t w t2 1 1 .
Äèçúþíêò 3, ðåçîëüâèðóÿñü ñ 8, äàåò íåíîðìàëèçîâàííûé äèçúþíêò 12, êîòî-
ðûé íîðìàëèçóåòñÿ, ÷òî îáîçíà÷åíî ñèìâîëîì �� :
#12 ( ( ) ( ) ( )) ( ( ) ( ) ( ))�
�
�
�� �
� �w t u t w t w t u t w t2 1 1 1 ,
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2016, òîì 52, ¹ 3 11
Äèçúþíêò 12 ïîãëîùàåò äèçúþíêòû 8 è 11. Äèçúþíêò 4, ðåçîëüâèðóÿñü ñ 7,
äàåò äèçúþíêò 13, êîòîðûé íîðìàëèçóåòñÿ:
#13 ( ( ) ( ) ( )) ( ( ) ( ) ( ))w t u t w t w t u t w t
� �
� �
��
� � � �2 1 1 1 .
Äèçúþíêò 1, ðåçîëüâèðóÿñü ñ 12, äàåò
#14 ( ( ) ( ) ( ))�
� �
�u t w t u t1 1 .
Ðåçîëüâèðîâàíèå 2 è 12 äàåò äèçúþíêò #15 ( ( ) ( ))�
�w t u t1 , ïîãëîùàþùèé
äèçúþíêòû 12 è 14.
Äèçúþíêòû 2 è 13 äàþò äèçúþíêò #16 ( ( ) ( ))w t w t
� �1 , ïîãëîùàþùèé 13.
Äèçúþíêòû 4 è 15 äàþò #17 ( ( ) ( )) ( ( ) ( ))�
� �
�� � � �u t w t u t w t1 1 .
Äèçúþíêòû 2 è 17 äàþò äèçúþíêò 18 ( ( ))�w t , êîòîðûé ïîãëîùàåò äèçúþí-
êòû 1, 2, 4, 10, 15, 16 è 17. Íà ýòîì ïðîöåññ ïîïîëíåíèÿ çàêàí÷èâàåòñÿ.  ðåçóëü-
òàòå èìååì ñëåäóþùåå ïîïîëíåííîå ìíîæåñòâî äèçúþíêòîâ:
3 ( ( ) ( ))u t u t
�1 ,
5 ( ( ) ( ) ( ))�
�
�u t w t u t1 1 ,
6 ( ( ) ( ) ( ))w t w t u t
�
�2 1 ,
7 ( ( ) ( ) ( ))w t u t u t
� �
�2 1 ,
18 ( ( ))�w t .
Ýòî ìíîæåñòâî èìååò åäèíñòâåííûé äèçúþíêò âòîðîãî ðîäà ( ( ) ( ))u t u t
�1 ,
íå ïðèíàäëåæàùèé C
B
~.
 ïðîöåññå ïîïîëíåíèÿ ôîðìèðóåòñÿ ñëåäóþùåå ìíîæåñòâî �C
B
~ :
( ( ) ( ) ( ))�
�
�u t w t u t1 1 ,
( ( ) ( ) ( ))w t w t u t
�
�2 1 ,
( ( ) ( ) ( ))w t u t u t
� �
�2 1 ,
( ( ))�
w t 1 , ( ( ))�
w t 2 .
Óìíîæåíèå ôîðìóëû �
�u t u t( ) ( )1 , çàäàâàåìîé îòðèöàíèåì äèçúþíêòà 3, íà
êîíúþíêöèþ äèçúþíêòîâ èç ìíîæåñòâà �C
B
~ äàåò òîæäåñòâåííûé íóëü. Ïîýòîìó
ïðîöåññ ñîãëàñîâàíèÿ çàêàí÷èâàåòñÿ, è ïîïîëíåííîå ìíîæåñòâî äèçúþíêòîâ
C CA B
� ~ ìîæíî ðàññìàòðèâàòü êàê ñïåöèôèêàöèþ àâòîìàòà, ñîãëàñîâàííîãî
ñ àâòîìàòîì B.
Ðàññìîòðèì òåïåðü ðåàëèçàöèþ ýòîãî æå ìåòîäà ñîãëàñîâàíèÿ X Y/ -àâòîìà-
òà A ñ Y X/ -àâòîìàòîì B, íå îñóùåñòâëÿþùóþ àíàëèç ÷àñòè÷íîñòè ñîñòîÿíèé
X Y/ -àâòîìàòà A r C CA B
( , )~� . Ïðè ýòîì ðàññìàòðèâàþòñÿ àâòîìàòû
A r C Cr
A B
( , )~� è A r Cr
B
( , )~ . Òàê æå êàê è ðàíüøå, ÿäðî àâòîìàòà A r C CA B
( , )~�
íå âûäåëÿåòñÿ, à äëÿ èñêëþ÷åíèÿ äîñòèæèìûõ èç íåãî òóïèêîâûõ ( )r �1 -ñîñòîÿ-
íèé ìíîæåñòâî äèçúþíêòîâ C CA B
� ~ ïîïîëíÿåòñÿ. Áîëåå òîãî, ÷òîáû ñóùåñòâåííî
óìåíüøèòü êîëè÷åñòâî àíàëèçèðóåìûõ ñîñòîÿíèé àâòîìàòà A r C Cr
A B
( , )~� ,
â ïîïîëíåííîå ìíîæåñòâî äèçúþíêòîâ äîáàâëÿþòñÿ òàêèå ñäâèãè âëåâî èìåþ-
ùèõñÿ â íåì äèçúþíêòîâ, ÷òî ðàíã êàæäîãî àòîìà â ñäâèãå íå ìåíüøå ìèíèìàëü-
íîãî ðàíãà àòîìîâ â C CA B
� ~, îáðàçîâàííûõ òåì æå ïðåäèêàòíûì ñèìâîëîì. Ýòî
íå èçìåíÿåò ÿäðî ñïåöèôèöèðóåìîãî àâòîìàòà. Ñ òîé æå öåëüþ ôîðìèðóåòñÿ, êàê
îïèñàíî âûøå, ìíîæåñòâî äèçúþíêòîâ �C
B
~ . Êîíúþíêöèÿ âñåõ äèçúþíêòîâ ðàñ-
øèðåííîãî ìíîæåñòâà C CA B
� ~ ïðåîáðàçóåòñÿ â ä.í.ô. Â êàæäîé ýëåìåíòàðíîé
êîíúþíêöèè ýòîé ä.í.ô. ÷àñòü åå, îáðàçîâàííàÿ ëèòåðàìè, ðàíã êîòîðûõ ìåíüøå
íóëÿ, çàäàåò ìíîæåñòâî ñîñòîÿíèé àâòîìàòà A r C Cr
A B
( , )~� , à ÷àñòü, îáðàçîâàí-
íàÿ ëèòåðàìè íóëåâîãî ðàíãà, çàäàåò îäíî è òî æå ìíîæåñòâî óñëîâèé ïåðåõîäîâ
äëÿ âñåõ ýòèõ ñîñòîÿíèé. Ïóñòü l — îäíà èç òàêèõ êîíúþíêöèé. Óäàëèâ èç íåå
ëèòåðû íóëåâîãî ðàíãà è óìíîæèâ îñòàâøóþñÿ ÷àñòü íà êîíúþíêöèþ âñåõ äèçú-
þíêòîâ èç �C
B
~ , ïîëó÷èì îäíó èëè íåñêîëüêî êîíúþíêöèé, ÷àñòè êîòîðûõ, îáðà-
12 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2016, òîì 52, ¹ 3
çîâàííûå ëèòåðàìè ðàíãà íóëü, çàäàþò ìíîæåñòâà óñëîâèé ïåðåõîäîâ èç ñîîòâå-
òñòâóþùèõ ñîñòîÿíèé àâòîìàòà A r Cr
B
( , )~ . Ïðîåêöèÿ íà X ìíîæåñòâà óñëîâèé
ïåðåõîäîâ ïîëó÷àåòñÿ, åñëè â çàäàþùåé åãî êîíúþíêöèè óäàëèòü âñå ëèòåðû, îá-
ðàçîâàííûå âûõîäíûìè ïðåäèêàòíûìè ñèìâîëàìè. Ñðàâíèâàÿ ïðîåêöèè íà X
ïîëó÷åííûõ ìíîæåñòâ óñëîâèé ïåðåõîäîâ ñ ïðîåêöèåé íà X ìíîæåñòâà óñëîâèé
ïåðåõîäîâ, çàäàâàåìîãî êîíúþíêöèåé l, îïðåäåëÿåì íàëè÷èå ñðåäè ñîñòîÿíèé, çà-
äàâàåìûõ êîíúþíêöèåé l, íåêîððåêòíûõ ñîñòîÿíèé. Óäàëåíèå èõ îñóùåñòâëÿåòñÿ
óìíîæåíèåì ä.í.ô. ôîðìóëû, ñîîòâåòñòâóþùåé ðàñøèðåííîìó ìíîæåñòâó äèçú-
þíêòîâ C CA B
� ~, íà îòðèöàíèÿ êîíúþíêòîâ, çàäàþùèõ íåêîððåêòíûå ñîñòîÿ-
íèÿ. Îïèñàííûé ïðîöåññ èòåðàòèâíî âûïîëíÿåòñÿ äî òåõ ïîð, ïîêà íå ïåðåñòàíóò
ïîÿâëÿòüñÿ íåêîððåêòíûå ñîñòîÿíèÿ ëèáî âñå ñîñòîÿíèÿ ðàññìàòðèâàåìîãî
àâòîìàòà áóäóò óäàëåíû.
Ïðèìåð 2. Ðàññìîòðèì ñîãëàñîâàíèå òåõ æå àâòîìàòîâ, ÷òî è â ïðèìåðå 1.
Ïîïîëíåííîå ìíîæåñòâî äèçúþíêòîâ C CA B
� ~ èìååò âèä
3 ( ( ) ( ))u t u t
�1 ,
5 ( ( ) ( ) ( ))�
�
�u t w t u t1 1 ,
6 ( ( ) ( ) ( ))w t w t u t
�
�2 1 ,
7 ( ( ) ( ) ( ))w t u t u t
� �
�2 1 ,
18 ( ( ))�w t .
Äîïîëíèì åãî ñäâèãàìè âëåâî äèçúþíêòà 18: ( ( ))�
w t 1 è ( ( ))�
w t 2 . Ïðîèçâåäå-
íèå âñåõ ýòèõ äèçúþíêòîâ, ïðåäñòàâëåííîå â ä.í.ô., ðàâíî �
�
�w t w t u t w t( ) ( ) ( ) ( )2 1 .
Îíî çàäàåò äâà ýêâèâàëåíòíûõ r-ñîñòîÿíèÿ, ìíîæåñòâî óñëîâèé ïåðåõîäîâ èç êî-
òîðûõ îïðåäåëÿåòñÿ ôîðìóëîé u t w t( ) ( )� . Ìíîæåñòâî �C
B
~ âìåñòå ñ äîáàâëåííûìè
ñäâèãàìè äèçúþíêòîâ èìååò âèä
( ( ) ( ) ( ))�
�
�u t w t u t1 1 ,
( ( ) ( ) ( ))w t w t u t
�
�2 1 ,
( ( ) ( ) ( ))w t u t u t
� �
�2 1 ,
( ( ))�
w t 1 , ( ( ))�
w t 2 .
Óìíîæåíèå ôîðìóëû �
�
w t w t( ) ( )2 1 , çàäàþùåé ïîëó÷åííûå äâà r-ñîñòîÿ-
íèÿ, íà êîíúþíêöèþ äèçúþíêòîâ èç �C
B
~ äàåò �
�
w t w t u t( ) ( ) ( )2 1 . Ìíîæåñòâî
óñëîâèé ïåðåõîäîâ èç ðàññìàòðèâàåìûõ ñîñòîÿíèé â àâòîìàòå A r Cr
B
( , )~� îïðåäå-
ëÿåòñÿ ôîðìóëîé u t( ). Ëåãêî âèäåòü, ÷òî ïðîåêöèè íà âõîäíîé àëôàâèò
X u u� �{ }, ìíîæåñòâ óñëîâèé ïåðåõîäîâ èç ðàññìàòðèâàåìûõ ñîñòîÿíèé â àâòî-
ìàòàõ A r C Cr
A B
( , )~� è A r Cr
B
( , )~ ñîâïàäàþò è ðàâíû u t( ). Òàêèì îáðàçîì, ýòè ñî-
ñòîÿíèÿ êîððåêòíû. Îòñþäà ñëåäóåò, ÷òî àâòîìàò, ñïåöèôèöèðóåìûé ðàñøèðåííûì
ìíîæåñòâîì äèçúþíêòîâ C CA B
� ~, ñîãëàñîâàí ñ àâòîìàòîì B. Ýòîò öèêëè÷åñêèé
àâòîìàò èìååò îäíî ñîñòîÿíèå, çàäàâàåìîå ôîðìóëîé �
�
w t w t u t( ) ( ) ( )2 1 1 , êî-
òîðîå ïîä äåéñòâèåì âõîäíîãî ñèìâîëà u ïåðåõîäèò â ñåáÿ, âûäàâàÿ ñèìâîë �w.
Çàìåòèì, ÷òî ìîùíîñòü ðàññìàòðèâàåìîãî íà ïðàêòèêå ïðîñòðàíñòâà ñîñòîÿ-
íèé Q r( , )� íå âñåãäà ðàâíà 2 1| |( )� r� , à îïðåäåëÿåòñÿ ìèíèìàëüíûìè ðàíãàìè àòî-
ìîâ, îáðàçîâàííûõ êàæäûì èç ïðåäèêàòíûõ ñèìâîëîâ. Òàê, â ðàññìîòðåííîì ïðè-
ìåðå r � 2 è | |� � 2, îäíàêî ìîùíîñòü ïðîñòðàíñòâà ñîñòîÿíèé ðàâíà íå 2 642 3�
� ,
à 2 2 323 2
� � . Ýòî îáóñëîâëåíî îòñóòñòâèåì â ñïåöèôèêàöèè àòîìà u t( )
2 .
ÇÀÊËÞ×ÅÍÈÅ
Âîçìîæíû äâà ïîäõîäà ê îðãàíèçàöèè ïðîöåññà ñîãëàñîâàíèÿ ñïåöèôèêàöèé
âçàèìîäåéñòâóþùèõ àâòîìàòîâ A è B, ïðåäñòàâëåííûõ ñîîòâåòñòâåííî ìíî-
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2016, òîì 52, ¹ 3 13
æåñòâàìè äèçúþíêòîâ CA è CB (C
B
~). Îáà îíè îñíîâàíû íà ìåòîäå ñîãëàñîâà-
íèÿ àâòîìàòîâ, èñïîëüçóþùåì èõ ïàðàëëåëüíóþ öèêëè÷åñêóþ êîìïîçèöèþ.
 ïåðâîì ïîäõîäå, îïèñàííîì â [3], ïðåîáðàçóåòñÿ ñïåöèôèêàöèÿ CA ñîãëàñó-
åìîãî àâòîìàòà ñ äîáàâëåííûìè äèçúþíêòàìè ïåðâîãî ðîäà, âûâîäèìûìè èç C
B
~
ïðè åãî R-ïîïîëíåíèè. Ýòî — äîïîëíèòåëüíûå óòâåðæäåíèÿ, íàëàãàþùèå îãðà-
íè÷åíèÿ íà ïîâåäåíèå àâòîìàòà A. Ïîïîëíåíèå C
B
~ îñóùåñòâëÿåòñÿ îäèí ðàç, è â
äàëüíåéøåì ïîëó÷åííîå ìíîæåñòâî íå èçìåíÿåòñÿ.
Âî âòîðîì ïîäõîäå, ðàññìîòðåííîì â íàñòîÿùåé ñòàòüå, ïðåîáðàçóåòñÿ ñïå-
öèôèêàöèÿ ïàðàëëåëüíîé êîìïîçèöèè àâòîìàòîâ A è
~
B , ò.å. C CA B
� ~. Ïðîöåññ
ñîãëàñîâàíèÿ íà÷èíàåòñÿ ñ R-ïîïîëíåíèÿ ìíîæåñòâà C CA B
� ~. Ïðè ýòîì ïîïîë-
íÿòü ïðèõîäèòñÿ ãîðàçäî áîëüøåå ìíîæåñòâî äèçúþíêòîâ, ÷åì â ïåðâîì ñëó÷àå,
îäíàêî ïîñëåäóþùèå ïðåîáðàçîâàíèÿ âûïîëíÿþòñÿ íàä áîëåå ïðîñòûì àâòîìà-
òîì è óìåíüøàåòñÿ êîëè÷åñòâî ïðîâåðîê êîððåêòíîñòè ñîñòîÿíèé.
 îáîèõ ïîäõîäàõ íå âûïîëíÿåòñÿ ïðåîáðàçîâàíèå ñïåöèôèêàöèè, ñîîòâåòñòâó-
þùåå âûäåëåíèþ ìàêñèìàëüíîãî öèêëè÷åñêîãî ïîäàâòîìàòà â àâòîìàòå A r C( , ), ãäå
C — ðàññìàòðèâàåìîå ìíîæåñòâî äèçúþíêòîâ, õîòÿ ïðîöåññ ñîãëàñîâàíèÿ ñîñòîèò
â óäàëåíèè íåêîððåêòíûõ ñîñòîÿíèé èìåííî â ýòîì àâòîìàòå. Êàê ïîêàçàíî, R-ïî-
ïîëíåíèå ìíîæåñòâà äèçúþíêòîâ C, ïî ñóòè, ñîîòâåòñòâóåò âûäåëåíèþ â àâòîìàòå
A r C( , ) êâàçèöèêëè÷åñêîãî àâòîìàòà, ÷òî óâåëè÷èâàåò êîëè÷åñòâî àíàëèçèðóåìûõ
ñîñòîÿíèé, òàê êàê ïðîâåðÿåòñÿ êîððåêòíîñòü íå òîëüêî ñîñòîÿíèé öèêëè÷åñêîãî
ïîäàâòîìàòà, íî ïðàâèëüíîñòü ïîëó÷àåìîãî ðåçóëüòàòà ñîõðàíÿåòñÿ.
 íàñòîÿùåé ðàáîòå ðàññìîòðåíû äâà ìåòîäà îáíàðóæåíèÿ è óäàëåíèÿ íå-
êîððåêòíûõ ñîñòîÿíèé íà óðîâíå ñïåöèôèêàöèé.  ïåðâîì ìåòîäå, àíàëîãè÷íî
òîìó, êàê ýòî îïèñàíî â [3], àíàëèç êîððåêòíîñòè îãðàíè÷èâàåòñÿ ÷àñòè÷íûìè ñî-
ñòîÿíèÿìè. Ñëåäóåò çàìåòèòü, ÷òî êàê îáíàðóæåíèå ÷àñòè÷íûõ ñîñòîÿíèé, òàê è
âûäåëåíèå êâàçèöèêëè÷åñêîãî ïîäàâòîìàòà â àâòîìàòå A r C( , ) îñóùåñòâëÿþòñÿ
ïðîöåäóðîé ïîïîëíåíèÿ ìíîæåñòâà äèçúþíêòîâ C. Ïîïîëíåíèå îñóùåñòâëÿåòñÿ
íà êàæäîé èòåðàöèè ðàáîòû àëãîðèòìà ïîñëå äîáàâëåíèÿ äèçúþíêòîâ, ñîîòâåò-
ñòâóþùåãî óäàëåíèþ íåêîððåêòíûõ ñîñòîÿíèé. Íà êàæäîì òàêîì ýòàïå, êðîìå
íà÷àëüíîãî, ïîïîëíÿåòñÿ óæå ïîïîëíåííîå ìíîæåñòâî ñ äîáàâëåííûìè ê íåìó
íåñêîëüêèìè äèçúþíêòàìè. Ýòî óïðîùàåò ïðîöåññ ïîïîëíåíèÿ. Óòâåðæäåíèå 2
ïîçâîëÿåò äëÿ íàõîæäåíèÿ ÷àñòè÷íûõ ñîñòîÿíèé èñïîëüçîâàòü íå ïîïîëíåíèå
ìíîæåñòâà äèçúþíêòîâ, à çàìûêàíèå åãî îòíîñèòåëüíî ðåçîëüâèðîâàíèÿ ïî âû-
õîäíûì àòîìàì íóëåâîãî ðàíãà. Îäíàêî, ïîñêîëüêó íåîáõîäèìî âûäåëÿòü êâàçè-
öèêëè÷åñêèé ïîäàâòîìàò â àâòîìàòå A r C( , ), âûïîëíÿåòñÿ R-ïîïîëíåíèå, â êîòî-
ðîì ðåçîëüâèðîâàíèå îñóùåñòâëÿåòñÿ ïî âñåì àòîìàì íóëåâîãî ðàíãà. Êðîìå
òîãî, ïðè ïîïîëíåíèè ìíîæåñòâà äèçúþíêòîâ C CA B
� ~ ÷àñòî óäîáíî
èñïîëüçîâàòü ìåòîä ðàçäåëüíîãî ðåçîëüâèðîâàíèÿ [6], â êîòîðîì äëÿ óìåíüøåíèÿ
êîëè÷åñòâà ïîðîæäàåìûõ äèçúþíêòîâ èñïîëüçóåòñÿ ðàçáèåíèå ïðåäèêàòíûõ
ñèìâîëîâ íà âõîäíûå è âûõîäíûå.
Âî âòîðîì ìåòîäå àíàëèçèðóþòñÿ âñå ñîñòîÿíèÿ àâòîìàòà A r C( , ), ïðåäñòàâ-
ëåííûå äèçúþíêòèâíîé íîðìàëüíîé ôîðìîé ôîðìóëû f t( ). Çäåñü äëÿ óìåíüøå-
íèÿ êîëè÷åñòâà àíàëèçèðóåìûõ ñîñòîÿíèé èñïîëüçóåòñÿ äîáàâëåíèå âî ìíîæåñ-
òâî C âñåâîçìîæíûõ ñäâèãîâ âëåâî èìåþùèõñÿ â íåì äèçúþíêòîâ, íå âûâîäÿùåå
ïðåîáðàçîâàííóþ ôîðìóëó f t( ) çà ðàìêè èñõîäíîãî ïðîñòðàíñòâà ñîñòîÿíèé. Äî-
áàâëåíèå òàêèõ äèçúþíêòîâ óäàëÿåò ñîñòîÿíèÿ, íå ïðèíàäëåæàùèå öèêëè÷åñêî-
ìó ïîäàâòîìàòó àâòîìàòà A r C( , ) .
 ñòàòüå îïèñàíû äâà ñïîñîáà îïðåäåëåíèÿ ñåìàíòèêè ÿçûêà L, êîòîðûå ðàç-
ëè÷àþòñÿ äëèíîé ñëîâ â àëôàâèòå � �( ), ïðåäñòàâëÿþùèõ ñîñòîÿíèÿ ñïåöèôèöèðó-
åìîãî àâòîìàòà. Èñïîëüçîâàíèå ñëîâ äëèíû r â 2| |� ðàç óìåíüøàåò ïðîñòðàíñòâî,
14 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2016, òîì 52, ¹ 3
â êîòîðîì ðàçìåùàþòñÿ ñîñòîÿíèÿ àâòîìàòà A r Cr ( , ), è, ñëåäîâàòåëüíî, ïðèìåðíî
âî ñòîëüêî æå ðàç óìåíüøàåòñÿ êîëè÷åñòâî àíàëèçèðóåìûõ ñîñòîÿíèé. Ïîýòîìó âî
âòîðîì èç îïèñàííûõ ìåòîäîâ óäîáíî èñïîëüçîâàòü òàêóþ ñåìàíòèêó ÿçûêà L.
Öåëåñîîáðàçíîñòü ïðèìåíåíèÿ êàæäîãî èç óêàçàííûõ òðåõ ìåòîäîâ ñîãëàñî-
âàíèÿ ñïåöèôèêàöèé îïðåäåëÿåòñÿ âèäîì èñõîäíîé ñïåöèôèêàöèè âçàèìîäåé-
ñòâóþùèõ àâòîìàòîâ. Îòìåòèì, ÷òî äîáàâëåíèå â C
B
~ ñäâèãîâ äèçúþíêòîâ âëåâî
öåëåñîîáðàçíî èñïîëüçîâàòü è â ìåòîäå, îïèñàííîì â [3].
ÑÏÈÑÎÊ ËÈÒÅÐÀÒÓÐÛ
1 × å á î ò à ð å â À . Í . Ðåãóëÿðíàÿ ôîðìà ñïåöèôèêàöèè äåòåðìèíèðîâàííûõ àâòîìàòîâ â ÿçûêå L //
Ïðèêëàä. äèñêðåò. ìàòåìàòèêà. — 2010. — ¹ 4. — Ñ. 64–72.
2. × å á î ò à ð å â À . Í . Ñîãëàñîâàíèå âçàèìîäåéñòâóþùèõ àâòîìàòîâ // Êèáåðíåòèêà è ñèñòåìíûé àíà-
ëèç. — 2015. — ¹ 5. — Ñ. 13–25.
3. × å á î ò à ð å â À . Í . Îáùèé ìåòîä ïðîâåðêè ñîãëàñîâàííîñòè âçàèìîäåéñòâóþùèõ àâòîìàòîâ ñ êî-
íå÷íîé ïàìÿòüþ // Êèáåðíåòèêà è ñèñòåìíûé àíàëèç. — 1999. — ¹ 6. — Ñ. 25–37.
4. × å í ü × . , Ë è Ð . Ìàòåìàòè÷åñêàÿ ëîãèêà è àâòîìàòè÷åñêîå äîêàçàòåëüñòâî òåîðåì. — Ì.: Íàóêà,
1973. — 360 ñ.
5. × å á î ò à ð å â À . Í . Ïðîâåðêà íåïðîòèâîðå÷èâîñòè ïðîñòûõ ñïåöèôèêàöèé àâòîìàòíûõ ñèñòåì //
Êèáåðíåòèêà è ñèñòåìíûé àíàëèç. — 1994. — ¹ 3. — Ñ. 3–11.
6. × å á î ò à ð å â À . Í . Ìåòîä ðàçäåëüíîãî ðåçîëüâèðîâàíèÿ äëÿ ïðîâåðêè âûïîëíèìîñòè ôîðìóë ÿçûêà L
// Êèáåðíåòèêà è ñèñòåìíûé àíàëèç. — 1998. — ¹ 6. — Ñ. 13–20.
Íàä³éøëà äî ðåäàêö³¿ 01.09.2015
À.Ì. ×åáîòàðüîâ
ÓÇÃÎÄÆÅÍÍß ÑÏÅÖÈÔ²ÊÀÖ²É ÀÂÒÎÌÀÒ²Â, ÙÎ ÏÎÄÀͲ ÌÎÂÎÞ L
Àíîòàö³ÿ. Ðîçãëÿíóòî äâà ìåòîäè óçãîäæåííÿ ñïåöèô³êàö³é àâòîìàò³â, ùî
âçàºìîä³þòü. Ñïåöèô³êàö³¿ ïîäàí³ ó âèãëÿä³ ìíîæèí äèç’þíêò³â ó ìîâ³ L.
Îáèäâà ìåòîäè áàçóþòüñÿ íà ìåòîä³ óçãîäæåííÿ àâòîìàò³â, ÿêèé âèêîðèñòî-
âóº ¿õíþ ïàðàëåëüíó êîìïîçèö³þ. Íàâåäåíî äâà ñïîñîáè âèçíà÷åííÿ ñåìàí-
òèêè ìîâè L, ïðèéíÿò³ ó ðîçãëÿíóòèõ ìåòîäàõ óçãîäæåííÿ ñïåöèô³êàö³é.
Êëþ÷îâ³ ñëîâà: ñïåöèô³êàö³ÿ àâòîìàòà, ìîâà L, óçãîäæåííÿ ñïåöèô³êàö³é,
êîìïîçèö³ÿ ñïåöèô³êàö³é, êîðåêòí³ñòü êîìïîçèö³¿.
A.N. Chebotarev
HARMONIZATION OF AUTOMATA SPECIFICATIONS REPRESENTED IN THE LANGUAGE L
Abstract. The author considers two methods for harmonization of automata
specifications represented as sets of clauses in the language L. Both methods are
based on the automata harmonization technique, which uses their parallel
composition. Two ways to determine language L semantics that are used in the
harmonization methods are described.
Keywords: automaton specification, language L, harmonization of specification,
composition of specification, composition correctness.
×åáîòàðåâ Àíàòîëèé Íèêîëàåâè÷,
äîêòîð òåõí. íàóê, âåäóùèé íàó÷íûé ñîòðóäíèê Èíñòèòóòà êèáåðíåòèêè ÍÀÍ Óêðàèíû
èì. Â.Ì. Ãëóøêîâà, Êèåâ, e-mail: ancheb@gmail.com.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2016, òîì 52, ¹ 3 15
|