Согласование взаимодействующих автоматов
Проблема согласования автоматов состоит в том, чтобы спроектировать систему, поведение которой при ее взаимодействии со средой будет удовлетворять заданным требованиям независимо от возможного поведения среды. Приведен ряд теоретических результатов, используемых при решении проблемы согласования, и...
Saved in:
| Published in: | Кибернетика и системный анализ |
|---|---|
| Date: | 2015 |
| Main Author: | |
| Format: | Article |
| Language: | Russian |
| Published: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2015
|
| Subjects: | |
| Online Access: | https://nasplib.isofts.kiev.ua/handle/123456789/124902 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Cite this: | Согласование взаимодействующих автоматов / А.Н. Чеботарев // Кибернетика и системный анализ. — 2015. — Т. 51, № 5. — С. 13-25. — Бібліогр.: 14 назв. — рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1859931943701839872 |
|---|---|
| author | Чеботарев, А.Н. |
| author_facet | Чеботарев, А.Н. |
| citation_txt | Согласование взаимодействующих автоматов / А.Н. Чеботарев // Кибернетика и системный анализ. — 2015. — Т. 51, № 5. — С. 13-25. — Бібліогр.: 14 назв. — рос. |
| collection | DSpace DC |
| container_title | Кибернетика и системный анализ |
| description | Проблема согласования автоматов состоит в том, чтобы спроектировать систему, поведение которой при ее взаимодействии со средой будет удовлетворять заданным требованиям независимо от возможного поведения среды. Приведен ряд теоретических результатов, используемых при решении проблемы согласования, и основанные на них алгоритмы ее решения.
Проблема узгодження автоматів полягає в тому, щоб спроектувати систему, поведінка якої при її взаємодії з середовищем буде задовольняти задані вимоги незалежно від можливої поведінки середовища. Наведено низку теоретичних результатів, що використовуються при розв’язанні проблеми узгодження, та алгоритми її розв’язання, які базуються на цих результатах.
The problem of automata harmonization is to design a system whose behavior during the interaction with its environment meets given requirements regardless of the environment’s behavior. A number of theoretical results employed in solving the harmonization problem and corresponding algorithms based on these results are presented.
|
| first_indexed | 2025-12-07T16:08:52Z |
| format | Article |
| fulltext |
ÓÄÊ 519.713.1
À.Í. ×ÅÁÎÒÀÐÅÂ
ÑÎÃËÀÑÎÂÀÍÈÅ ÂÇÀÈÌÎÄÅÉÑÒÂÓÞÙÈÕ ÀÂÒÎÌÀÒÎÂ
Àííîòàöèÿ. Ïðîáëåìà ñîãëàñîâàíèÿ àâòîìàòîâ ñîñòîèò â òîì, ÷òîáû ñïðîåêòèðîâàòü ñèñ-
òåìó, ïîâåäåíèå êîòîðîé ïðè åå âçàèìîäåéñòâèè ñî ñðåäîé áóäåò óäîâëåòâîðÿòü çàäàííûì
òðåáîâàíèÿì íåçàâèñèìî îò âîçìîæíîãî ïîâåäåíèÿ ñðåäû. Ïðèâåäåí ðÿä òåîðåòè÷åñêèõ
ðåçóëüòàòîâ, èñïîëüçóåìûõ ïðè ðåøåíèè ïðîáëåìû ñîãëàñîâàíèÿ, è îñíîâàííûå íà íèõ
àëãîðèòìû åå ðåøåíèÿ.
Êëþ÷åâûå ñëîâà: âçàèìîäåéñòâèå àâòîìàòîâ, êîìïîçèöèè àâòîìàòîâ, ñäâèã àâòîìàòà ïî
âõîäó, ñîãëàñîâàíèå àâòîìàòîâ, êîððåêòíîñòü êîìïîçèöèè.
ÂÂÅÄÅÍÈÅ
Çàäà÷è ñîãëàñîâàíèÿ àâòîìàòîâ âîçíèêàþò ïðè èñïîëüçîâàíèè òåîðåòèêî-àâòî-
ìàòíîãî ïîäõîäà ê ïðîåêòèðîâàíèþ ðåàêòèâíûõ àëãîðèòìîâ, ò.å. àëãîðèòìîâ
âçàèìîäåéñòâèÿ ïðîåêòèðóåìîé ñèñòåìû ñî ñðåäîé, â êîòîðîé îíà ôóíêöèîíè-
ðóåò. Ñðåäà, êàê ïðàâèëî, íåäåòåðìèíèðîâàííà è â ñèëó ýòîãî ìîæåò ðàçëè÷-
íûì îáðàçîì ðåàãèðîâàòü íà äåéñòâèÿ ïðîåêòèðóåìîé ñèñòåìû. Çàäà÷à ñîñòîèò
â òîì, ÷òîáû ñïðîåêòèðîâàòü àëãîðèòì ôóíêöèîíèðîâàíèÿ òàêîé ñèñòåìû, ïî-
âåäåíèå êîòîðîé ïðè åå âçàèìîäåéñòâèè ñî ñðåäîé áóäåò óäîâëåòâîðÿòü çàäàí-
íûì òðåáîâàíèÿì íåçàâèñèìî îò âîçìîæíîãî ïîâåäåíèÿ ñðåäû. Òðåáîâàíèÿ
ê ñîâìåñòíîìó ïîâåäåíèþ ñèñòåìû è ñðåäû, ñ êîòîðîé îíà âçàèìîäåéñòâóåò,
îáû÷íî ôîðìóëèðóþòñÿ â êàêîì-ëèáî ëîãè÷åñêîì ÿçûêå, òàêîì êàê ðàçëè÷íî-
ãî ðîäà òåìïîðàëüíûå ëîãèêè, ëîãèêè ïåðâîãî ïîðÿäêà èëè îãðàíè÷åííûå ëî-
ãèêè âòîðîãî ïîðÿäêà.  êà÷åñòâå ìîäåëåé ïðîåêòèðóåìîé ñèñòåìû è ñðåäû
èñïîëüçóþòñÿ àâòîìàòíûå ìîäåëè, íàïðèìåð àâòîìàòû-ðàñïîçíàâàòåëè íàä áåñ-
êîíå÷íûìè ñëîâàìè èëè äåðåâüÿìè, òðàíçèöèîííûå ñèñòåìû, òðàíñäüþñåðû
(àâòîìàòû ñ âõîäîì è âûõîäîì) è äð. Ïðè ýòîì âîçíèêàåò ïðîáëåìà âûÿñíå-
íèÿ âîçìîæíîñòè ðåàëèçàöèè (ðåàëèçóåìîñòè) òðåáîâàíèé ê ïîâåäåíèþ ðåàê-
òèâíîé ñèñòåìû â âèäå ïîâåäåíèÿ ñîîòâåòñòâóþùåé àâòîìàòíîé ìîäåëè. Î÷å-
âèäíî, ÷òî òðåáîâàíèÿ, â ÿâíîé èëè íåÿâíîé ôîðìå îãðàíè÷èâàþùèå ïîâåäåíèå
ñðåäû, íå ìîãóò áûòü ðåàëèçîâàíû, ïîñêîëüêó ïðåäïîëàãàåòñÿ, ÷òî íèêàêèå
äîïîëíèòåëüíûå îãðàíè÷åíèÿ íà ïîâåäåíèå ñðåäû, êðîìå òåõ, ÷òî îïðåäåëÿþò-
ñÿ åå ñïåöèôèêàöèåé, íå äîëæíû íàëàãàòüñÿ.
Ýòà ïðîáëåìà áûëà ñôîðìóëèðîâàíà À. ×åð÷åì [1] â âèäå ñëåäóþùåé ïðî-
áëåìû ðàçðåøèìîñòè. Ïóñòü X è Y — êîíå÷íûå àëôàâèòû, à R X Y� �� � — ðå-
ãóëÿðíîå îòíîøåíèå, ò.å. îòíîøåíèå, êîòîðîå ìîæåò áûòü çàäàíî êàêèì-ëèáî àâ-
òîìàòîì-ðàñïîçíàâàòåëåì íàä áåñêîíå÷íûìè ñëîâàìè â àëôàâèòå X Y� . Ïðîáëå-
ìà ðàçðåøèìîñòè ôîðìóëèðóåòñÿ ñëåäóþùèì îáðàçîì: ñóùåñòâóåò ëè òàêàÿ
ôóíêöèÿ f X Y: � �� , ÷òî äëÿ âñåõ w X� � èìååò ìåñòî R w f w( , ( ))? Ðàçëè÷íûå
îãðàíè÷åíèÿ è óòî÷íåíèÿ ýòîé ïðîáëåìû ñâÿçàíû ñî ñïîñîáîì çàäàíèÿ îòíîøå-
íèÿ R, íàïðèìåð ôîðìóëîé ëîãèêè LTL èëè CTL*, è îãðàíè÷åíèÿìè, íàëàãàåìû-
ìè íà ôóíêöèþ f , òàêæå ñâÿçàííûìè ñî ñïîñîáîì åå çàäàíèÿ, ñêàæåì, â âèäå
X Y/ -òðàíñäüþñåðà. Òàêèå ìîäèôèêàöèè ïðîáëåìû ðàçðåøèìîñòè ×åð÷à îáû÷íî
íàçûâàþòñÿ ïðîáëåìàìè ðåàëèçóåìîñòè.
Ïðèìåíèòåëüíî ê ïðîåêòèðîâàíèþ ðåàêòèâíûõ ñèñòåì çàäàíèå îòíîøåíèÿ R
ðàññìàòðèâàåòñÿ êàê ñïåöèôèêàöèÿ ïðîåêòèðóåìîé ñèñòåìû, à ôóíêöèÿ f ðåàëè-
çóåòñÿ òðàíñäüþñåðîì [2].  ïðîñòåéøåì ñëó÷àå, êîãäà èíôîðìàöèÿ î ïîâåäåíèè
ñðåäû îòñóòñòâóåò, à ñïåöèôèêàöèÿ ñèñòåìû çàäàíà â âèäå íåèíèöèàëèçèðîâàí-
íîãî òðàíñäüþñåðà A èëè ëþáîé äðóãîé ýêâèâàëåíòíîé ìîäåëè êîíå÷íîãî àâòî-
ìàòà, îíà ðåàëèçóåìà, åñëè àâòîìàò A ñîäåðæèò öèêëè÷åñêèé âïîëíå îïðåäåëåí-
íûé ïîäàâòîìàò. Çàìåòèì, ÷òî ìíîæåñòâî ñîñòîÿíèé òàêîãî ïîäàâòîìàòà çàìêíó-
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2015, òîì 51, ¹ 5 13
� À.Í. ×åáîòàðåâ, 2015
òî îòíîñèòåëüíî ôóíêöèè ïåðåõîäîâ. Ñèòóàöèÿ óñëîæíÿåòñÿ ïðè íàëè÷èè
èíôîðìàöèè î ñðåäå, êîòîðàÿ çàäàåòñÿ àíàëîãè÷íûì îáðàçîì.  ýòîì ñëó÷àå ñïå-
öèôèêàöèÿ ñèñòåìû ðåàëèçóåìà, äàæå åñëè ñîîòâåòñòâóþùèé åé àâòîìàò íå èìå-
åò öèêëè÷åñêîãî âïîëíå îïðåäåëåííîãî ïîäàâòîìàòà, îäíàêî èìååò öèêëè÷åñêèé
ïîäàâòîìàò, ÷àñòè÷íîñòü êîòîðîãî ñîãëàñîâàíà ñî ñðåäîé, ò.å. íå íàëàãàåò äîïîë-
íèòåëüíûõ îãðàíè÷åíèé íà åå ïîâåäåíèå. Îòñþäà âîçíèêàåò ïðîáëåìà ñîãëàñîâà-
íèÿ ñïåöèôèêàöèè ñèñòåìû ñî ñïåöèôèêàöèåé ñðåäû. Ïîíÿòèå ñîãëàñóåìîñòè
ñïåöèôèêàöèè ñèñòåìû ñî ñðåäîé, â îòëè÷èå îò áîëåå îáùåãî ïîíÿòèÿ ðåàëèçóå-
ìîñòè ñïåöèôèêàöèè ñèñòåìû, ñâÿçàíî ñ îãðàíè÷åíèåì ñâîéñòâ, îïðåäåëÿåìûõ
ñïåöèôèêàöèÿìè ñèñòåìû è ñðåäû, ñâîéñòâàìè áåçîïàñíîñòè (safety) [3].
Îãðàíè÷åíèå ñâîéñòâ, îïðåäåëÿåìûõ ñïåöèôèêàöèåé, ñâîéñòâàìè, ïðåäñòàâèìû-
ìè òðàíñäüþñåðîì, ïîçâîëÿåò ðåøàòü çàäà÷ó ñîãëàñîâàíèÿ êàê íà óðîâíå
ñïåöèôèêàöèé, òàê è íà óðîâíå ñèíòåçèðîâàííûõ àâòîìàòîâ.
Âïåðâûå ïðîáëåìà ñîãëàñîâàíèÿ àâòîìàòîâ áûëà ñôîðìóëèðîâàíà â 1991 ã.
â [4], ãäå áûëî îïðåäåëåíî ïîíÿòèå ñîãëàñîâàííîñòè äâóõ ÷àñòè÷íûõ íåäåòåðìè-
íèðîâàííûõ àâòîìàòîâ Ìóðà è ïðåäëîæåíû àëãîðèòìû ñîãëàñîâàíèÿ àâòîìàòîâ
ñ êîíå÷íîé ïàìÿòüþ. Ïîíÿòèå ñîãëàñîâàííîñòè íåäåòåðìèíèðîâàííûõ àâòîìàòîâ
îïðåäåëÿëîñü íåêîíñòðóêòèâíî ÷åðåç ïîíÿòèå ñîãëàñîâàííîñòè äåòåðìèíèðîâàí-
íûõ àâòîìàòîâ è áåñêîíå÷íûå ìíîæåñòâà äåòåðìèíèçàöèé íåäåòåðìèíèðîâàííûõ
àâòîìàòîâ. Äëÿ êîíñòðóêòèâíîãî ðåøåíèÿ çàäà÷è ñîãëàñîâàíèÿ ïðèøëîñü îãðàíè-
÷èòüñÿ àâòîìàòàìè ñ êîíå÷íîé ïàìÿòüþ.  [5] ñîîòâåòñòâóþùèå çàäà÷è ðàññìàò-
ðèâàëèñü íà óðîâíå ëîãè÷åñêèõ ñïåöèôèêàöèé àâòîìàòîâ. Ïðèâåäåíû àëãîðèòìû
ñîãëàñîâàíèÿ ñïåöèôèêàöèé â ÿçûêå L, ãàðàíòèðóþùèå, ÷òî àâòîìàòû, ñèíòåçè-
ðîâàííûå ïî ñîãëàñîâàííûì ñïåöèôèêàöèÿì, áóäóò ñîãëàñîâàíû.
 íàñòîÿùåé ðàáîòå äàåòñÿ áîëåå îáùåå êîíñòðóêòèâíîå îïðåäåëåíèå ïîíÿ-
òèÿ ñîãëàñîâàííîñòè àâòîìàòîâ, íå îãðàíè÷èâàþùååñÿ àâòîìàòàìè ñ êîíå÷íîé
ïàìÿòüþ. Ïðèâîäèòñÿ ðÿä òåîðåòè÷åñêèõ ðåçóëüòàòîâ, èñïîëüçóåìûõ ïðè ðåøå-
íèè çàäà÷è ñîãëàñîâàíèÿ, à òàêæå îïèñûâàåòñÿ ïîäõîä, îñíîâàííûé íà ïîíÿòèè
êîððåêòíîñòè ïàðàëëåëüíîé êîìïîçèöèè �-àâòîìàòîâ.
Ðàáîòà ñîñòîèò èç äâóõ ÷àñòåé. Ïåðâàÿ, ïðåäñòàâëåííàÿ íàñòîÿùåé ñòàòüåé,
ïîñâÿùåíà ðåøåíèþ ïðîáëåìû ñîãëàñîâàíèÿ àâòîìàòîâ, âòîðàÿ — ïðîáëåìå ñî-
ãëàñîâàíèÿ ñïåöèôèêàöèé àâòîìàòîâ â ÿçûêå L.
ÌÎÄÅËÈ ÀÂÒÎÌÀÒÎÂ È ÈÕ ÊÎÌÏÎÇÈÖÈÈ
Ðàññìàòðèâàþòñÿ ÷àñòè÷íûå íåäåòåðìèíèðîâàííûå X Y/ -àâòîìàòû Ìóðà. Òà-
êîé àâòîìàò A îïðåäåëÿåòñÿ ïÿòåðêîé � X Y Q A A, , , ,� � , ãäå X Y Q, , — êîíå÷-
íûå ìíîæåñòâà ñîîòâåòñòâåííî âõîäíûõ ñèìâîëîâ, âûõîäíûõ ñèìâîëîâ è ñî-
ñòîÿíèé, à �A
QQ X: � � 2 è �A Q Y: � — âñþäó îïðåäåëåííûå ôóíêöèè ïå-
ðåõîäîâ è âûõîäîâ. Åñëè | |X
1, òî àâòîìàò A íàçûâàåòñÿ àâòîíîìíûì
Y -àâòîìàòîì, êîòîðûé îïðåäåëÿåòñÿ ÷åòâåðêîé � Y Q A A, , ,� � . Ôóíêöèÿ ïåðå-
õîäîâ òàêîãî àâòîìàòà èìååò âèä �A
QQ: � 2 .
Íåäåòåðìèíèðîâàííûé X Y/ -àâòîìàò A áóäåì íàçûâàòü êâàçèäåòåðìèíèðî-
âàííûì, åñëè äëÿ ëþáûõ q q q Q, ,1 2 � è x X� èç q q q xA1 2, ( , )� � ñëåäóåò
� �A Aq q( ) ( )1 2� . Àíàëîãè÷íî íåäåòåðìèíèðîâàííûé àâòîíîìíûé Y -àâòîìàò
A Y Q A A
� , , ,� � íàçûâàåòñÿ êâàçèäåòåðìèíèðîâàííûì, åñëè äëÿ êàæäîãî q Q�
è ëþáûõ q q qA1 2, ( )� � âûïîëíÿåòñÿ � �A Aq q( ) ( )1 2� .
Êâàçèäåòåðìèíèðîâàííûé X Y/ -àâòîìàò èíîãäà óäîáíî ïðåäñòàâëÿòü â âèäå
äåòåðìèíèðîâàííîãî àâòîìàòà áåç âûõîäîâ ñ òåì æå ìíîæåñòâîì ñîñòîÿíèé è
ñ âõîäíûì àëôàâèòîì �A X Y
� . Òàêîé àâòîìàò A QA A A
� � , , � , ãäå �A —
âõîäíîé àëôàâèò, QA — ìíîæåñòâî ñîñòîÿíèé, à �A A A AQ Q: � �� — ÷àñòè÷íàÿ
ôóíêöèÿ ïåðåõîäîâ, íàçîâåì �-àâòîìàòîì (çàìåòèì, ÷òî â ïîíÿòèè «�-àâòîìàò»
ñèìâîë � îáîçíà÷àåò òèï àâòîìàòà, à íå íàçâàíèå àëôàâèòà, êàê ýòî èìååò ìåñòî
äëÿ àâòîíîìíîãî Y -àâòîìàòà). Â äàëüíåéøåì ñèìâîëû àëôàâèòà �
�X Y áóäåì
çàïèñûâàòü â âèäå xy, ãäå x X� , y Y� . Ôóíêöèÿ ïåðåõîäîâ �-àâòîìàòà, ñîîòâåò-
ñòâóþùåãî êâàçèäåòåðìèíèðîâàííîìó X Y/ -àâòîìàòó Ìóðà A, îïðåäåëÿåòñÿ ñëå-
14 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2015, òîì 51, ¹ 5
äóþùèì îáðàçîì: �A q xy q( , )
1 òîãäà è òîëüêî òîãäà, êîãäà äëÿ X Y/ -àâòîìàòà A
q q xA1 � � ( , ) è �A q y( )1
. Óòâåðæäåíèå âèäà �A q xy q( , )
1 áóäåì íàçûâàòü
ïåðåõîäîì è çàïèñûâàòü â âèäå q xy q: � 1. Ñèìâîë âõîäíîãî àëôàâèòà xy â òàêîé
çàïèñè íàçûâàåòñÿ îòìåòêîé ïåðåõîäà.
 äàëüíåéøåì îãðàíè÷èìñÿ ðàññìîòðåíèåì êâàçèäåòåðìèíèðîâàííûõ àâòîìàòîâ.
�-àâòîìàò A QA A A
� � , , � íàçûâàåòñÿ öèêëè÷åñêèì, åñëè äëÿ êàæäîãî
q QA� ñóùåñòâóþò òàêèå � �1 2, ��A è q q QA1 2, � , ÷òî q qA1 1
� �( , ) è
q qA
� �( , )2 2 . Àâòîìàò, óäîâëåòâîðÿþùèé òîëüêî ïåðâîìó èç óêàçàííûõ òðåáî-
âàíèé, íàçîâåì êâàçèöèêëè÷åñêèì. Î÷åâèäíî, ÷òî àâòîìàòíàÿ ìîäåëü ðåàêòèâíîé
ñèñòåìû äîëæíà áûòü ïî êðàéíåé ìåðå êâàçèöèêëè÷åñêèì àâòîìàòîì. Ëþáîé
èíèöèàëüíûé êâàçèöèêëè÷åñêèé àâòîìàò, ò.å. àâòîìàò ñ âûäåëåííûìè íà÷àëüíû-
ìè ñîñòîÿíèÿìè, ìîæåò áûòü çàäàí â âèäå ïàðû � A Q, 0 , ãäå A — öèêëè÷åñêèé
àâòîìàò, à Q0 — ìíîæåñòâî íà÷àëüíûõ ñîñòîÿíèé. Ìàêñèìàëüíûé öèêëè÷åñêèé
ïîäàâòîìàò àâòîìàòà íàçîâåì åãî ÿäðîì.
Ïîâåäåíèå öèêëè÷åñêîãî àâòîìàòà õàðàêòåðèçóåòñÿ ìíîæåñòâîì äîïóñòè-
ìûõ äëÿ íåãî ñâåðõñëîâ (áåñêîíå÷íûõ ñëîâ).
Ñâåðõñëîâî l
� � �1 2 3 � â àëôàâèòå �A äîïóñòèìî â ñîñòîÿíèè q �-àâòî-
ìàòà A, åñëè ñóùåñòâóåò òàêîå ñâåðõñëîâî ñîñòîÿíèé q q q0 1 2 � , ãäå q q0
, ÷òî
äëÿ ëþáîãî i
�0 1 2, , , q qi A i i
1 1� �( , ). Áóäåì ãîâîðèòü, ÷òî ñâåðõñëîâî ñî-
ñòîÿíèé q q q0 1 2 � ñîîòâåòñòâóåò âõîäíîìó ñâåðõñëîâó l.
Ñâåðõñëîâî l
� � �0 1 2 � â àëôàâèòå Y äîïóñòèìî â ñîñòîÿíèè q àâòîíîì-
íîãî Y -àâòîìàòà A, åñëè ñóùåñòâóåò òàêîå ñâåðõñëîâî ñîñòîÿíèé q q q0 1 2 � , ãäå
q q0
, ÷òî äëÿ ëþáîãî i
�0 1 2, , , q qi A i
�1 � ( ) è � �A i iq( )
1 .
Ýòè îïðåäåëåíèÿ ëåãêî ïåðåôîðìóëèðîâàòü äëÿ X Y/ -àâòîìàòîâ.
Ìíîæåñòâî âñåõ ñâåðõñëîâ, äîïóñòèìûõ â ñîñòîÿíèè q, îáîçíà÷àåòñÿ W q( ).
Ñîñòîÿíèÿ q1 è q2 îäíîãî è òîãî æå èëè ðàçëè÷íûõ àâòîìàòîâ íàçûâàþòñÿ ýêâè-
âàëåíòíûìè, åñëè W q W q( ) ( )1 2
.
Ñâåðõñëîâî l äîïóñòèìî äëÿ àâòîìàòà A, åñëè îíî äîïóñòèìî õîòÿ áû â îä-
íîì èç åãî ñîñòîÿíèé. Ìíîæåñòâî âñåõ ñâåðõñëîâ, äîïóñòèìûõ äëÿ àâòîìàòà A,
îáîçíà÷àåòñÿ W A( ).
Àâòîìàòû A è B íàçûâàþòñÿ ñòðîãî ýêâèâàëåíòíûìè (îáîçíà÷àåòñÿ A B~ ),
åñëè äëÿ êàæäîãî ñîñòîÿíèÿ àâòîìàòà A èìååòñÿ ýêâèâàëåíòíîå åìó ñîñòîÿíèå
àâòîìàòà B è íàîáîðîò.
Ïóñòü q t( ) îáîçíà÷àåò ñîñòîÿíèå àâòîìàòà A â ìîìåíò äèñêðåòíîãî âðåìåíè t,
à s t( ) — ñîñòîÿíèå àâòîìàòà B â ýòîò æå ìîìåíò. Ðàññìàòðèâàåìûé ñïîñîá âçà-
èìîäåéñòâèÿ íåäåòåðìèíèðîâàííûõ àâòîìàòîâ Ìóðà A X Y QA A A
� , , , ,� � è
B Y X QB B B
� , , , ,� � ìîæíî îïèñàòü ñîîòíîøåíèÿìè
q t q t x tA( ) ( ( ), ( )),� �� 1 y t q tA( ) ( ( ))
� ,
s t s t y tB( ) ( ( ), ( ))� � �� 1 1 , x t s tB( ) ( ( ))
� .
Âîçìîæíû è äðóãèå ñïîñîáû îðãàíèçàöèè âçàèìîäåéñòâèÿ àâòîìàòîâ. Âûáîð
òîé èëè èíîé ìîäåëè âçàèìîäåéñòâèÿ îïðåäåëÿåòñÿ ñïîñîáîì ðåàëèçàöèè ïðî-
åêòèðóåìîãî àëãîðèòìà. Ðàññìàòðèâàåìàÿ çäåñü ìîäåëü âçàèìîäåéñòâèÿ îðèåí-
òèðîâàíà íà àïïàðàòóðíóþ ðåàëèçàöèþ, êîãäà âçàèìîäåéñòâèå îñóùåñòâëÿåòñÿ
ñ ïîìîùüþ ïåðåäà÷è ñèãíàëîâ, à íå ñîîáùåíèé. Ñîâìåñòíîå ïîâåäåíèå àâòî-
ìàòîâ, âçàèìîäåéñòâóþùèõ ñîãëàñíî îïèñàííîìó âûøå ñïîñîáó, õàðàêòåðèçó-
åòñÿ èõ ïðàâîé êîìïîçèöèåé.
Îïðåäåëåíèå 1. Ïðàâàÿ êîìïîçèöèÿ àâòîìàòîâ A X Y QA A A
� , , , ,� � è
B Y X QB B B
� , , , ,� � (îáîçíà÷àåòñÿ A B|� ) ïðåäñòàâëÿåò ñîáîé àâòîíîìíûé, íå-
äåòåðìèíèðîâàííûé Z-àâòîìàò Ìóðà C Z QC C C
� , , ,� � , ãäå Z Y X
� ,
Q Q QC A B
� , à ôóíêöèÿ ïåðåõîäîâ �C è ôóíêöèÿ âûõîäîâ �C îïðåäåëÿþòñÿ
ñëåäóþùèì îáðàçîì. Äëÿ q QA� , s QB� � � �C B Aq s q s s s q( , ) ( , ) | ( , ( )),
� � � �{
� � �q q sA B� �( , ( ))}, � � �C A Bq s q s( , ) ( ( ), ( ))
.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2015, òîì 51, ¹ 5 15
Ýòî îïðåäåëåíèå íå ñèììåòðè÷íî îòíîñèòåëüíî àâòîìàòîâ A è B. Î÷åâèäíî, ÷òî
êîìïîçèöèÿ A è B íå ñîâïàäàåò ñ êîìïîçèöèåé B è A. Çàìåòèì, ÷òî ïðàâàÿ êîìïîçèöèÿ
êâàçèäåòåðìèíèðîâàííûõ àâòîìàòîâ òàêæå ÿâëÿåòñÿ êâàçèäåòåðìèíèðîâàííûì àâòîìàòîì.
Ðàññìàòðèâàÿ àâòîìàò Ñ êàê �-àâòîìàò, ïðèâåäåííîå îïðåäåëåíèå ìîæíî ïå-
ðåôîðìóëèðîâàòü òàê: C Z QC C
� , , � , ãäå Z X Y
� , Q Q QC A B
� , à ôóíêöèÿ
ïåðåõîäîâ �C îïðåäåëÿåòñÿ ñëåäóþùèì îáðàçîì. Äëÿ ëþáûõ q QA� , s QB� ,
x X� , y Y� �C q s xy(( , ), ) = ( ' , ' )q s òîãäà è òîëüêî òîãäà, êîãäà â Y X/ -àâòîìàòå B
s s qB A' ( , ( ))� � � , �B s x( ' )
è â X Y/ -àâòîìàòå A q q xA' ( , )� � , �A q y( ' )
.
ÑÎÃËÀÑÎÂÀÍÍÎÑÒÜ ÀÂÒÎÌÀÒÎÂ
Íåôîðìàëüíî X Y/ -àâòîìàò A ñîãëàñîâàí ñ Y X/ -àâòîìàòîì B, åñëè ïðè èõ
âçàèìîäåéñòâèè íå ìîæåò âîçíèêíóòü ñèòóàöèè, êîãäà ïåðåõîä â îäíîì èç àâ-
òîìàòîâ ïîä äåéñòâèåì ñèãíàëà, ïîñòóïàþùåãî èç äðóãîãî àâòîìàòà, áóäåò íå
îïðåäåëåí. Òàêîå âçàèìîäåéñòâèå àâòîìàòîâ íàçîâåì êîððåêòíûì. Î÷åâèäíî,
÷òî âïîëíå îïðåäåëåííûé àâòîìàò A ñîãëàñîâàí ñ ëþáûì âïîëíå îïðåäåëåí-
íûì àâòîìàòîì B. Êðîìå òîãî, åñëè ïðàâàÿ êîìïîçèöèÿ àâòîìàòîâ A è B íå
ñîäåðæèò öèêëè÷åñêîãî ïîäàâòîìàòà, òî àâòîìàò A íå ñîãëàñîâàí ñ àâòîìàòîì B.
Êîìïîçèöèÿ C A B
�| îïðåäåëÿåò ìíîæåñòâî X Y� -ñâåðõñëîâ, êîòîðûå ìî-
ãóò áûòü ïîðîæäåíû â ïðîöåññå âçàèìîäåéñòâèÿ àâòîìàòîâ A è B. Îäíàêî íå âñå
ýòè ñâåðõñëîâà ñîîòâåòñòâóþò êîððåêòíîìó âçàèìîäåéñòâèþ. Ñîñòîÿíèå ( , )q s ,
äëÿ êîòîðîãî ñóùåñòâóåò � �s s qB A� �( , ( )) òàêîå, ÷òî � �A Bq s( , ( ))�
�, íàçîâåì
êðèòè÷åñêèì.  òàêîì ñîñòîÿíèè âîçìîæíî ïðåêðàùåíèå ñîâìåñòíîé ðàáîòû àâ-
òîìàòîâ A è B. Ïîýòîìó ïîâåäåíèå àâòîìàòà A äîëæíî áûòü îãðàíè÷åíî òàê, ÷òî-
áû åãî êîìïîçèöèÿ ñ àâòîìàòîì B íå ìîãëà ïåðåéòè â êðèòè÷åñêîå ñîñòîÿíèå.
Êàæäîå ñâåðõñëîâî w, äîïóñòèìîå äëÿ êîìïîçèöèè C (ðàññìàòðèâàåìîé êàê
�-àâòîìàò), äîïóñòèìî äëÿ àâòîìàòà A. X Y� -ñâåðõñëîâî, êîòîðîìó â àâòîìàòå C
ñîîòâåòñòâóåò ñâåðõñëîâî ñîñòîÿíèé, ñîäåðæàùåå êðèòè÷åñêîå ñîñòîÿíèå, òàêæå
íàçîâåì êðèòè÷åñêèì. Çàäà÷à ñîãëàñîâàíèÿ àâòîìàòà A ñ àâòîìàòîì B çàêëþ÷àåò-
ñÿ â òîì, ÷òîáû àâòîìàò A çàìåíèòü àâòîìàòîì A * , äëÿ êîòîðîãî W A( )* ñîñòîèò
èç âñåõ ñâåðõñëîâ èç W A( ), íå ÿâëÿþùèõñÿ êðèòè÷åñêèìè. X Y/ -àâòîìàò A ìî-
æåò áûòü ñîãëàñîâàí ñ Y X/ -àâòîìàòîì B òîëüêî òîãäà, êîãäà ïðàâàÿ êîìïîçèöèÿ
C A B
�| èìååò íåïóñòîé öèêëè÷åñêèé ïîäàâòîìàò C ', ëþáîå ñîñòîÿíèå ( , )q s êî-
òîðîãî óäîâëåòâîðÿåò ñëåäóþùåìó óñëîâèþ ñîãëàñîâàííîñòè: äëÿ êàæäîãî
s s qB A' ( , ( ))� � � ñóùåñòâóåò òàêîå q q sA B' ( , ( ' ))� � � , ÷òî ( ' , ' )q s ïðèíàäëåæèò
ìíîæåñòâó ñîñòîÿíèé ïîäàâòîìàòà �C . Ìàêñèìàëüíûé òàêîé öèêëè÷åñêèé ïîäàâ-
òîìàò êîìïîçèöèè C îáîçíà÷èì C * . Çàìåòèì, ÷òî åñëè ñîñòîÿíèå ( , )q s ïðèíàäëå-
æèò öèêëè÷åñêîìó ïîäàâòîìàòó êîìïîçèöèè, òî � �B As q( , ( )) � �, ò.å. ïåðåõîä
â àâòîìàòå B èç ñîñòîÿíèÿ s ïîä äåéñòâèåì ñèãíàëà �A q( ) îïðåäåëåí.
Äàäèì òåïåðü ôîðìàëüíîå îïðåäåëåíèå ñîãëàñîâàííîñòè àâòîìàòà A ñ àâòî-
ìàòîì B.
Îáû÷íî ïðåäñòàâëÿåò èíòåðåñ èíèöèàëüíîå ïîâåäåíèå âçàèìîäåéñòâóþùèõ
àâòîìàòîâ, ò.å. ïîâåäåíèå, îïðåäåëÿåìîå íà÷àëüíûìè ñîñòîÿíèÿìè ýòèõ àâòîìà-
òîâ. Èíèöèàëüíûì ïîäàâòîìàòîì àâòîìàòà A, ïîðîæäåííûì ñîñòîÿíèåì q, íàçû-
âàåòñÿ ìèíèìàëüíûé ïîäàâòîìàò àâòîìàòà A, ñîäåðæàùèé q è âñå äîñòèæèìûå èç
íåãî ñîñòîÿíèÿ. Èíèöèàëüíûé êâàçèöèêëè÷åñêèé ïîäàâòîìàò àâòîìàòà A, ïîðîæ-
äåííûé ñîñòîÿíèåì q (îáîçíà÷àåòñÿ � A q, ), — ýòî ìàêñèìàëüíûé êâàçèöèêëè-
÷åñêèé ïîäàâòîìàò àâòîìàòà, ïîðîæäåííîãî ñîñòîÿíèåì q.
Îïðåäåëåíèå 2. Èíèöèàëüíûé êâàçèöèêëè÷åñêèé X Y/ -àâòîìàò � A q, 0 ñî-
ãëàñîâàí ñ èíèöèàëüíûì êâàçèöèêëè÷åñêèì Y X/ -àâòîìàòîì � B s, 0 òîãäà è òîëü-
êî òîãäà, êîãäà èíèöèàëüíûé êâàçèöèêëè÷åñêèé ïîäàâòîìàò C0 êîìïîçèöèè
A B|� , ïîðîæäåííûé ñîñòîÿíèåì ( , )q s0 0 , íå ïóñò è êàæäîå åãî ñîñòîÿíèå ( , )q s
óäîâëåòâîðÿåò óñëîâèþ ñîãëàñîâàííîñòè.  ýòîì ñëó÷àå ãîâîðèì, ÷òî àâòîìàò A
ñîãëàñîâàí ñ àâòîìàòîì B â ñîñòîÿíèè ( , )q s0 0 êîìïîçèöèè A B|� .
16 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2015, òîì 51, ¹ 5
Çàäà÷à ñîãëàñîâàíèÿ X Y/ -àâòîìàòà A ñ Y X/ -àâòîìàòîì B ñâîäèòñÿ ê íà-
õîæäåíèþ ïîäàâòîìàòà C * êîìïîçèöèè A B|� . Åñëè òàêîé ïîäàâòîìàò íå ïóñò, òî
ðåçóëüòàòîì ñîãëàñîâàíèÿ ÿâëÿåòñÿ àâòîìàò A * ñ ñîñòîÿíèÿìè q si j( ), ñîîòâåòñòâó-
þùèìè ñîñòîÿíèÿì ( , )q si j ïîäàâòîìàòà C * . Îòìåòêà ñîñòîÿíèÿ q si j( ) ðàâíà
�A iq( ), à ôóíêöèÿ ïåðåõîäîâ îïðåäåëÿåòñÿ ñëåäóþùèì îáðàçîì. Èç ñîñòîÿíèÿ
q si j( ) èìååòñÿ ïåðåõîä â ñîñòîÿíèå q sl k( ) ïîä äåéñòâèåì x X� òîãäà è òîëüêî
òîãäà, êîãäà èç ñîñòîÿíèÿ ( , )q si j àâòîìàòà C * åñòü ïåðåõîä â ñîñòîÿíèå ( , )q sl k è
x sB k
� ( ). Àâòîìàò A * ÿâëÿåòñÿ îãðàíè÷åíèåì àâòîìàòà A â òîì ñìûñëå, ÷òî,
âî-ïåðâûõ, íå äëÿ êàæäîãî ñîñòîÿíèÿ q àâòîìàòà A àâòîìàò A * ìîæåò èìåòü ñî-
ñòîÿíèå q s( ) è, âî-âòîðûõ, ìíîæåñòâî ñâåðõñëîâ, äîïóñòèìûõ â ñîñòîÿíèè q s( )
àâòîìàòà A * , ñîäåðæèòñÿ â àíàëîãè÷íîì ìíîæåñòâå äëÿ q, ò.å. W q s W q( ( )) ( )� .
Êàæäîå ñîñòîÿíèå ( , )q s ïîäàâòîìàòà C * êîìïîçèöèè C A B
�
*
| îïðåäåëÿåò
ïàðó âçàèìîäåéñòâóþùèõ èíèöèàëüíûõ êâàçèöèêëè÷åñêèõ àâòîìàòîâ � A q s* , ( )
è � B s, òàêèõ, ÷òî àâòîìàò � A q s* , ( ) ñîãëàñîâàí ñ àâòîìàòîì � B s, . Òàêèì îáðà-
çîì, ìíîæåñòâî QC * ñîñòîÿíèé àâòîìàòà C * — ýòî ìíîæåñòâî âñåõ òåõ ñîñòîÿ-
íèé êîìïîçèöèè A B*
|� , â êîòîðûõ àâòîìàò A * ñîãëàñîâàí ñ àâòîìàòîì B.
Äëÿ îïèñàíèÿ àëãîðèòìà ïîñòðîåíèÿ àâòîìàòà C * â [4] ââåäåíî ïîíÿòèå çàêðûòî-
ãî ñîñòîÿíèÿ ïðàâîé êîìïîçèöèè. Ïðèâåäåì èíäóêòèâíîå îïðåäåëåíèå ýòîãî ïîíÿòèÿ.
Îïðåäåëåíèå 3. Ñîñòîÿíèå ( , )q s ÿäðà ïðàâîé êîìïîçèöèè àâòîìàòîâ A è B
íàçûâàåòñÿ çàêðûòûì, åñëè ñóùåñòâóåò òàêîå � �s s qB A� �( , ( )), ÷òî âûïîëíÿåòñÿ
îäíî èç óñëîâèé: 1) � �A Bq s( , ( ))�
�; 2) äëÿ êàæäîãî � � �q q sA B� �( , ( )) ñîñòîÿ-
íèå ( , )� �q s çàêðûòî.
Âûäåëåíèå ïîäàâòîìàòà C * èç ÿäðà êîìïîçèöèè A B|� ñîñòîèò â èòåðàòèâíîì
ïîñòðîåíèè ìíîæåñòâà âñåõ çàêðûòûõ ñîñòîÿíèé ýòîãî ÿäðà. Ïîñòðîåíèå íà÷èíàåòñÿ
ñ íàõîæäåíèÿ âñåõ çàêðûòûõ ñîñòîÿíèé, óäîâëåòâîðÿþùèõ óñëîâèþ 1. Çàòåì îñóùå-
ñòâëÿåòñÿ ðàñøèðåíèå ýòîãî ìíîæåñòâà íà îñíîâàíèè óñëîâèÿ 2. Åñëè ïîëó÷åííîå
ìíîæåñòâî çàêðûòûõ ñîñòîÿíèé ñîâïàäàåò ñ ìíîæåñòâîì âñåõ ñîñòîÿíèé ÿäðà êîì-
ïîçèöèè, òî àâòîìàò A íåëüçÿ ñîãëàñîâàòü ñ B.  ïðîòèâíîì ñëó÷àå, ïîñëå óäàëåíèÿ
èç ÿäðà êîìïîçèöèè âñåõ çàêðûòûõ ñîñòîÿíèé è âûäåëåíèÿ öèêëè÷åñêîãî ïîäàâòî-
ìàòà, áóäåò ïîëó÷åí àâòîìàò C *, êîòîðîìó ñòàâèòñÿ â ñîîòâåòñòâèå àâòîìàò A * .
Çàìåòèì, ÷òî âìåñòî àâòîìàòà A * ìîæíî èñïîëüçîâàòü ëþáóþ åãî ìèíèìè-
çèðîâàííóþ ôîðìó ïðè ïîäõîäÿùåì äîîïðåäåëåíèè çíà÷åíèé ôóíêöèè ïåðåõî-
äîâ â ÷àñòè÷íûõ ñîñòîÿíèÿõ. Äëÿ ïàð íà÷àëüíûõ ñîñòîÿíèé, îïðåäåëÿåìûõ àâòî-
ìàòîì C * , ñîâìåñòíîå ïîâåäåíèå ñîîòâåòñòâóþùèõ èíèöèàëüíûõ àâòîìàòîâ ñî-
õðàíÿåòñÿ ïðè ëþáîì äîîïðåäåëåíèè àâòîìàòà A * äî âïîëíå îïðåäåëåííîãî.
Äåéñòâèòåëüíî, ïðè ëþáîì äîîïðåäåëåíèè ôóíêöèè ïåðåõîäîâ â ÷àñòè÷íîì ñî-
ñòîÿíèè q s( ) àâòîìàòà A * ìíîæåñòâî âõîäíûõ ñèìâîëîâ, êîòîðûå ìîãóò ïîÿâèòü-
ñÿ íà âõîäå ïîëó÷åííîãî àâòîìàòà A1
* , êîãäà ïðàâàÿ êîìïîçèöèÿ A B1
*
|� íàõîäèò-
ñÿ â ñîñòîÿíèè ( ( ), )q s s , îñòàåòñÿ òàêèì æå, êàê è â êîìïîçèöèè A B*
|� . Òàêèì
îáðàçîì, äîîïðåäåëåíèå íå âëèÿåò íà ïîâåäåíèå êîìïîçèöèè.
Ïðèìåð 1. Ïóñòü X Y/ -àâòîìàò Ìóðà A ïðåäñòàâëåí ñëåäóþùèì ìíî-
æåñòâîì ñòðîê:
( ) :y a x b� .
( ) :y b x b� ,
x a� .
( ) :y c x c� ,
x d� .
( ) :y d x b� ,
x b c� { }, .
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2015, òîì 51, ¹ 5 17
Çäåñü X x x
{ }, , Y y y
{ }, , Q a b c dA
{ }, , , . Ñëåâà îò ñèìâîëà ñîñòîÿíèÿ
â ñêîáêàõ óêàçàíà åãî îòìåòêà. Îïèñàíèå Y X/ -àâòîìàòà B èìååò âèä
( ) : ,x y1 1 2� { },
y � 1.
( ) :x y2 1� ,
y � 1.
Ñîãëàñîâàíèå àâòîìàòà A ñ àâòîìàòîì B íà÷èíàåòñÿ ñ ïîñòðîåíèÿ ïðàâîé
êîìïîçèöèè A B|� , â êîòîðîé âûäåëèì ìàêñèìàëüíûé öèêëè÷åñêèé ïîäàâòîìàò.
Ýòîò àâòîíîìíûé àâòîìàò èìååò ñëåäóþùèé âèä:
( ) ( , ) : ( , )yx a b1 2� .
( ) ( , ) : ( , )yx b a1 1� .
( ) ( , ): ( , )yx b a2 1� .
( ) ( , ): ( , ), ( , )yx c d c1 1 2� { }.
( ) ( , ) : ( , )yx c d2 1� .
( ) ( , ) : ( , ), ( , )yx d b c1 1 1� { }.
Ñîñòîÿíèå ( , )a 1 çàêðûòî â ñèëó óñëîâèÿ 1. Ñîãëàñíî óñëîâèþ 2 çàêðûòûìè
ñòàíîâÿòñÿ ñîñòîÿíèÿ ( , )b 1 è ( , )b 2 . Äðóãèõ çàêðûòûõ ñîñòîÿíèé íåò. Ïîñëå óäàëå-
íèÿ âñåõ çàêðûòûõ ñîñòîÿíèé ïîëó÷èì ïîäàâòîìàò êîìïîçèöèè
( ) ( , ) : ( , ), ( , )yx c d c1 1 2� { }.
( ) ( , ): ( , )yx c d2 1� .
( ) ( , ): ( , )yx d c1 1� .
Ïîñêîëüêó ýòîò ïîäàâòîìàò öèêëè÷åñêèé, îí ñîâïàäàåò ñ àâòîìàòîì C * , êîòî-
ðîìó ñîîòâåòñòâóåò ñëåäóþùèé X Y/ -àâòîìàò Ìóðà A * :
( ) :y c x c1 2� ,
x d� 1.
( ) :y c x d2 1� .
( ) :y d x c1 1� .
Äîîïðåäåëèâ ñîñòîÿíèå c2 ïåðåõîäîì ïîä äåéñòâèåì x â c2 è ìèíèìèçèðî-
âàâ ïîëó÷åííûé àâòîìàò, áóäåì èìåòü àâòîìàò
( ) :y c x c� ,
x d� 1.
( ) :y d x c1 � .
Êîíåö ïðèìåðà.
Ðàññìîòðèì òåïåðü ïîäõîä ê ñîãëàñîâàíèþ àâòîìàòîâ, îñíîâàííûé íà äðó-
ãîì, áîëåå ïðîñòî âû÷èñëÿåìîì âèäå èõ êîìïîçèöèè, êîòîðóþ íàçîâåì ïàðàë-
ëåëüíîé. Ïðè ïîñòðîåíèè ïàðàëëåëüíîé êîìïîçèöèè X Y/ -àâòîìàò A è Y X/ -àâ-
òîìàò B óäîáíî ðàññìàòðèâàòü êàê äåòåðìèíèðîâàííûå �-àâòîìàòû ñ îäíèì è
òåì æå àëôàâèòîì �
�X Y . Ïðè ýòîì äëÿ îáîèõ àâòîìàòîâ îòìåòêè ïåðåõîäîâ
èìåþò âèä xy, ãäå x X� , y Y� .
Îïðåäåëåíèå 4. Ïàðàëëåëüíàÿ êîìïîçèöèÿ �-àâòîìàòîâ A QA A
� �, , � è
B QB B
� �, , � (îáîçíà÷àåòñÿ A B| | ) ïðåäñòàâëÿåò ñîáîé �-àâòîìàò
D QD D
� �, , � , ãäå Q Q QD A B
� . Îáîçíà÷èì �( )q ìíîæåñòâî âñåõ ñèìâîëîâ
� ��, äëÿ êîòîðûõ ïåðåõîä èç ñîñòîÿíèÿ q îïðåäåëåí, òîãäà � � �(( , )) ( ) ( )q s q s
�
è � � � � � �D A Bq s q s(( , ), ) ( ( , ), ( , ))
äëÿ âñåõ � ��(( , ))q s .
Ìàêñèìàëüíûé öèêëè÷åñêèé ïîäàâòîìàò ïàðàëëåëüíîé êîìïîçèöèè �-àâòî-
ìàòîâ A è B íàçîâåì ïàðàëëåëüíîé öèêëè÷åñêîé êîìïîçèöèåé ýòèõ àâòîìàòîâ.
Óòâåðæäåíèå 1. Èç A A~ 1 è B B~ 1 ñëåäóåò ñòðîãàÿ ýêâèâàëåíòíîñòü êîì-
ïîçèöèé D A B
| | è D A B1 1 1
| | .
Äîêàçàòåëüñòâî. Äëÿ ïðîèçâîëüíîãî ñîñòîÿíèÿ ( , )q s îäíîé èç êîìïîçèöèé,
ñêàæåì D, ðàññìîòðèì ñîñòîÿíèå ( , )� �q s êîìïîçèöèè D1 òàêîå, ÷òî q ýêâèâàëåíò-
íî �q , à s ýêâèâàëåíòíî �s . Èç q q~ � è s s~ � ñëåäóåò, ÷òî � �( , ) ( , )q s q s
� � è äëÿ
18 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2015, òîì 51, ¹ 5
êàæäîãî � ��( , )q s âûïîëíÿåòñÿ � � � �A Aq q( , ) ~ ( , )
1
� , � � � �B Bs s( , ) ~ ( , )
1
� . Ïóñòü
� �D q s q s(( , ), ) ( , )
1 1 è � �D q s q s
1 1 1(( , ), ) ( , )� �
� � , òîãäà q q1 1~ � è s s1 1~ � . Îòñþäà
âûòåêàåò, ÷òî êàæäîå ñâåðõñëîâî â àëôàâèòå �, äîïóñòèìîå â ñîñòîÿíèè ( , )q s , äî-
ïóñòèìî â ñîñòîÿíèè ( , )� �q s , è íàîáîðîò, à çíà÷èò, ñîñòîÿíèÿ ( , )q s è ( , )� �q s ýêâè-
âàëåíòíû. Òàêèì îáðàçîì, äëÿ êàæäîãî ñîñòîÿíèÿ êîìïîçèöèè D èìååòñÿ ýêâèâà-
ëåíòíîå åìó ñîñòîÿíèå êîìïîçèöèè D1, è íàîáîðîò, èç ÷åãî ñëåäóåò ñòðîãàÿ ýêâè-
âàëåíòíîñòü ýòèõ àâòîìàòîâ.
Ïðè èññëåäîâàíèè ñîãëàñóåìîñòè àâòîìàòîâ A è B, èñõîäÿ èç ñâîéñòâ ïàðàëëåëüíîé
êîìïîçèöèè, âìåñòî àâòîìàòà B èñïîëüçóåòñÿ åãî òàê íàçûâàåìûé ëåâûé ñäâèã ïî âõîäó [4].
Ëåâûì ñäâèãîì ïî Y Y X� -ñâåðõñëîâà l y x y x y x
( , )( , )( , ) ...1 1 2 2 3 3 íàçû-
âàåòñÿ ñâåðõñëîâî
~
( , )( , )( , ) ...l y x y x y x
2 1 3 2 4 3 Ïîíÿòèå ëåâîãî ñäâèãà ïî Y åñ-
òåñòâåííûì îáðàçîì ðàñïðîñòðàíÿåòñÿ íà ìíîæåñòâà Y X� -ñâåðõñëîâ. Ëåâûì ñäâè-
ãîì ïî Y ìíîæåñòâà Y X� -ñâåðõñëîâ W íàçîâåì ìíîæåñòâî
~ ~
|W l l W
�{ }. Â [4] ïî-
êàçàíî, ÷òî äëÿ âñÿêîãî öèêëè÷åñêîãî Y X/ -àâòîìàòà B Y X QB B B
� , , , ,� � ñó-
ùåñòâóåò òàêîé öèêëè÷åñêèé Y X/ -àâòîìàò
~
B , íàçûâàåìûé ëåâûì ñäâèãîì ïî
âõîäó àâòîìàòà B, ÷òî W B W B(
~
)
~
( )
.  êà÷åñòâå òàêîãî àâòîìàòà èñïîëüçóåòñÿ
Y X/ -àâòîìàò
~
, , , ,~ ~ ~B Y X Q
B B B
� � � , ãäå Q s y s Q y Y s y
B B B~ ( , ) | , , ( , )
� � �{ �
� �}, � � �~ (( , ), ) ( , ) | ( , ), ( , )
B i i B B is y y s y s s y s y1 1 1
� � �{ } , � �~ (( , )) ( )
B Bs y s
.
Äëÿ ñîîòâåòñòâóþùåãî �-àâòîìàòà
~
B ñ âõîäíûì àëôàâèòîì X Y� ôóíêöèÿ ïåðå-
õîäîâ îïðåäåëÿåòñÿ ñëåäóþùèì îáðàçîì: � ~ (( , ), ) ( , )
B
s y x y s y1 1 1 1
òîãäà è òîëüêî
òîãäà, êîãäà s s yB1 � � ( , ), �B s x( )1 1
è �B s y( , )1 1 � �.
Êàê ñëåäóåò èç ýòîãî îïðåäåëåíèÿ, ëåâûé ñäâèã ïî âõîäó êâàçèöèêëè÷åñêîãî
(öèêëè÷åñêîãî) êâàçèäåòåðìèíèðîâàííîãî àâòîìàòà òàêæå ÿâëÿåòñÿ êâàçèöèêëè-
÷åñêèì (öèêëè÷åñêèì) êâàçèäåòåðìèíèðîâàííûì àâòîìàòîì. Óòâåðæäåíèå 1 ïî-
çâîëÿåò ìèíèìèçèðîâàòü àâòîìàò
~
B , ïîëó÷åííûé îïèñàííûì ñïîñîáîì.
Óòâåðæäåíèå 2. Ïóñòü ( , ( , ))� � �q s y — ñîñòîÿíèå ïàðàëëåëüíîé êîìïîçèöèè D
àâòîìàòîâ A è
~
B , äëÿ êîòîðîãî �(( , ( , )))� � � � �q s y , òîãäà ëþáîé ïåðåõîä èç òàêîãî
ñîñòîÿíèÿ îñóùåñòâëÿåòñÿ â ñîñòîÿíèå âèäà ( , ( , ( )))q s qA� .
Äîêàçàòåëüñòâî. Ïóñòü äëÿ �-àâòîìàòà D �D q s y x y q s y(( , ( , )), ) ( , ( , ))� � �
1 1 .
 ñîîòâåòñòâèè ñ îïðåäåëåíèåì ïàðàëëåëüíîé êîìïîçèöèè �-àâòîìàòîâ
�A q x y q( , )�
1 1 , � ~ (( , ), ) ( , )
B
s y x y s y� �
1 1 . Ýòî çíà÷èò, ÷òî äëÿ X Y/ -àâòîìàòà A
�A q y( )
1, à äëÿ Y X/ -àâòîìàòà
~
( , ) (( , ), )~B s y s y y
B
� � �� 1 . Ñîãëàñíî îïðåäåëå-
íèþ ëåâîãî ñäâèãà ïî âõîäó ïðàâàÿ êîìïîíåíòà âñåõ ñîñòîÿíèé, ïðèíàäëåæàùèõ
� ~ (( , ), )
B
s y y� � 1 , ðàâíà y1 è, ñëåäîâàòåëüíî, y y qA
1 � ( ) . Òàêèì îáðàçîì, âñÿ-
êîå ñîñòîÿíèå, â êîòîðîå îñóùåñòâëÿåòñÿ ïåðåõîä â àâòîìàòå D, èìååò âèä
( , ( , ( )))q s qA� . Êîíåö äîêàçàòåëüñòâà.
Îòñþäà ñëåäóåò, ÷òî âñå ñîñòîÿíèÿ ïàðàëëåëüíîé öèêëè÷åñêîé êîìïîçèöèè
èìåþò âèä ( , ( , ( )))q s qA� .
Òåîðåìà 1. Ïðàâàÿ êîìïîçèöèÿ C X Y/ -àâòîìàòà A è Y X/ -àâòîìàòà B è ïà-
ðàëëåëüíàÿ êîìïîçèöèÿ D �-àâòîìàòîâ A è
~
B èìåþò èçîìîðôíûå ÿäðà.
Äîêàçàòåëüñòâî. 1. Ïóñòü � — îòîáðàæåíèå ñîñòîÿíèé ÿäðà àâòîìàòà C
â ñîñòîÿíèÿ àâòîìàòà D, îïðåäåëåííîå ñëåäóþùèì îáðàçîì: �( , )q s
( , ( , ( )))q s qA� . Äëÿ ëþáîãî ñîñòîÿíèÿ ( , )q s ÿäðà àâòîìàòà C � �B As q( , ( )) � �,
â ñèëó ÷åãî ñîñòîÿíèå ( , ( ))s qA� ïðèíàäëåæèò ëåâîìó ñäâèãó ïî âõîäó àâòîìà-
òà B è, ñëåäîâàòåëüíî, ñîñòîÿíèå ( , ( , ( )))q s qA� ïðèíàäëåæèò ïàðàëëåëüíîé êîì-
ïîçèöèè D. Òàêèì îáðàçîì, ýòî îòîáðàæåíèå îïðåäåëåíî äëÿ âñåõ ñîñòîÿíèé ÿäðà
êîìïîçèöèè C. Çäåñü àâòîìàòû B è
~
B ðàññìàòðèâàþòñÿ êàê Y X/ -àâòîìàòû, à àâ-
òîìàò D — êàê �-àâòîìàò. Ïîêàæåì, ÷òî äëÿ �-àâòîìàòîâ C è D èç
�C q s xy q s(( , ), ) ( , )
1 1 , ãäå ñîñòîÿíèÿ ( , )q s è ( , )q s1 1 ïðèíàäëåæàò ÿäðó àâòîìàòà C,
ñëåäóåò � � �D q s xy q s( ( , ), ) ( , )
1 1 , ò.å. � � �D A Aq s q xy q s q(( , ( , ( ))), ) ( , ( , ( )))
1 1 1 .
Ñîãëàñíî îïðåäåëåíèþ ïàðàëëåëüíîé êîìïîçèöèè ýòî ðàâåíñòâî ñîîòâåòñòâóåò
äâóì ðàâåíñòâàì: à) �A q xy q( , )
1; á) � � �~ (( , ( )), ) ( , ( ))
B A As q xy s q
1 1 .
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2015, òîì 51, ¹ 5 19
Êàê ñëåäóåò èç îïðåäåëåíèÿ ïðàâîé êîìïîçèöèè, �C q s xy q s(( , ), ) ( , )
1 1 òîãäà
è òîëüêî òîãäà, êîãäà s s qB A1 � � �( , ( )), �B s x( )1
è �A q xy q( , )
1. Èòàê, ðàâåí-
ñòâî à) âûïîëíÿåòñÿ. Ïîêàæåì òåïåðü ñïðàâåäëèâîñòü ðàâåíñòâà á). Â ñîîòâå-
òñòâèè ñ îïðåäåëåíèåì ëåâîãî ñäâèãà àâòîìàòà ïî âõîäó ýòî ðàâåíñòâî èìååò
ìåñòî òîãäà è òîëüêî òîãäà, êîãäà s s qB A1 � � �( , ( )) , �B s x( )1
è �B s y( , )1 � �.
Îñòàåòñÿ ïîêàçàòü, ÷òî �B s y( , )1 � �. Òàê êàê ( , )q s1 1 ïðèíàäëåæèò ÿäðó àâòîìàòà
C, òî � �B As q( , ( ))1 1 � �, à èç �A q xy q( , )
1 ñëåäóåò �A q y( )1
. Òàêèì îáðàçîì,
íåîáõîäèìûå è äîñòàòî÷íûå óñëîâèÿ âûïîëíåíèÿ ðàâåíñòâà �C q s xy q s(( , ), ) ( , )
1 1
äëÿ ïðàâîé êîìïîçèöèè C è ñîîòâåòñòâóþùåãî ðàâåíñòâà äëÿ ïàðàëëåëüíîé êîì-
ïîçèöèè D ñîâïàäàþò.
2. Ïóñòü � — îòîáðàæåíèå ñîñòîÿíèé ÿäðà àâòîìàòà D â ñîñòîÿíèÿ àâòî-
ìàòà C òàêîå, ÷òî � �( , ( , ( ))) ( , )q s q q sA
. Ïîêàæåì, ÷òî äëÿ �-àâòîìàòîâ C è D èç
� � �D A Aq s q xy q s q(( , ( , ( ))), ) ( , ( , ( )))
1 1 1 , ãäå ( , ( , ( )))q s qA� è ( , ( , ( )))q s qA1 1 1� —
ñîñòîÿíèÿ ÿäðà àâòîìàòà D, ñëåäóåò � � � � �C A Aq s q xy q s q( ( , ( , ( ))), ) ( , ( , ( )))
1 1 1 ,
ò.å. çíà÷åíèå �C q s xy(( , ), ) îïðåäåëåíî è ðàâíî ( , )q s1 1 . Ýòî èìååò ìåñòî òîã-
äà è òîëüêî òîãäà, êîãäà s s qB A1 � � �( , ( )) , �B s x( )1
è �A q xy q( , )
1. Èç
� � �D A Aq s q xy q s q(( , ( , ( ))), ) ( , ( , ( )))
1 1 1 ñëåäóåò �A q xy q( , )
1 è � �~ (( , ( )),
B As q
xy s qA) ( , ( ))
1 1� , ÷òî, â ñâîþ î÷åðåäü, äàåò s s qB A1 � � �( , ( )) è �B s x( )1
. Îòñþäà
âûòåêàåò, ÷òî �C q s xy q s(( , ), ) ( , )
1 1 .
Îòîáðàæåíèÿ � è � èíúåêòèâíû, ïîýòîìó èç ÷àñòè 1 äîêàçàòåëüñòâà ñëåäóåò,
÷òî ÿäðî àâòîìàòà C èçîìîðôíî ïîäìíîæåñòâó ñîñòîÿíèé ÿäðà àâòîìàòà D, à èç
÷àñòè 2 — ÷òî ÿäðî àâòîìàòà D èçîìîðôíî ïîäìíîæåñòâó ñîñòîÿíèé ÿäðà àâòî-
ìàòà C. Òàêèì îáðàçîì, ÿäðà àâòîìàòîâ C è D èçîìîðôíû. Êîíåö äîêàçàòåëüñòâà.
Ñîãëàñíî òåîðåìå 1 äëÿ êàæäîãî öèêëè÷åñêîãî ïîäàâòîìàòà ïðàâîé êîìïî-
çèöèè àâòîìàòîâ A è B ñóùåñòâóåò èçîìîðôíûé åìó ïîäàâòîìàò ïàðàëëåëüíîé
êîìïîçèöèè àâòîìàòîâ A è
~
B , è íàîáîðîò.
Îòìåòèì, ÷òî åñëè ( , ) (( , ( )), )~s y s q y
B A1 � � � , òî â �-àâòîìàòå
~
B ýòîìó óòâåð-
æäåíèþ ñîîòâåòñòâóåò � �~ (( , ( )), ) ( , )
B As q xy s y
1 , ãäå x sB
� ( )1 .
Äëÿ èëëþñòðàöèè òåîðåìû 1 ðàññìîòðèì ïîâåäåíèå ÿäåð ïðàâîé è ïàðàë-
ëåëüíîé êîìïîçèöèé ñîîòâåòñòâåííî â ñîñòîÿíèè ( , )q s è ( , ( , ( )))q s qA� .
Ïðèìåð 2. Ïóñòü ïåðåõîäû èç ñîñòîÿíèÿ q â X Y/ -àâòîìàòå Ìóðà A îïðåäå-
ëåíû ñëåäóþùèì îáðàçîì:
q x q y q y: ( ), ( )1 1 1 2 2� { },
x q y2 3 2� { }( ) ,
x q y q y3 5 1 2 2� { }( ), ( ) ,
à ìíîæåñòâî ñîñòîÿíèé � �B As q( , ( )), â êîòîðûå àâòîìàò B ïåðåõîäèò èç ñî-
ñòîÿíèÿ s ïîä äåéñòâèåì �A q( ), èìååò âèä { }s x s x s x1 1 2 2 3 3( ), ( ), ( ) . Çäåñü
X x x x
{ }1 2 3, , , Y y y y
{ }1 2 3, , è îòìåòêè ñîñòîÿíèé çàïèñàíû â ñêîáêàõ íå-
ïîñðåäñòâåííî ïîñëå ñèìâîëà ñîñòîÿíèÿ.
Ìíîæåñòâî � �~ (( , ( )), )
B
A
y Y
s q y
�
� âñåõ ñîñòîÿíèé, â êîòîðûå èìåþòñÿ ïåðå-
õîäû èç ñîñòîÿíèÿ ( , ( ))s qA� àâòîìàòà
~
B , ïîëó÷àåòñÿ, åñëè âî ìíîæåñòâå
� �B As q Y( , ( ))� óäàëèòü âñå ïàðû ( , )s yi j , äëÿ êîòîðûõ �B i js y( , )
�.
Ïóñòü ýòî ìíîæåñòâî ðàâíî
{( ( ), ), [( ( ), )], ( ( ), )s x y s x y s x y1 1 1 2 2 1 3 3 1 ,
( ( ), ), ( ( ), ), [( ( ), )]s x y s x y s x y1 1 2 2 2 2 3 3 2 ,
[( ( ), )], ( ( ), ), ( ( ), )s x y s x y s x y1 1 3 2 2 3 3 3 3 }.
Çäåñü â êâàäðàòíûå ñêîáêè çàêëþ÷åíû òàêèå ñîñòîÿíèÿ âèäà ( ( ), )s x yi j k , ÷òî
�B i ks y( , )
�. Ïåðåõîäû â ýòè ñîñòîÿíèÿ îòñóòñòâóþò, òàê êàê îíè íå ïðè-
íàäëåæàò àâòîìàòó
~
B . Ñîîòâåòñòâóþùèå ïåðåõîäû â �-àâòîìàòàõ A è
~
B èìåþò
ñëåäóþùèé âèä:
20 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2015, òîì 51, ¹ 5
q x y q: 1 1 1� , ( , ( )): ( , )s q x y s yA� 1 1 1 1� ,
x y q1 2 2� , x y s y3 1 3 1� ( , ) ,
x y q2 2 3� , x y s y1 2 1 2� ( , ) ,
x y q3 1 5� , x y s y2 2 2 2� ( , ) ,
x y q3 2 2� . x y s y2 3 2 3� ( , ) ,
x y s y3 3 3 3� ( , ) .
Ïîñòðîèì âñå ïåðåõîäû èç ñîñòîÿíèÿ ( , ( , ( )))q s qA� ïàðàëëåëüíîé êîìïîçèöèè
A B| |
~
, ðàññìàòðèâàåìîé êàê �-àâòîìàò. Ýòè ïåðåõîäû îïðåäåëåíû äëÿ ñèìâîëîâ àëôàâèòà
X Y� , ïðèíàäëåæàùèõ � �( ) ( , ( )) , , ,q s q x y x y x y x yA�
� { }1 1 1 2 2 2 3 1 , è èìåþò âèä
( , ( , ( ))): ( , ( , ))q s q x y q s yA� 1 1 1 1 1� ,
x y q s y1 2 2 1 2� ( , ( , )) ,
x y q s y2 2 3 2 2� ( , ( , )) ,
x y q s y3 1 5 3 1� ( , ( , )) .
Ìíîæåñòâî ïåðåõîäîâ ïðàâîé êîìïîçèöèè èç ñîñòîÿíèÿ ( , )q s ðàâíî
{( ( ), ( )), ( ( ), ( )), ( ( ), ( )),q y s x q y s x q y s x1 1 1 1 2 2 1 1 3 2 2 2
( ( ), ( )), [( ( ), ( ))]q y s x q y s x5 1 3 3 2 2 3 3 }.
Ñîñòîÿíèå ( ( ), ( ))q y s x2 2 3 3 íå ïðèíàäëåæèò êîìïîçèöèè, ïîñêîëüêó �B s y( , )3 2
�. Äëÿ �-àâòîìàòà C ýòî ïîâåäåíèå â ñîñòîÿíèè ( , )q s îïèñûâàåòñÿ ñëåäóþ-
ùèì îáðàçîì:
( , ): ( , )q s x y q s1 1 1 1� ,
x y q s1 2 2 1� ( , ) ,
x y q s2 2 3 2� ( , ) ,
x y q s3 1 5 3� ( , ) .
Îòñþäà âèäíî, ÷òî îòîáðàæåíèå � �( , ) ( , ( , ( )))q s q s qA
ñîõðàíÿåò ôóíêöèþ ïå-
ðåõîäîâ. Êîíåö ïðèìåðà.
Äëÿ îïèñàíèÿ ïðåäëàãàåìîãî ïîäõîäà ê ñîãëàñîâàíèþ àâòîìàòîâ íà îñíîâå
èõ ïàðàëëåëüíîé êîìïîçèöèè â óñëîâèè �, ïðèíàäëåæàùåì X Y� , âûäåëèì äâå
÷àñòè: ïðîåêöèþ � íà X (îáîçíà÷àåòñÿ Pr X ( )� ) è ïðîåêöèþ � íà Y (PrY ( )� ). Ïî-
íÿòèå ïðîåêöèè ðàñïðîñòðàíèì íà ìíîæåñòâà óñëîâèé.
Óñëîâèå âîçìîæíîñòè ñîãëàñîâàíèÿ X Y/ -àâòîìàòà A ñ Y X/ -àâòîìàòîì B
â òåðìèíàõ èõ ïðàâîé êîìïîçèöèè, ðàññìàòðèâàåìîé êàê �-àâòîìàò, ìîæíî ñôîð-
ìóëèðîâàòü òàêèì îáðàçîì. Àâòîìàò A ìîæåò áûòü ñîãëàñîâàí ñ àâòîìàòîì B
òîãäà è òîëüêî òîãäà, êîãäà ïðàâàÿ êîìïîçèöèÿ àâòîìàòîâ A è B èìååò öèêëè÷åñ-
êèé ïîäàâòîìàò �C , ëþáîå ñîñòîÿíèå ( , )q s êîòîðîãî óäîâëåòâîðÿåò ñëåäóþùåìó
óñëîâèþ: äëÿ êàæäîãî x s s s qB B A� �{ }� � �( )| ( , ( ))1 1 ñóùåñòâóåò òàêîå
q q xA1 � � ( , ), ÷òî ñîñòîÿíèå ( , )q s1 1 ïðèíàäëåæèò ìíîæåñòâó ñîñòîÿíèé àâòî-
ìàòà �C . Íàïîìíèì, ÷òî äëÿ �-àâòîìàòà �C �C q s xy q s�
(( , ), ) ( , )1 1 , åñëè
s s qB A1 � � �( , ( )), �B s x( )1
è q q sA B1 1� � �( , ( )), �A q y( )1
. Ðàññìàòðèâàÿ
êîìïîçèöèþ C êàê �-àâòîìàò è èñïîëüçóÿ ââåäåííîå ïîíÿòèå ïðîåêöèè, ýòî óñëî-
âèå ìîæíî çàïèñàòü â âèäå Pr X C q s( ( , ))'� = { }� � �B B As s s q( )| ( , ( ))1 1 � . Íèæíèé
èíäåêñ ïðè ñèìâîëå � óêàçûâàåò, êàêîìó àâòîìàòó ïðèíàäëåæèò ñîñòîÿíèå ( , )q s .
Ñôîðìóëèðóåì ýòî ñâîéñòâî äëÿ ñîñòîÿíèé ïîäàâòîìàòà ïàðàëëåëüíîé êîìïî-
çèöèè �-àâòîìàòîâ A è
~
B , èçîìîðôíîãî àâòîìàòó �C . Ñîñòîÿíèþ ( , )q s àâòîìàòà �C
ñîîòâåòñòâóåò ñîñòîÿíèå ( , ( , ( )))q s qA� ïàðàëëåëüíîé êîìïîçèöèè D àâòîìàòîâ A
è
~
B òàêîå, ÷òî � �D A Cq s q q s(( , ( , ( )))) (( , ))'�
. Èñõîäÿ èç îïðåäåëåíèÿ ëåâîãî
ñäâèãà àâòîìàòà ïî âõîäó è èç òîãî, ÷òî â ñèëó öèêëè÷íîñòè àâòîìàòà B äëÿ êàæ-
äîãî s QB� ñóùåñòâóåò òàêîé y Y� , ÷òî �B s y( , ) � �, íåñëîæíî ïîêàçàòü, ÷òî äëÿ
àâòîìàòà
~
B Pr { }X B A B B As q s s s q( ( , ( ))) ( )| ( , ( ))~� � � � �
�1 1 . Òåïåðü äëÿ ïàðàë-
ëåëüíîé öèêëè÷åñêîé êîìïîçèöèè âîçìîæíîñòü ñîãëàñîâàíèÿ îõàðàêòåðèçóåì
ñëåäóþùèì îáðàçîì. Àâòîìàò A ìîæåò áûòü ñîãëàñîâàí ñ àâòîìàòîì B òîãäà è
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2015, òîì 51, ¹ 5 21
òîëüêî òîãäà, êîãäà ïàðàëëåëüíàÿ öèêëè÷åñêàÿ êîìïîçèöèÿ �-àâòîìàòîâ A è
~
B
èìååò öèêëè÷åñêèé ïîäàâòîìàò �D , ëþáîå ñîñòîÿíèå ( , ( , ( )))q s qA� êîòîðîãî
óäîâëåòâîðÿåò óñëîâèþ Pr PrX D A X B Aq s q s q( ( , ( , ( )))) ( ( , ( )))' ~� �� �
. Òàêèì îá-
ðàçîì, äëÿ �-àâòîìàòà, ñîîòâåòñòâóþùåãî ïàðàëëåëüíîé öèêëè÷åñêîé êîìïîçè-
öèè D, óñëîâèå ñîãëàñîâàííîñòè âûïîëíÿåòñÿ, åñëè â êàæäîì åãî ñîñòîÿíèè
( , ( , ( )))q s qA� ïðîåêöèÿ íà X ìíîæåñòâà óñëîâèé âñåõ ïåðåõîäîâ èç ýòîãî ñîñòîÿíèÿ
ñîâïàäàåò ñ ïðîåêöèåé íà X ìíîæåñòâà óñëîâèé âñåõ ïåðåõîäîâ â �-àâòîìàòå
~
B èç
ñîñòîÿíèÿ ( , ( ))s qA� . Ýòî óñëîâèå äëÿ ñîñòîÿíèÿ ( , ( , ( )))q s qA� íàçîâåì óñëîâèåì
êîððåêòíîñòè êîìïîçèöèè â ñîñòîÿíèè ( , ( , ( )))q s qA� . Ïàðàëëåëüíàÿ öèêëè÷åñêàÿ
êîìïîçèöèÿ àâòîìàòîâ A è
~
B êîððåêòíà, åñëè îíà êîððåêòíà â êàæäîì ñîñòîÿíèè.
Ïðîöåññ ñîãëàñîâàíèÿ àâòîìàòîâ A è B îñóùåñòâëÿåòñÿ ñëåäóþùèì îáðàçîì.
Ñòðîèòñÿ ïàðàëëåëüíàÿ öèêëè÷åñêàÿ êîìïîçèöèÿ �-àâòîìàòîâ A è
~
B . Çàòåì äëÿ ñî-
ñòîÿíèé ýòîé êîìïîçèöèè ïðîâåðÿåòñÿ óñëîâèå êîððåêòíîñòè. Âñå ñîñòîÿíèÿ êîìïî-
çèöèè, íå óäîâëåòâîðÿþùèå óñëîâèþ êîððåêòíîñòè, óäàëÿþòñÿ.  ïîëó÷åííîì àâòî-
ìàòå ñíîâà âûäåëÿåòñÿ ìàêñèìàëüíûé öèêëè÷åñêèé ïîäàâòîìàò, äëÿ ñîñòîÿíèé êîòî-
ðîãî ïðîâåðÿåòñÿ óñëîâèå êîððåêòíîñòè. Ýòîò ïðîöåññ ïðîäîëæàåòñÿ äî òåõ ïîð,
ïîêà íå áóäåò ïîëó÷åí öèêëè÷åñêèé ïîäàâòîìàò, âñå ñîñòîÿíèÿ êîòîðîãî óäîâëåòâî-
ðÿþò óñëîâèþ êîððåêòíîñòè. Ðåçóëüòàòîì ýòîãî ïðîöåññà ñîãëàñîâàíèÿ ÿâëÿåòñÿ
�-àâòîìàò A * , èçîìîðôíûé ïîëó÷åííîìó ïîäàâòîìàòó ïàðàëëåëüíîé êîìïîçèöèè.
Ïðèìåð 3. Ðàññìîòðèì òå æå àâòîìàòû, ÷òî è â ïðèìåðå 1, äëÿ ñëó÷àÿ, êîãäà
àâòîìàòû A è
~
B ïðåäñòàâëåíû â âèäå �-àâòîìàòîâ:
�-àâòîìàò A èìååò âèä
a xy b: � . d xy b: � ,
b xy a: � , xy b� ,
xy b� . xy c� .
c xy d: � ,
xy c� .
�-àâòîìàò
~
B âûãëÿäèò ñëåäóþùèì îáðàçîì:
( , ): ( , )1 1y xy y� , ( , ): ( , )2 1y xy y� ,
xy y� ( , )2 , xy y� ( , )1 .
xy y� ( , )2 , ( , ): ( , )2 1y xy y� ,
xy y� ( , )1 . xy y� ( , )1 .
( , ): ( , )1 1y xy y� ,
xy y� ( , )1 .
Ïðè ïîñòðîåíèè A B| |
~
ðàññìàòðèâàþòñÿ òàêèå ïàðû ( , ( , ))q s y ñîñòîÿíèé àâòî-
ìàòîâ A è
~
B , äëÿ êîòîðûõ � �( ) ( , )q s y� � �. Íàïîìíèì, åñëè � � �� �( ) ( , )q s y , òî
� � � � � �D q s y q s y(( , ( , )), ) ( ( , ), (( , ), ))
.
Ïðèâåäåì ïàðàëëåëüíóþ öèêëè÷åñêóþ êîìïîçèöèþ, êîòîðàÿ ïîëó÷àåòñÿ èç
ïàðàëëåëüíîé êîìïîçèöèè â ðåçóëüòàòå óäàëåíèÿ âñåõ íåäîñòèæèìûõ ñîñòîÿíèé:
( , ( , )): ( , ( , ))a y xy b y1 2� . ( , ( , )): ( , ( , ))c y xy d y2 1� .
( , ( , )): ( , ( , ))b y xy a y1 1� . ( , ( , )): ( , ( , ))d y xy b y1 1� ,
( , ( , )): ( , ( , ))b y xy a y2 1� . xy c y� ( , ( , ))1 .
( , ( , )): ( , ( , ))c y xy d y1 1� ,
xy c y� ( , ( , ))2 .
Êîìïîçèöèÿ íåêîððåêòíà â ñîñòîÿíèè ( , ( , ))a y1 , ïîñêîëüêó Pr X a y( ( , ( , )))� 1 �
� Pr X y( ( , ))� 1 . Ïîñëå óäàëåíèÿ ýòîãî ñîñòîÿíèÿ ìàêñèìàëüíûé öèêëè÷åñêèé
ïîäàâòîìàò ïîëó÷åííîãî àâòîìàòà ïðèíèìàåò âèä
( , ( , )): ( , ( , ))c y xy d y1 1� ,
xy c y� ( , ( , ))2 .
( , ( , )): ( , ( , ))c y xy d y2 1� .
( , ( , )): ( , ( , ))d y xy c y1 1� .
Ýòîò ïîäàâòîìàò êîìïîçèöèè êîððåêòåí â êàæäîì ñîñòîÿíèè è èçîìîðôåí àâ-
òîìàòó A * , ïîëó÷åííîìó â ïðèìåðå 1 è ðàññìàòðèâàåìîìó êàê �-àâòîìàò.
22 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2015, òîì 51, ¹ 5
Çàìåòèì, ÷òî â ïðèâåäåííîì âûøå àâòîìàòå
~
B ñîñòîÿíèÿ ( , )1 y , ( , )2 y , ( , )2 y
ýêâèâàëåíòíû. Ïîýòîìó â êà÷åñòâå àâòîìàòà
~
B ìîæíî áûëî èñïîëüçîâàòü àâòîìàò
( , ): ( , )1 1y xy y� , ( ): ( , )2 1xy y� ,
xy � ( )2 , xy � ( )2 .
xy � ( )2 ,
xy � ( )2 .
Êîíåö ïðèìåðà.
Åñëè ðàññìàòðèâàåòñÿ êîìïîçèöèÿ èíèöèàëüíûõ àâòîìàòîâ, êîòîðàÿ òàêæå ÿâëÿ-
åòñÿ èíèöèàëüíûì àâòîìàòîì, òî óñëîâèå êîððåêòíîñòè ïðîâåðÿåòñÿ òîëüêî äëÿ òåõ
ñîñòîÿíèé êîìïîçèöèè, êîòîðûå ïðèíàäëåæàò åå èíèöèàëüíîìó öèêëè÷åñêîìó ïîäàâ-
òîìàòó. Åñëè â ïðîöåññå ðàáîòû àëãîðèòìà íà÷àëüíîå ñîñòîÿíèå áóäåò óäàëåíî, òî àë-
ãîðèòì çàêàí÷èâàåò ðàáîòó â ñèëó íåâîçìîæíîñòè ñîãëàñîâàíèÿ èíèöèàëüíûõ àâòîìà-
òîâ. Òàêèì îáðàçîì, ìåòîäû, îñíîâàííûå íà ïîíÿòèè ñîãëàñîâàííîñòè íåèíèöèàëüíûõ
àâòîìàòîâ, ìîãóò ïîòðåáîâàòü çíà÷èòåëüíî áîëüøåãî êîëè÷åñòâà âû÷èñëåíèé, ÷åì
ïðåäëîæåííûé çäåñü ñïîñîá ïðåîáðàçîâàíèÿ èíèöèàëüíîãî àâòîìàòà.
ÏÐÎÁËÅÌÀ ÐÅÀËÈÇÓÅÌÎÑÒÈ È ÑÎÃËÀÑÎÂÀÍÈÅ ÀÂÒÎÌÀÒÎÂ
Êàê îòìå÷àëîñü âî ââåäåíèè, ïðîáëåìà ñîãëàñîâàíèÿ ÿâëÿåòñÿ ÷àñòíûì ñëó÷à-
åì ïðîáëåìû ðåàëèçóåìîñòè ñïåöèôèêàöèè ñèñòåìû. Îáû÷íî ïðîáëåìà ðåàëè-
çóåìîñòè ðåøàåòñÿ îäíîâðåìåííî ñ ïðîáëåìîé ñèíòåçà àâòîìàòà èëè àëãîðèò-
ìà, èñõîäÿ èç ñïåöèôèêàöèè òðåáîâàíèé ê èõ ôóíêöèîíèðîâàíèþ, ñôîðìóëè-
ðîâàííûõ â âèäå óòâåðæäåíèé â ïîäõîäÿùåì ëîãè÷åñêîì ÿçûêå. Äëÿ òîãî
÷òîáû ó÷åñòü òðåáîâàíèÿ ðåàëèçóåìîñòè, Ïíóýëè è Ðîçíåð [6], Àáàäè, Ëýì-
ïîðò è Âîëïåð [7] ïðåäëîæèëè äëÿ ñèíòåçà ðåàêòèâíûõ ñèñòåì èñïîëüçîâàòü
èãðîâûå ìîäåëè, îïèñûâàþùèå áåñêîíå÷íóþ èãðó ìåæäó ñèñòåìîé è ñðåäîé,
ñ êîòîðîé îíà âçàèìîäåéñòâóåò. Ïîñòðîåíèå êîððåêòíîãî àëãîðèòìà ôóíêöèî-
íèðîâàíèÿ ñèñòåìû çàêëþ÷àåòñÿ â íàõîæäåíèè âûèãðûøíîé ñòðàòåãèè â èãðå,
ìîäåëèðóþùåé ñîâìåñòíîå ïîâåäåíèå ýòîé ñèñòåìû è ñðåäû. Âûèãðûøíóþ
ñòðàòåãèþ ìîæíî ïîëó÷èòü òîëüêî çà ñ÷åò îãðàíè÷åíèÿ âîçìîæíîñòè âûáîðà
î÷åðåäíîãî õîäà ñèñòåìû, âûáîð î÷åðåäíîãî õîäà ñðåäû ìîæåò áûòü ëþáûì
â ðàìêàõ åå âîçìîæíîñòåé. Ñïåöèôèêàöèè, äëÿ êîòîðûõ âûèãðûøíûå ñòðàòå-
ãèè ñóùåñòâóþò, íàçûâàþòñÿ ðåàëèçóåìûìè. Ñëîæíîñòü ïîñòðîåíèÿ òàêîé
ñòðàòåãèè çàâèñèò îò âèäà ñâîéñòâ ñèñòåìû, çàäàâàåìûõ ñïåöèôèêàöèåé. Òàê,
åñëè ñïåöèôèêàöèÿ ïðåäñòàâëÿåò ñîáîé ôîðìóëó ÿçûêà LTL, çàäà÷à ïîñòðîå-
íèÿ ñòðàòåãèè ïîëíà â êëàññå 2EXPTIME [6]. Ïîýòîìó äëÿ ïðàêòè÷åñêîãî èñ-
ïîëüçîâàíèÿ èãðîâûõ ìîäåëåé îãðàíè÷èâàþòñÿ áîëåå óçêèìè êëàññàìè
ñâîéñòâ. Äëÿ ïîëó÷åíèÿ ïðèåìëåìîé ñëîæíîñòè ðåøåíèÿ ïðîáëåìû ðåàëèçóå-
ìîñòè îãðàíè÷èâàþò âûðàçèòåëüíûå âîçìîæíîñòè ÿçûêà ñïåöèôèêàöèè è ñîîò-
âåòñòâåííî êëàññ ñâîéñòâ, âûðàçèìûõ â ýòîì ÿçûêå. Òàê, â [8] ðàññìàòðèâàåòñÿ
ôðàãìåíò ÿçûêà LTL, ñîñòîÿùèé èç áóëåâûõ êîìáèíàöèé ôîðìóë âèäà Fp (èëè
Gp), ãäå F (êîãäà-íèáóäü), G (âñåãäà) — òåìïîðàëüíûå îïåðàòîðû, à p — ôîð-
ìóëà, íå ñîäåðæàùàÿ òåìïîðàëüíûõ îïåðàòîðîâ. Ýòî ïîçâîëèëî ïîëó÷èòü àëãî-
ðèòì ïðîâåðêè ðåàëèçóåìîñòè, ïðèíàäëåæàùèé êëàññó PSPACE. Â [9] ðàññìàò-
ðèâàþòñÿ ñïåöèôèêàöèè, ïðåäñòàâèìûå ôîðìóëàìè âèäà (GF GFp p1 2� ��
� �� � � � �GF GF GF GFp q q qm n) ( )1 2 ãäå p qi i, — áóëåâû ôîðìóëû îò àòî-
ìàðíûõ âûñêàçûâàíèé èç ìíîæåñòâà P. Ïîêàçàíî, ÷òî â ýòîì ñëó÷àå ïðîáëåìà
ðåàëèçóåìîñòè ìîæåò áûòü ðåøåíà ñî ñëîæíîñòüþ EXPTIME è êîëè÷åñòâîì
îïåðàöèé O mn P(( ) )| |�2 3 . Â íàñòîÿùåé ðàáîòå ïðåäïîëàãàåòñÿ, ÷òî ñîâìåñòíîå
ïîâåäåíèå ñèñòåìû è ñðåäû õàðàêòåðèçóåòñÿ òîëüêî ñâîéñòâàìè áåçîïàñíîñòè (safety).
Ôîðìàëüíî ñâîéñòâà ðàññìàòðèâàþòñÿ êàê ïîäìíîæåñòâà ìíîæåñòâà âñåõ
ñâåðõñëîâ â àëôàâèòå � , àññîöèèðóåìîì ñî ñïåöèôèêàöèåé. Ìíîæåñòâî ñâåðõ-
ñëîâ S îïðåäåëÿåò ñâîéñòâî áåçîïàñíîñòè òîãäà è òîëüêî òîãäà, êîãäà êàæäîå
ñâåðõñëîâî, íå ïðèíàäëåæàùåå S , èìååò êîíå÷íûé ïðåôèêñ, ëþáîå ïðîäîëæåíèå
êîòîðîãî íå ïðèíàäëåæèò S . Äëÿ ñïåöèôèêàöèè, çàäàþùåé òîëüêî èíâàðèàíòíûå
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2015, òîì 51, ¹ 5 23
ñâîéñòâà áåçîïàñíîñòè, îïðåäåëåíèå åå ðåàëèçóåìîñòè ñâîäèòñÿ ê ñîãëàñîâàíèþ
ñïåöèôèêàöèé ïðîåêòèðóåìîé ñèñòåìû è ñðåäû èëè ñïåöèôèöèðóåìûõ èìè àâòî-
ìàòíûõ ìîäåëåé. Ïîñêîëüêó âûðàçèòåëüíûå âîçìîæíîñòè ñïåöèôèêàöèé îãðàíè-
÷åíû ñâîéñòâàìè, ïðåäñòàâèìûìè �-àâòîìàòàìè, ïðîöåññ ñîãëàñîâàíèÿ ìîæíî
âûïîëíÿòü êàê íà óðîâíå ñïåöèôèêàöèé (÷åìó áóäåò ïîñâÿùåíà âòîðàÿ ÷àñòü
ýòîé ðàáîòû), òàê è íà óðîâíå ñèíòåçèðîâàííûõ àâòîìàòîâ. Ðàçâèâàåìûé çäåñü
ïîäõîä ê ñîãëàñîâàíèþ àâòîìàòîâ õàðàêòåðèçóåòñÿ ñëåäóþùèìè îñîáåííîñòÿìè.
1. Ïðîáëåìû ñîãëàñîâàíèÿ è ñèíòåçà ðàññìàòðèâàþòñÿ íåçàâèñèìî è ìîãóò
ðåøàòüñÿ â ëþáîì ïîðÿäêå.
2. Â áîëüøèíñòâå ðàáîò, ïîñâÿùåííûõ ñèíòåçó ðåàêòèâíûõ ñèñòåì, ïðîáëå-
ìà ðåàëèçóåìîñòè ðàññìàòðèâàåòñÿ áåç êàêîé-ëèáî èíôîðìàöèè î ïîâåäåíèè ñðå-
äû. Ïðåäïîëàãàåòñÿ, ÷òî â ëþáîé ìîìåíò âðåìåíè íà âõîä ñèñòåìû ìîæåò ïîñòó-
ïèòü ëþáîé ñèìâîë âûõîäíîãî àëôàâèòà ñðåäû. Ñëåäîâàòåëüíî, íà ëþáîå âõîä-
íîå ñâåðõñëîâî x ñèñòåìà äîëæíà ðåàãèðîâàòü òàêèì îáðàçîì, ÷òîáû
ñîîòâåòñòâóþùåå âõîä-âûõîäíîå ñâåðõñëîâî (x y, ) óäîâëåòâîðÿëî òðåáîâàíèÿì
ñïåöèôèêàöèè.  äåéñòâèòåëüíîñòè îáû÷íî èìååòñÿ èíôîðìàöèÿ î ïîâåäåíèè
ñðåäû. Ïîýòîìó â íàñòîÿùåé ðàáîòå ñðåäà ðàññìàòðèâàåòñÿ êàê ðåàêòèâíàÿ ñèñòå-
ìà, âçàèìîäåéñòâèå ñ êîòîðîé íà óðîâíå ñïåöèôèêàöèé îïèñûâàåòñÿ êàê èõ
êîíúþíêöèÿ, à íà óðîâíå àâòîìàòîâ — êàê êîìïîçèöèÿ ñîîòâåòñòâóþùèõ àâòî-
ìàòîâ. Òàêîé ïîäõîä õîòÿ è óñëîæíÿåò ðåøåíèå ïðîáëåìû ñèíòåçà, îäíàêî äàåò
áîëåå ðåàëèñòè÷íûå îöåíêè âîçìîæíîñòè ðåàëèçàöèè ñèñòåìû. Òàê, ñïåöèôèêà-
öèÿ, íå ðåàëèçóåìàÿ ïðè òðàäèöèîííîì ïîäõîäå, ìîæåò îêàçàòüñÿ ðåàëèçóåìîé
ïðè ó÷åòå èíôîðìàöèè î ïîâåäåíèè ñðåäû.
Àíàëîãè÷íûé ïîäõîä ðàññìàòðèâàëñÿ â [10] äëÿ ñïåöèôèêàöèé, ïðåäñòàâ-
ëåííûõ â ÿçûêå CTL* è CTL, ãäå ïîêàçàíî, ÷òî ñîîòâåòñòâóþùàÿ ïðîáëåìà ðåà-
ëèçóåìîñòè ïîëíà â êëàññå 3EXPTIME è 2EXPTIME ñîîòâåòñòâåííî. Ñëåäóåò çà-
ìåòèòü, ÷òî ïðîáëåìà ñîãëàñîâàíèÿ àâòîìàòîâ äàæå ñ ó÷åòîì èíôîðìàöèè î ñðå-
äå èìååò ïîëèíîìèàëüíóþ ñëîæíîñòü.
ÇÀÊËÞ×ÅÍÈÅ
Çàäà÷à ñîãëàñîâàíèÿ àâòîìàòîâ èëè èõ ëîãè÷åñêèõ ñïåöèôèêàöèé âîçíèêàåò ïðè
àâòîìàòíîì ïîäõîäå ê ïðîåêòèðîâàíèþ ðåàêòèâíûõ ñèñòåì. Ïðè ýòîì êàê äëÿ
ïðîåêòèðóåìîé ñèñòåìû, òàê è äëÿ ñðåäû, ñ êîòîðîé îíà âçàèìîäåéñòâóåò, èñ-
ïîëüçóþòñÿ àâòîìàòíûå ìîäåëè.  íàñòîÿùåé ðàáîòå â êà÷åñòâå òàêèõ ìîäåëåé
ðàññìàòðèâàþòñÿ ÷àñòè÷íûå íåäåòåðìèíèðîâàííûå àâòîìàòû Ìóðà íàä áåñêîíå÷-
íûìè ñëîâàìè. Ñîãëàñîâàííîñòü àâòîìàòà ñî ñðåäîé ÿâëÿåòñÿ ÷àñòíûì ñëó÷àåì
åãî ðåàëèçóåìîñòè, êîãäà ñâîéñòâà, õàðàêòåðèçóþùèå òðåáóåìîå ïîâåäåíèå àâòî-
ìàòà ïðè åãî âçàèìîäåéñòâèè ñî ñðåäîé, îãðàíè÷èâàþòñÿ èíâàðèàíòíûìè îòíîñè-
òåëüíî äèñêðåòíîãî âðåìåíè ñâîéñòâàìè áåçîïàñíîñòè. Òàêèå ñâîéñòâà ïðåäñòàâè-
ìû ðàññìàòðèâàåìûìè àâòîìàòàìè, ïîýòîìó çàäà÷à ñîãëàñîâàíèÿ ìîæåò ðåøàòü-
ñÿ êàê íà óðîâíå ñïåöèôèêàöèé, òàê è íà óðîâíå ñèíòåçèðîâàííûõ ïî íèì
àâòîìàòîâ. Àâòîìàò, ñèíòåçèðîâàííûé ïî åãî ñïåöèôèêàöèè â ëîãè÷åñêîì ÿçûêå,
âîîáùå ãîâîðÿ, ìîæåò áûòü ÷àñòè÷íûì, ÷òî òðåáóåò åãî ñîãëàñîâàíèÿ ñî ñðåäîé.
Äëÿ îïèñàíèÿ âçàèìîäåéñòâèÿ àâòîìàòîâ èñïîëüçóþòñÿ äâà âèäà êîìïîçè-
öèè: ïðàâàÿ è ïàðàëëåëüíàÿ. Â îáåèõ êîìïîçèöèÿõ ïðåäïîëàãàåòñÿ, ÷òî èçìåíå-
íèÿ ñîñòîÿíèé àâòîìàòîâ ïðîèñõîäÿò â îäèí è òîò æå ìîìåíò äèñêðåòíîãî âðåìå-
íè, îäíàêî â ïðàâîé êîìïîçèöèè â ðåàëüíîì âðåìåíè îíè îñóùåñòâëÿþòñÿ ïîñëå-
äîâàòåëüíî. Â çàâèñèìîñòè îò ðåàëèçàöèè àâòîìàòîâ ïàðàëëåëüíàÿ êîìïîçèöèÿ
ìîæåò îïèñûâàòü èõ âçàèìîäåéñòâèå áåç çàìåíû àâòîìàòà B åãî ëåâûì ñäâèãîì.
Òàê, âçàèìîäåéñòâèå àâòîìàòîâ A è B, ïîñòðîåííûõ íà òðèããåðàõ, ïåðåêëþ÷àþ-
ùèõñÿ ïî ïåðåäíåìó ôðîíòó òàêòèðóþùåãî ñèãíàëà, îïèñûâàåòñÿ ïàðàëëåëüíîé
êîìïîçèöèåé ýòèõ àâòîìàòîâ. Â èãðîâûõ ìîäåëÿõ âçàèìîäåéñòâèÿ àâòîìàòîâ èç-
ìåíåíèÿ èõ ñîñòîÿíèé ïðîèñõîäÿò ïîñëåäîâàòåëüíî â äâóõ ñìåæíûõ òàêòàõ. Ñî-
îòâåòñòâóþùàÿ êîìïîçèöèÿ àâòîìàòîâ ðàññìàòðèâàëàñü â [4], ãäå îíà íàçâàíà
ñèììåòðè÷íîé öèêëè÷åñêîé êîìïîçèöèåé. Ðàçëè÷èÿ â ýòèõ ìîäåëÿõ íå âëèÿþò íà
ìåòîäû è ðåçóëüòàòû ðåøåíèÿ çàäà÷è ñîãëàñîâàíèÿ.
24 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2015, òîì 51, ¹ 5
Îáû÷íî ðàññìàòðèâàåòñÿ âçàèìîäåéñòâèå èíèöèàëüíûõ àâòîìàòîâ, îäíàêî
èìååòñÿ íåñêîëüêî ïðè÷èí, ïî÷åìó íàñòîÿùàÿ ðàáîòà ïîñâÿùåíà â îñíîâíîì âîï-
ðîñàì ñîãëàñîâàíèÿ íåèíèöèàëüíûõ àâòîìàòîâ. Ïðåäëîæåííîå çäåñü ðåøåíèå çà-
äà÷è ñîãëàñîâàíèÿ îðèåíòèðîâàíî íà ìåòîäîëîãèþ ïðîåêòèðîâàíèÿ ðåàêòèâíûõ
àëãîðèòìîâ, â êîòîðîé ñïåöèôèêàöèÿ àâòîìàòíûõ ìîäóëåé èìååò âèä � S , 0 , ãäå
S — ñïåöèôèêàöèÿ íåèíèöèàëüíîãî àâòîìàòà, à 0 — íà÷àëüíîå óñëîâèå, âûäå-
ëÿþùåå â íåì îäíî èëè íåñêîëüêî íà÷àëüíûõ ñîñòîÿíèé. Ìíîãèå çàäà÷è ïðîåê-
òèðîâàíèÿ, â òîì ÷èñëå è ïðîáëåìà ðåàëèçóåìîñòè, ðåøàþòñÿ íà óðîâíå ñïåöè-
ôèêàöèé. Ñîãëàñîâàíèå ñïåöèôèêàöèé îñíîâûâàåòñÿ íà ìåòîäàõ ñîãëàñîâàíèÿ
àâòîìàòîâ, ïîýòîìó íà àâòîìàòíîì óðîâíå ýòó çàäà÷ó åñòåñòâåííî ðàññìàòðèâàòü
äëÿ íåèíèöèàëüíûõ àâòîìàòîâ. Êðîìå òîãî, èìååòñÿ ðÿä çàäà÷, ñâÿçàííûõ ñ ñèí-
òåçîì íåèíèöèàëüíûõ àâòîìàòîâ [11–13], â ÷àñòíîñòè, òàêàÿ çàäà÷à âîçíèêàåò
ïðè êîìïîçèöèîííîì ïîäõîäå ê ïðîåêòèðîâàíèþ ðåàêòèâíûõ àëãîðèòìîâ [14].
 çàêëþ÷åíèå çàìåòèì, ÷òî ñîãëàñîâàíèå àâòîìàòà ñî ñðåäîé èìååò çíà÷åíèå
íå òîëüêî äëÿ îáåñïå÷åíèÿ êîððåêòíîñòè ôóíêöèîíèðîâàíèÿ ñèñòåìû, íî è äëÿ
óâåëè÷åíèÿ âîçìîæíîñòåé îïòèìèçàöèè àâòîìàòà, ïîëó÷åííîãî â ðåçóëüòàòå ñèí-
òåçà. Ïîýòîìó, åñëè äàæå àâòîìàò çàâåäîìî ñîãëàñîâàí ñî ñðåäîé, ïðîöåäóðó ñî-
ãëàñîâàíèÿ èíîãäà öåëåñîîáðàçíî âûïîëíÿòü, ÷òîáû óâåëè÷èòü ÷àñòè÷íîñòü
àâòîìàòà, èñïîëüçóåìóþ ïðè îïòèìèçàöèè.
ÑÏÈÑÎÊ ËÈÒÅÐÀÒÓÐÛ
1. C h u r c h A . Applications of recursive arithmetic to the problem of circuit synthesis // Summaries
of the Summer Inst. for Symbolic Logic. — New York: Cornell Univ., 1957. — P. 3–50.
2. K u p f e r m a n O . Recent challenges and ideas in temporal synthesis // Proc. 38th Conf. on Theory and
Practice of Computer Science (SOFSEM 2012), Lect. Notes Comput. Sci. — 2012. — 7147. — P. 88–98.
3. A l p e r n B . , S c h n e i d e r F . B . Defining liveness // Information Processing Letters. —
1985. — 21, N 4. — P. 181–185.
4. × å á î ò à ð å â À . Í . Âçàèìîäåéñòâèå àâòîìàòîâ // Êèáåðíåòèêà è ñèñòåìíûé àíàëèç. — 1991.
— ¹ 6. — Ñ. 17–29.
5. × å á î ò à ð å â À . Í . Îáùèé ìåòîä ïðîâåðêè ñîãëàñîâàííîñòè âçàèìîäåéñòâóþùèõ àâòîìàòîâ
ñ êîíå÷íîé ïàìÿòüþ // Êèáåðíåòèêà è ñèñòåìíûé àíàëèç. — 1999. — ¹ 6. — Ñ. 25–37.
6. P n u e l i A . , R o s n e r R . On the synthesis of a reactive module // Proc. 16th ACM Symp. on
Principles of Programming Languages. — New York: ACM Press, 1989. — P. 179–190.
7. A b a d i M . , L a m p o r t L . , W o l p e r P . Realizable and unrealizable specifications of reactive
systems // Intern. Colloquium on Automata, Languages, and Programming, Lect. Notes Comput. Sci.
— 1989. — 372. — P. 1–17.
8. A l u r R . , L a T o r r e S . Deterministic generators and games for LTL fragments // ACM Trans.
Computational Logic. — 2004. — 5, N 1. — P. 1–25.
9. P i t e r m a n N . , P n u e l i A . , S a ’ a r Y . Synthesis of Reactive(1) Designs // Proc. Intern. Conf.
on Verification, Model Checking, and Abstract Interpretation, Lect. Notes Comput. Sci. — 2006. —
3855. — P. 364–380.
10. K u p f e r m a n O . , M a d h u s u d a n P . , T h i a g a r a j a n P . S . , V a r d i M . Open systems in
reactive environments: Control and synthesis // Proc. 11th Intern. Conf. on Concurrency Theory.
Lect. Notes Comput. Sci. — 2000. — 1877. — P. 92–107.
11. S i n g h a l V . , P i x l e y C . The verification problem for safe replaceability // Proc. Conf. on
Computer-Aided Verification, Lect. Notes Comput. Sci. — 1994. — 818. — P. 311–323.
12. Q a d e e r S . , B r a y t o n R . K . , S i n g h a l V . , P i x l e y C . Latch redundancy removal
without global reset // Proc. Intern. Conf. on Computer Design. — S.l.: IEEE Computer Society,
1996. — P. 432–439.
13. H e n z i n g e r T . A . , K r i s h n a n S . C . , K u p f e r m a n O . , M a n g F . Y . C . Synthesis of
uninitialized systems // Proc. Intern. Colloquium ICALP 2002, Lect. Notes Comput. Sci. — 2002. —
2380. — P. 644–656.
14. × å á î ò à ð å â À . Í . Êîìïîçèöèîííûé ïîäõîä ê ïðîåêòèðîâàíèþ ðåàêòèâíûõ àëãîðèòìîâ //
Êèáåðíåòèêà è ñèñòåìíûé àíàëèç. — 2013. — ¹ 5. — Ñ. 14–27.
Ïîñòóïèëà 10.12.2014
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2015, òîì 51, ¹ 5 25
|
| id | nasplib_isofts_kiev_ua-123456789-124902 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 0023-1274 |
| language | Russian |
| last_indexed | 2025-12-07T16:08:52Z |
| publishDate | 2015 |
| publisher | Інститут кібернетики ім. В.М. Глушкова НАН України |
| record_format | dspace |
| spelling | Чеботарев, А.Н. 2017-10-11T16:48:45Z 2017-10-11T16:48:45Z 2015 Согласование взаимодействующих автоматов / А.Н. Чеботарев // Кибернетика и системный анализ. — 2015. — Т. 51, № 5. — С. 13-25. — Бібліогр.: 14 назв. — рос. 0023-1274 https://nasplib.isofts.kiev.ua/handle/123456789/124902 519.713.1 Проблема согласования автоматов состоит в том, чтобы спроектировать систему, поведение которой при ее взаимодействии со средой будет удовлетворять заданным требованиям независимо от возможного поведения среды. Приведен ряд теоретических результатов, используемых при решении проблемы согласования, и основанные на них алгоритмы ее решения. Проблема узгодження автоматів полягає в тому, щоб спроектувати систему, поведінка якої при її взаємодії з середовищем буде задовольняти задані вимоги незалежно від можливої поведінки середовища. Наведено низку теоретичних результатів, що використовуються при розв’язанні проблеми узгодження, та алгоритми її розв’язання, які базуються на цих результатах. The problem of automata harmonization is to design a system whose behavior during the interaction with its environment meets given requirements regardless of the environment’s behavior. A number of theoretical results employed in solving the harmonization problem and corresponding algorithms based on these results are presented. ru Інститут кібернетики ім. В.М. Глушкова НАН України Кибернетика и системный анализ Кибернетика Согласование взаимодействующих автоматов Узгодження автоматів, що взаємодіють Harmonization of interacting automata Article published earlier |
| spellingShingle | Согласование взаимодействующих автоматов Чеботарев, А.Н. Кибернетика |
| title | Согласование взаимодействующих автоматов |
| title_alt | Узгодження автоматів, що взаємодіють Harmonization of interacting automata |
| title_full | Согласование взаимодействующих автоматов |
| title_fullStr | Согласование взаимодействующих автоматов |
| title_full_unstemmed | Согласование взаимодействующих автоматов |
| title_short | Согласование взаимодействующих автоматов |
| title_sort | согласование взаимодействующих автоматов |
| topic | Кибернетика |
| topic_facet | Кибернетика |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/124902 |
| work_keys_str_mv | AT čebotarevan soglasovanievzaimodeistvuûŝihavtomatov AT čebotarevan uzgodžennâavtomatívŝovzaêmodíûtʹ AT čebotarevan harmonizationofinteractingautomata |