Использование согласования логических спецификаций автоматов при решении игровых задач
Игровые модели широко используются при решении задач реализуемости, синтеза и верификации реактивных систем. Для решения таких задач в статье рассматривается автоматный подход, основанный на понятии согласованности автоматов или их логических спецификаций. Соответствующие методы существенно отличают...
Gespeichert in:
| Veröffentlicht in: | Кибернетика и системный анализ |
|---|---|
| Datum: | 2014 |
| 1. Verfasser: | |
| Format: | Artikel |
| Sprache: | Russian |
| Veröffentlicht: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2014
|
| Schlagworte: | |
| Online Zugang: | https://nasplib.isofts.kiev.ua/handle/123456789/115815 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Zitieren: | Использование согласования логических спецификаций автоматов при решении игровых задач / А.Н. Чеботарев // Кибернетика и системный анализ. — 2014. — Т. 50, № 4. — С. 3-13. — Бібліогр.: 12 назв. — рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
nasplib_isofts_kiev_ua-123456789-115815 |
|---|---|
| record_format |
dspace |
| spelling |
Чеботарев, А.Н. 2017-04-13T19:06:12Z 2017-04-13T19:06:12Z 2014 Использование согласования логических спецификаций автоматов при решении игровых задач / А.Н. Чеботарев // Кибернетика и системный анализ. — 2014. — Т. 50, № 4. — С. 3-13. — Бібліогр.: 12 назв. — рос. https://nasplib.isofts.kiev.ua/handle/123456789/115815 519.713.1 Игровые модели широко используются при решении задач реализуемости, синтеза и верификации реактивных систем. Для решения таких задач в статье рассматривается автоматный подход, основанный на понятии согласованности автоматов или их логических спецификаций. Соответствующие методы существенно отличаются от тех, которые используются в игровом контексте. Показано, как эти методы можно применять для синтеза выигрышной стратегии в игре двух лиц, не связанной с проектированием реактивных систем. Ігрові моделі широко використовуються при розв’язанні задач реалізовності, синтезу та верифікації реактивних систем. Для розв’язання таких задач у статті розглянуто автоматний підхід, який базується на понятті узгодженості автоматів або їхніх логічних специфікацій. Відповідні методи суттєво відрізняються від тих, що застосовуються в ігровому контексті. Показано, як ці методи можуть використовуватися для синтезу виграшної стратегії у грі двох осіб, не пов’язаній з проектуванням реактивних систем. Game models have been widely used to solve realizability, synthesis, and verification problems. In this paper, we consider an alternative approach to solving these problems based on the notion of compatibility of automata (FSMs) or their logical specifications. The corresponding methods substantially differ from those used in the game setting. We show how these methods can be used for the synthesis of a winning strategy in a two-player game, which does not relate to the development of reactive systems. ru Інститут кібернетики ім. В.М. Глушкова НАН України Кибернетика и системный анализ Кибернетика Использование согласования логических спецификаций автоматов при решении игровых задач Використання узгодження логічних специфікацій автоматів при розв’язанні ігрових задач Using the compatibility analysis of automata logical specification to solve game problems Article published earlier |
| institution |
Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| collection |
DSpace DC |
| title |
Использование согласования логических спецификаций автоматов при решении игровых задач |
| spellingShingle |
Использование согласования логических спецификаций автоматов при решении игровых задач Чеботарев, А.Н. Кибернетика |
| title_short |
Использование согласования логических спецификаций автоматов при решении игровых задач |
| title_full |
Использование согласования логических спецификаций автоматов при решении игровых задач |
| title_fullStr |
Использование согласования логических спецификаций автоматов при решении игровых задач |
| title_full_unstemmed |
Использование согласования логических спецификаций автоматов при решении игровых задач |
| title_sort |
использование согласования логических спецификаций автоматов при решении игровых задач |
| author |
Чеботарев, А.Н. |
| author_facet |
Чеботарев, А.Н. |
| topic |
Кибернетика |
| topic_facet |
Кибернетика |
| publishDate |
2014 |
| language |
Russian |
| container_title |
Кибернетика и системный анализ |
| publisher |
Інститут кібернетики ім. В.М. Глушкова НАН України |
| format |
Article |
| title_alt |
Використання узгодження логічних специфікацій автоматів при розв’язанні ігрових задач Using the compatibility analysis of automata logical specification to solve game problems |
| description |
Игровые модели широко используются при решении задач реализуемости, синтеза и верификации реактивных систем. Для решения таких задач в статье рассматривается автоматный подход, основанный на понятии согласованности автоматов или их логических спецификаций. Соответствующие методы существенно отличаются от тех, которые используются в игровом контексте. Показано, как эти методы можно применять для синтеза выигрышной стратегии в игре двух лиц, не связанной с проектированием реактивных систем.
Ігрові моделі широко використовуються при розв’язанні задач реалізовності, синтезу та верифікації реактивних систем. Для розв’язання таких задач у статті розглянуто автоматний підхід, який базується на понятті узгодженості автоматів або їхніх логічних специфікацій. Відповідні методи суттєво відрізняються від тих, що застосовуються в ігровому контексті. Показано, як ці методи можуть використовуватися для синтезу виграшної стратегії у грі двох осіб, не пов’язаній з проектуванням реактивних систем.
Game models have been widely used to solve realizability, synthesis, and verification problems. In this paper, we consider an alternative approach to solving these problems based on the notion of compatibility of automata (FSMs) or their logical specifications. The corresponding methods substantially differ from those used in the game setting. We show how these methods can be used for the synthesis of a winning strategy in a two-player game, which does not relate to the development of reactive systems.
|
| url |
https://nasplib.isofts.kiev.ua/handle/123456789/115815 |
| citation_txt |
Использование согласования логических спецификаций автоматов при решении игровых задач / А.Н. Чеботарев // Кибернетика и системный анализ. — 2014. — Т. 50, № 4. — С. 3-13. — Бібліогр.: 12 назв. — рос. |
| work_keys_str_mv |
AT čebotarevan ispolʹzovaniesoglasovaniâlogičeskihspecifikaciiavtomatovprirešeniiigrovyhzadač AT čebotarevan vikoristannâuzgodžennâlogíčnihspecifíkacíiavtomatívprirozvâzanníígrovihzadač AT čebotarevan usingthecompatibilityanalysisofautomatalogicalspecificationtosolvegameproblems |
| first_indexed |
2025-11-26T21:22:50Z |
| last_indexed |
2025-11-26T21:22:50Z |
| _version_ |
1850776674277261312 |
| fulltext |
À.Í. ×ÅÁÎÒÀÐÅÂ
ÓÄÊ 519.713.1 ÈÑÏÎËÜÇÎÂÀÍÈÅ ÑÎÃËÀÑÎÂÀÍÈß
ËÎÃÈ×ÅÑÊÈÕ ÑÏÅÖÈÔÈÊÀÖÈÉ ÀÂÒÎÌÀÒÎÂ
ÏÐÈ ÐÅØÅÍÈÈ ÈÃÐÎÂÛÕ ÇÀÄÀ×
Àííîòàöèÿ. Èãðîâûå ìîäåëè øèðîêî èñïîëüçóþòñÿ ïðè ðåøåíèè çàäà÷ ðåàëèçóåìîñòè,
ñèíòåçà è âåðèôèêàöèè ðåàêòèâíûõ ñèñòåì. Äëÿ ðåøåíèÿ òàêèõ çàäà÷ â ñòàòüå ðàññìàòðè-
âàåòñÿ àâòîìàòíûé ïîäõîä, îñíîâàííûé íà ïîíÿòèè ñîãëàñîâàííîñòè àâòîìàòîâ èëè èõ
ëîãè÷åñêèõ ñïåöèôèêàöèé. Ñîîòâåòñòâóþùèå ìåòîäû ñóùåñòâåííî îòëè÷àþòñÿ îò òåõ, êî-
òîðûå èñïîëüçóþòñÿ â èãðîâîì êîíòåêñòå. Ïîêàçàíî, êàê ýòè ìåòîäû ìîæíî ïðèìåíÿòü
äëÿ ñèíòåçà âûèãðûøíîé ñòðàòåãèè â èãðå äâóõ ëèö, íå ñâÿçàííîé ñ ïðîåêòèðîâàíèåì
ðåàêòèâíûõ ñèñòåì.
Êëþ÷åâûå ñëîâà: ÿçûê ñïåöèôèêàöèè L, ñîãëàñîâàíèå àâòîìàòîâ, ñèíòåç àâòîìàòà, ìî-
äåëü èãðû, âûèãðûøíàÿ ñòðàòåãèÿ.
ÂÂÅÄÅÍÈÅ
Èãðîâûå ìîäåëè øèðîêî èñïîëüçóþòñÿ ïðè ðåøåíèè çàäà÷ ðåàëèçóåìîñòè,
ñèíòåçà è âåðèôèêàöèè îòêðûòûõ ñèñòåì, ò.å. ñèñòåì, âçàèìîäåéñòâóþùèõ ñî
ñâîèì îêðóæåíèåì.  ýòèõ çàäà÷àõ ñïåöèôèêàöèÿ òðåáîâàíèé ê ïîâåäåíèþ
ñèñòåìû, âçàèìîäåéñòâóþùåé ñî ñðåäîé, âûðàæàåòñÿ â êàêîì-ëèáî ëîãè÷åñêîì
ÿçûêå, òàêîì êàê ðàçëè÷íîãî ðîäà òåìïîðàëüíûå ëîãèêè, ëîãèêè ïåðâîãî ïî-
ðÿäêà èëè îãðàíè÷åííûå ëîãèêè âòîðîãî ïîðÿäêà. Âàæíîé îñîáåííîñòüþ îò-
êðûòîé ñèñòåìû ÿâëÿåòñÿ òî, ÷òî â ïðîöåññå åå ïðîåêòèðîâàíèÿ íèêàêèå îãðà-
íè÷åíèÿ íà ïîâåäåíèå ñðåäû, êðîìå îïðåäåëÿåìûõ åå ñïåöèôèêàöèåé, íå äîë-
æíû íàëàãàòüñÿ. Ñïåöèôèêàöèÿ îòêðûòîé ñèñòåìû ïðåäïîëàãàåòñÿ òàêîé, ÷òî
âñå òðåáîâàíèÿ ê ïîâåäåíèþ ñèñòåìû ïðè åå âçàèìîäåéñòâèè ñî ñðåäîé âû-
ïîëíÿþòñÿ ïðè ëþáîì äîïóñòèìîì ïîâåäåíèè ñðåäû.
Èñïîëüçîâàíèå äëÿ ñèíòåçà îòêðûòûõ (ðåàêòèâíûõ) ñèñòåì ìîäåëåé, îïèñû-
âàþùèõ èãðó ìåæäó ñèñòåìîé è ñðåäîé, ñ êîòîðîé îíà âçàèìîäåéñòâóåò, áûëî
ïðåäëîæåíî â ðàáîòàõ Ïíóýëè è Ðîçíåðà [1], Àáàäè, Ëýìïîðòà è Âîëïåðà [2],
Äèëëà [3]. Êàê ïðàâèëî, òàêèå ìîäåëè îïðåäåëÿþòñÿ äâóäîëüíûì ãðàôîì è óñëî-
âèåì âûèãðûøà. Âåðøèíû ãðàôà (ñîñòîÿíèÿ) ðàçáèòû íà äâà ìíîæåñòâà, êàæäîå
èç êîòîðûõ ñîîòâåòñòâóåò îäíîìó èç èãðîêîâ, à óñëîâèå âûèãðûøà â îáùåì ñëó-
÷àå çàäàåò íåêîòîðîå ìíîæåñòâî áåñêîíå÷íûõ ïîñëåäîâàòåëüíîñòåé ñîñòîÿíèé,
ïîðîæäàåìûõ ïîî÷åðåäíûìè õîäàìè èãðîêîâ. Èãðû íà êîíå÷íûõ ãðàôàõ ðàñ-
ñìàòðèâàëèñü â òàêèõ çàäà÷àõ ïðîåêòèðîâàíèÿ ðåàêòèâíûõ ñèñòåì, êàê ñèíòåç
êîíòðîëëåðà [4], âåðèôèêàöèÿ ïðîòîêîëîâ [5], êîìïîçèöèîííîå ïðîåêòèðîâàíèå,
âåðèôèêàöèÿ [6] è äð. Ïîñòðîåíèå êîððåêòíîãî àëãîðèòìà ôóíêöèîíèðîâàíèÿ
ñèñòåìû çàêëþ÷àåòñÿ â íàõîæäåíèè âûèãðûøíîé ñòðàòåãèè â èãðå, ìîäåëèðóþ-
ùåé ýòó ñèñòåìó. Òàêóþ ñòðàòåãèþ ìîæíî ïîëó÷èòü òîëüêî çà ñ÷åò îãðàíè÷åíèÿ
âûáîðà î÷åðåäíîãî õîäà ñèñòåìû. Âûáîð î÷åðåäíîãî õîäà ñðåäû ìîæåò áûòü ëþ-
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2014, òîì 50, ¹ 4 3
© À.Í. ×åáîòàðåâ, 2014
áûì â ðàìêàõ åå âîçìîæíîñòåé. Ñïåöèôèêàöèè, äëÿ êîòîðûõ âûèãðûøíûå ñòðà-
òåãèè ñóùåñòâóþò, íàçûâàþòñÿ ðåàëèçóåìûìè. Ñëîæíîñòü ïîñòðîåíèÿ òàêîé
ñòðàòåãèè çàâèñèò îò ñïîñîáà çàäàíèÿ óñëîâèÿ âûèãðûøà è, ñëåäîâàòåëüíî, îò õà-
ðàêòåðà ñâîéñòâ ñèñòåìû, çàäàâàåìûõ ýòèì óñëîâèåì. Òàê, ïðè çàäàíèè óñëîâèÿ
LTL ôîðìóëîé çàäà÷à ïîñòðîåíèÿ ñòðàòåãèè ïîëíà â êëàññå 2EXPTIME [1]. Ïîý-
òîìó äëÿ ïðàêòè÷åñêîãî ïðèìåíåíèÿ èãðîâûõ ìîäåëåé îãðàíè÷èâàþòñÿ áîëåå
óçêèìè êëàññàìè ñâîéñòâ. Â íàñòîÿùåé ðàáîòå äëÿ ñïåöèôèêàöèè èãðîâûõ ìîäå-
ëåé èñïîëüçóåòñÿ ëîãè÷åñêèé ÿçûê L [7], ôîðìóëû êîòîðîãî çàäàþò ñâîéñòâà áå-
çîïàñíîñòè (safety). Ôîðìàëüíî ñâîéñòâà ðàññìàòðèâàþòñÿ êàê ïîäìíîæåñòâà
ìíîæåñòâà �� âñåõ áåñêîíå÷íûõ ñëîâ (ñâåðõñëîâ) â íåêîòîðîì àëôàâèòå � . Ìíî-
æåñòâî S � �� îïðåäåëÿåò ñâîéñòâî áåçîïàñíîñòè òîãäà è òîëüêî òîãäà, êîãäà
êàæäîå ñâåðõñëîâî, íå ïðèíàäëåæàùåå S , èìååò ïðåôèêñ, ëþáîå ïðîäîëæåíèå
êîòîðîãî íå ïðèíàäëåæèò S . Äëÿ ñïåöèôèêàöèè, çàäàþùåé òîëüêî ñâîéñòâà áåçî-
ïàñíîñòè, ïðîâåðêà åå ðåàëèçóåìîñòè ñâîäèòñÿ ê òàêîìó ïðåîáðàçîâàíèþ, â ðå-
çóëüòàòå êîòîðîãî (åñëè ýòî âîçìîæíî) ïîëó÷àåòñÿ ñïåöèôèêàöèÿ, íå îãðàíè÷è-
âàþùàÿ ïîâåäåíèå ñðåäû.  [8, 9] ýòà çàäà÷à ôîðìàëèçóåòñÿ â òåðìèíàõ ñîãëàñî-
âàíèÿ ñïåöèôèêàöèè ñèñòåìû ñî ñïåöèôèêàöèåé ñðåäû. Ìåòîäû åå ðåøåíèÿ,
ïðåäëîæåííûå â [8, 9] êàê íà óðîâíå ñïåöèôèêàöèé, òàê è íà óðîâíå
ñîîòâåòñòâóþùèõ àâòîìàòîâ, ñóùåñòâåííî îòëè÷àþòñÿ îò ñîâðåìåííûõ ìåòîäîâ
ðåøåíèÿ èãðîâûõ çàäà÷. Â íàñòîÿùåé ñòàòüå ïîêàçàíî, ÷òî ìåòîäû ïðîåêòèðîâà-
íèÿ ðåàêòèâíûõ àëãîðèòìîâ, îñíîâàííûå íà ñîãëàñîâàíèè ñïåöèôèêàöèé, ìîãóò
èñïîëüçîâàòüñÿ äëÿ ðåøåíèÿ èãðîâûõ çàäà÷, íå ñâÿçàííûõ ñ òàêèì ïðîåêòèðîâà-
íèåì. Íà ïðîñòîì, íî äîñòàòî÷íî èëëþñòðàòèâíîì, ïðèìåðå èãðû ÍÈÌ ïîêàçû-
âàåòñÿ ñïåöèôèêà èñïîëüçîâàíèÿ ýòèõ ìåòîäîâ äëÿ ïîñòðîåíèÿ âûèãðûøíîé
ñòðàòåãèè â èãðå äâóõ ëèö ñ íóëåâîé ñóììîé.
ÑÈÍÒÀÊÑÈÑ È ÑÅÌÀÍÒÈÊÀ ßÇÛÊÀ L
ßçûê L [7] ïðåäñòàâëÿåò ñîáîé ôðàãìåíò ëîãèêè ïðåäèêàòîâ ïåðâîãî ïîðÿäêà
ñ îäíîìåñòíûìè ïðåäèêàòàìè è ôèêñèðîâàííîé îáëàñòüþ èíòåðïðåòàöèè, â êà-
÷åñòâå êîòîðîé âûñòóïàåò ìíîæåñòâî Z öåëûõ ÷èñåë (ìîìåíòîâ âðåìåíè). Ñïå-
öèôèêàöèÿ â ÿçûêå L èìååò âèä ôîðìóëû �tF t( ) . Çäåñü F t( ) — ôîðìóëà, ïî-
ñòðîåííàÿ ñ ïîìîùüþ ëîãè÷åñêèõ ñâÿçîê èç àòîìàðíûõ ôîðìóë (àòîìîâ) âèäà
p t k( )� , ãäå p — îäíîìåñòíûé ïðåäèêàòíûé ñèìâîë, t — ïåðåìåííàÿ, ïðèíè-
ìàþùàÿ çíà÷åíèÿ èç ìíîæåñòâà öåëûõ ÷èñåë, k — öåëîå ÷èñëî, íàçûâàåìîå
ðàíãîì àòîìà. Ðàçíîñòü ìåæäó ìàêñèìàëüíûì è ìèíèìàëüíûì çíà÷åíèÿìè
ðàíãîâ àòîìîâ, âñòðå÷àþùèõñÿ â ôîðìóëå, íàçûâàåòñÿ ãëóáèíîé ôîðìóëû.
Ïóñòü � � { , , , }p p pm1 2 � — ìíîæåñòâî âñåõ ïðåäèêàòíûõ ñèìâîëîâ ôîðìó-
ëû F t( ) . Ïðè îïðåäåëåíèè ñåìàíòèêè ÿçûêà L îí ðàññìàòðèâàåòñÿ êàê ôîðìàëèçì
äëÿ çàäàíèÿ ìíîæåñòâà ñâåðõñëîâ (áåñêîíå÷íûõ ñëîâ) â àëôàâèòå äâîè÷íûõ âåêòî-
ðîâ, äëèíà êîòîðûõ ðàâíà ìîùíîñòè ìíîæåñòâà �. Îáû÷íî ñèìâîëû òàêîãî àëôàâè-
òà ðàññìàòðèâàþòñÿ êàê îòîáðàæåíèÿ âèäà �: { , }� � 0 1 . Òàê êàê ýòîò àëôàâèò îäíî-
çíà÷íî îïðåäåëÿåòñÿ ìíîæåñòâîì ïðåäèêàòíûõ ñèìâîëîâ � , îáîçíà÷èì åãî � �( ) .
Ïóñòü � — êîíå÷íûé àëôàâèò, Z — ìíîæåñòâî öåëûõ ÷èñåë,
N Z� �
z z| 0 . Îòîáðàæåíèÿ u: Z � � è l: N� � � íàçûâàþòñÿ ñîîòâåòñòâåííî
äâóñòîðîííèì ñâåðõñëîâîì (îáîçíà÷àåòñÿ � �u u u u u( ) ( ) ( ) ( ) ( )� �2 1 0 1 2 ) è ñâåðõ-
ñëîâîì (îáîçíà÷àåòñÿ l l( ) ( )1 2 � ) â àëôàâèòå � . Áåñêîíå÷íûé îòðåçîê u k( , )� �1
äâóñòîðîííåãî ñâåðõñëîâà u íàçîâåì k-ñóôôèêñîì ýòîãî ñâåðõñëîâà.
Îïèøåì ñåìàíòèêó ÿçûêà L. Ôîðìóëû ÿçûêà L èíòåðïðåòèðóþòñÿ íà ìíî-
æåñòâå öåëûõ ÷èñåë.  ñèëó ýòîãî, êàê ïîêàçàíî â [7], ìîæíî îãðàíè÷èòüñÿ ðàñ-
ñìîòðåíèåì ôîðìóë, ó êîòîðûõ ìàêñèìàëüíûé ðàíã àòîìîâ ðàâåí 0. Êàæäîé ôîð-
4 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2014, òîì 50, ¹ 4
ìóëå F tF t� � ( ) ñòàâèòñÿ â ñîîòâåòñòâèå ìíîæåñòâî ìîäåëåé äëÿ ýòîé ôîðìóëû,
ò.å. ìíîæåñòâî òàêèõ èíòåðïðåòàöèé, íà êîòîðûõ F èñòèííà. Ïóñòü
� � { , , , }p p pm1 2 � — ìíîæåñòâî âñåõ ïðåäèêàòíûõ ñèìâîëîâ, èìåþùèõñÿ
â ôîðìóëå F (ñèãíàòóðà ôîðìóëû). Èíòåðïðåòàöèÿ ôîðìóëû F — ýòî óïîðÿäî-
÷åííûé íàáîð îïðåäåëåííûõ íà Z îäíîìåñòíûõ ïðåäèêàòîâ � �1, ,� m , ñîîòâåò-
ñòâóþùèõ ïðåäèêàòíûì ñèìâîëàì èç � . Èíòåðïðåòàöèþ I m�
�� �1, ,� ìîæíî
ïðåäñòàâèòü â âèäå äâóñòîðîííåãî ñâåðõñëîâà â àëôàâèòå � �( ) , à ìíîæåñòâî
âñåõ ìîäåëåé äëÿ F — â âèäå ìíîæåñòâà M F( ) äâóñòîðîííèõ ñâåðõñëîâ â ýòîì
àëôàâèòå. Åñëè íå ðàçëè÷àòü èíòåðïðåòàöèè è ñîîòâåòñòâóþùèå èì äâóñòîðîí-
íèå ñâåðõñëîâà, òî ìîæíî ãîâîðèòü îá èñòèííîñòè ôîðìóëû F íà äâóñòîðîííåì
ñâåðõñëîâå u è çíà÷åíèè ôîðìóëû F t( ) â íåêîòîðîé òî÷êå � äâóñòîðîííåãî ñâåðõ-
ñëîâà u . Ñìûñë ïîíÿòèÿ ãëóáèíû ôîðìóëû ñîñòîèò â òîì, ÷òî èñòèííîñòíîå çíà-
÷åíèå ôîðìóëû F t( ) ãëóáèíû r â òî÷êå � èíòåðïðåòàöèè u îïðåäåëÿåòñÿ îòðåçêîì
u r( , )� �� ñîîòâåòñòâóþùåãî äâóñòîðîííåãî ñâåðõñëîâà u .
Áóäåì ñ÷èòàòü, ÷òî ôîðìóëà F tF t� � ( ) çàäàåò ìíîæåñòâî 0-ñóôôèêñîâ âñåõ
äâóñòîðîííèõ ñâåðõñëîâ èç M F( ) . Îáîçíà÷èì ýòî ìíîæåñòâî ñâåðõñëîâ W F( ).
Îïðåäåëèì àâòîìàòíóþ ñåìàíòèêó ÿçûêà L.
Îïðåäåëåíèå 1. Êîíå÷íûé X Y� -àâòîìàò Ìóðà A — ýòî ïÿòåðêà
�X Y Q A A, , , ,� � , ãäå X è Y — ñîîòâåòñòâåííî âõîäíîé è âûõîäíîé àëôàâèòû,
Q — êîíå÷íîå ìíîæåñòâî ñîñòîÿíèé, à �A
QQ X: � � 2 è �A Q Y: � — ôóíê-
öèè ñîîòâåòñòâåííî ïåðåõîäîâ è âûõîäîâ. Àâòîìàò A íàçûâàåòñÿ äåòåðìèíèðî-
âàííûì, åñëè äëÿ ëþáûõ x X q Q , | ( , )|�A q x � 1, â ïðîòèâíîì ñëó÷àå îí íàçû-
âàåòñÿ íåäåòåðìèíèðîâàííûì.
Îïðåäåëåíèå 2. X Y� -àâòîìàò A X Y Q A A�
�, , , ,� � íàçûâàåòñÿ êâàçèäå-
òåðìèíèðîâàííûì, åñëè äëÿ ëþáûõ x X q Q , èç q q q xA1 2, ( , ) � ñëåäóåò
� �( ) ( )q q1 2� .
Êâàçèäåòåðìèíèðîâàííûé X Y� -àâòîìàò óäîáíî ðàññìàòðèâàòü êàê äåòåð-
ìèíèðîâàííûé ÷àñòè÷íûé àâòîìàò áåç âûõîäîâ ñ âõîäíûì àëôàâèòîì � � �X Y .
Òàêîé àâòîìàò A Q A�
��, , � , ãäå �A Q Q: � �� — ÷àñòè÷íàÿ ôóíêöèÿ ïåðåõî-
äîâ, íàçîâåì �-àâòîìàòîì.
Îïðåäåëåíèå 3. �-àâòîìàò A Q A�
��, , � íàçûâàåòñÿ öèêëè÷åñêèì, åñëè äëÿ
êàæäîãî q Q ñóùåñòâóþò òàêèå � �1 2, � è q q Q1 2, , ÷òî q qA1 1� � �( , ) è
q qA� � �( , )2 2 .
Öèêëè÷åñêèé �-àâòîìàò ìîæíî îõàðàêòåðèçîâàòü â òåðìèíàõ äîïóñòèìûõ
ñâåðõñëîâ.
Îïðåäåëåíèå 4. Ñâåðõñëîâî l � � �1 2� äîïóñòèìî â ñîñòîÿíèè q �-àâòîìàòà A ,
åñëè ñóùåñòâóåò òàêîå ñâåðõñëîâî ñîñòîÿíèé q q q0 1 2� , ãäå q q0 � , ÷òî äëÿ ëþ-
áîãî i = 0, 1, 2,… q qi A i i� ��1 1� �( , ) . Ñâåðõñëîâî l äîïóñòèìî äëÿ àâòîìàòà A ,
åñëè îíî äîïóñòèìî õîòÿ áû â îäíîì èç åãî ñîñòîÿíèé.
Îáîçíà÷èì W A( ) ìíîæåñòâî âñåõ ñâåðõñëîâ, äîïóñòèìûõ äëÿ àâòîìàòà A .
Ôîðìóëà F ñïåöèôèöèðóåò àâòîìàò A , åñëè W A W F( ) ( )� .
Ïóñòü � � { , , , }p p pm1 2 � — ñèãíàòóðà ôîðìóëû F t( ) , à r — ãëóáèíà ýòîé
ôîðìóëû. Ïîñëåäîâàòåëüíîñòü � � �0 1, , ,� r âåêòîðîâ èç � �( ) íàçîâåì ñîñòîÿíè-
åì ãëóáèíû r , à ìíîæåñòâî Q r( , )� âñåõ òàêèõ ïîñëåäîâàòåëüíîñòåé — ïðîñòðàí-
ñòâîì ñîñòîÿíèé ãëóáèíû r äëÿ ôîðìóëû F t( ) . Ôîðìóëó F t( ) áóäåì ðàññìàòðè-
âàòü êàê ïðîïîçèöèîíàëüíóþ ôîðìóëó îò ïåðåìåííûõ p t p tm1 ( ), , ( ),�
p t p tm1 1 1( ), , ( ), ,� �� � p t r p t rm1 ( ), , ( )� �� . Åñëè êîìïîíåíòû âåêòîðà � i
â ñîñòîÿíèè q r� � � �0 1, , ,� ðàññìàòðèâàòü êàê èñòèííîñòíûå çíà÷åíèÿ ñîîòâåò-
ñòâóþùèõ àòîìîâ ðàíãà i r� ïðè îïðåäåëåííîì óïîðÿäî÷åíèè ìíîæåñòâà � , òî
ìîæíî ãîâîðèòü î çíà÷åíèè ôîðìóëû F t( ) íà ñîñòîÿíèè q.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2014, òîì 50, ¹ 4 5
Íà ìíîæåñòâå Q r( , )� îïðåäåëèì îòíîøåíèå N íåïîñðåäñòâåííîãî ñëåäîâà-
íèÿ òàê, ÷òî çà êàæäûì ñîñòîÿíèåì q r� � � �0 1, , ,� íåïîñðåäñòâåííî ñëåäóþò
2| |� ñîñòîÿíèé âèäà � � �1, , ,� r , ãäå � � �( ) . Ìíîæåñòâî âñåõ ñîñòîÿíèé, êîòî-
ðûå íåïîñðåäñòâåííî ñëåäóþò çà q , îáîçíà÷èì N q( ) .
Ïðè èñïîëüçîâàíèè ÿçûêà L äëÿ ñïåöèôèêàöèè X Y� -àâòîìàòîâ ïðåäèêàò-
íûå ñèìâîëû ñòàâÿòñÿ â ñîîòâåòñòâèå âõîäíûì è âûõîäíûì äâîè÷íûì êàíàëàì
ñïåöèôèöèðóåìîãî àâòîìàòà. Ïîýòîìó ìíîæåñòâî ïðåäèêàòíûõ ñèìâîëîâ � ðàç-
áèâàåòñÿ íà äâà êëàññà: âõîäíûå è âûõîäíûå, êîòîðûå îáîçíà÷àþòñÿ ñîîòâåò-
ñòâåííî U è W . Ïðè ýòîì X U� �( ) , Y W� �( ) è êàæäûé âåêòîð èç � �( ) ìîæíî
ðàññìàòðèâàòü êàê ïàðó
�x y, , ãäå x X , y Y .
Ïîñòðîèì âñïîìîãàòåëüíûé �-àâòîìàò A F Q A� �
� �( ) ( ), ,� � � . Ìíîæåñòâî ñî-
ñòîÿíèé Q� — ýòî âñå òå ñîñòîÿíèÿ èç Q r( , )� , íà êîòîðûõ F t( ) èñòèííà. Ïóñòü ñî-
ñòîÿíèå q Q � èìååò âèä � � �0 1, , ,� r è � � �( ) , òîãäà � � � � �A rq( , ) , , ,� 1 � .
Åñëè òàêèõ ñîñòîÿíèé íåò, òî çíà÷åíèå � �A q( , ) íå îïðåäåëåíî. Àâòîìàò A F( ) îïðå-
äåëèì êàê ìàêñèìàëüíûé öèêëè÷åñêèé ïîäàâòîìàò àâòîìàòà A F� ( ).
Êàê ñëåäóåò èç îïðåäåëåíèÿ ôóíêöèè ïåðåõîäîâ, âñå ñîñòîÿíèÿ àâòîìàòà
A F( ) âèäà � � �, , ,1 � r , ãäå � � �( ) , ýêâèâàëåíòíû. Àâòîìàò A F* ( ) , ñîñòîÿíèÿ-
ìè êîòîðîãî ÿâëÿþòñÿ êëàññû ýòîé ýêâèâàëåíòíîñòè, ýêâèâàëåíòåí àâòîìàòó
A F( ) . Òàêèì îáðàçîì, â êà÷åñòâå ñîñòîÿíèé àâòîìàòà, ñïåöèôèöèðóåìîãî ôîð-
ìóëîé F , ìîæíî ðàññìàòðèâàòü ïîñëåäîâàòåëüíîñòè âåêòîðîâ èç � �( ) âèäà
� �1, ,� r . Äëÿ àâòîìàòà A F* ( ) ñîñòîÿíèå � � �0 1, , ,� r àâòîìàòà A F( ) ìîæíî
ðàññìàòðèâàòü êàê ïåðåõîä èç ñîñòîÿíèÿ � � �0 1 1, , ,� r� â ñîñòîÿíèå � �1, ,� r
ïîä äåéñòâèåì ñèìâîëà � r .
ÈÃÐÎÂÀß ÌÎÄÅËÜ ÎÒÊÐÛÒÎÉ ÑÈÑÒÅÌÛ
Èãðà äâóõ ëèö îñóùåñòâëÿåòñÿ íà ðàçìå÷åííîì äâóäîëüíîì ãðàôå G V V�
1 2, ,
� �1 2, , ,P L� , ãäå V V1 2, — íåïåðåñåêàþùèåñÿ ìíîæåñòâà âåðøèí ñîîòâåò-
ñòâåííî Èãðîêà 1 è Èãðîêà 2; � 1 1 2 2: V
V
� , � 2 2 2 1: V
V
� — îòîáðàæåíèÿ,
îïðåäåëÿþùèå ìíîæåñòâî ðåáåð ãðàôà, à èìåííî: ( , ) � — ðåáðî, åñëè Vi ,
� � i ( ) (i { , }1 2 ); P — ìíîæåñòâî äâîè÷íûõ ïåðåìåííûõ (ïðåäèêàòíûõ ñèì-
âîëîâ); L V V P: 1 2 2� � — îòîáðàæåíèå, ðàçìå÷àþùåå âåðøèíû ãðàôà G.
Êàæäîå ðåáðî ãðàôà ñîîòâåòñòâóåò õîäó èãðîêà, òàê ÷òî � i ( ) îïðåäåëÿåò ìíîæåñ-
òâî õîäîâ èãðîêà i, äîïóñòèìûõ â ïîçèöèè . Òàêîé äâóäîëüíûé ãðàô íàçûâàåòñÿ
àðåíîé èãðû. Èãðà îïðåäåëÿåòñÿ àðåíîé G , íà÷àëüíîé âåðøèíîé 0 1 2 �V V ,
óêàçûâàþùåé, êàêîé èç èãðîêîâ äåëàåò ïåðâûé õîä, è óñëîâèåì âûèãðûøà äëÿ
îäíîãî èç èãðîêîâ (êàê ïðàâèëî, äëÿ Èãðîêà 1). Ïðåäïîëàãàåòñÿ, ÷òî äëÿ âñÿ-
êîãî V1 � 1 ( ) � � è äëÿ âñÿêîãî V2 � 2 ( ) � � . Äîïóñòèìûé ïðîöåññ
— ýòî áåñêîíå÷íàÿ ïîñëåäîâàòåëüíîñòü âåðøèí, ãåíåðèðóåìàÿ èãðîêàìè,
îñóùåñòâëÿþùèìè ïîî÷åðåäíûå õîäû, è íà÷èíàþùàÿñÿ âåðøèíîé 0 .
Òàêèì îáðàçîì,
� 0 1 2� , ãäå äëÿ n �1 2 3, , ,� 2 1 1 2 2n n� � � ( ) ,
2 2 2 1n n �� ( ) . Ïîâåäåíèå èãðîêà îïðåäåëÿåòñÿ åãî ñòðàòåãèåé, îãðàíè÷èâà-
þùåé âîçìîæíîñòü âûáîðà î÷åðåäíîãî õîäà èç ìíîæåñòâà äîïóñòèìûõ õîäîâ.
Îáû÷íî èíòåðåñóþòñÿ ñòðàòåãèåé Èãðîêà 1, ïðåäñòàâëÿþùåé ñîáîé îòîáðàæå-
íèå � 1 0 2 1 2 2: ( )*� � �V V
V
òàêîå, ÷òî äëÿ âñÿêîãî
, çàêàí÷èâàþùåãîñÿ âåð-
øèíîé V1, èìååì �
1 1( ) ( )� � . Ïðîöåññîì, îãðàíè÷èâàåìûì ñòðàòåãèåé
�1, íàçûâàåòñÿ òàêîé äîïóñòèìûé ïðîöåññ, ÷òî äëÿ âñÿêîãî i V 1
� i i� 1 1 0( )� . Ñòðàòåãèÿ, çàâèñÿùàÿ òîëüêî îò ïîñëåäíåé âåðøèíû ïðî-
öåññà, íàçûâàåòñÿ ïîçèöèîííîé, èëè íå èìåþùåé ïàìÿòè.
Ñóùåñòâóåò ìíîãî ðàçëè÷íûõ ñïîñîáîâ çàäàíèÿ óñëîâèÿ âûèãðûøà, òàêèõ
êàê ôîðìóëû ëîãèêè LTL [10], óñëîâèÿ ðàñïîçíàâàíèÿ äëÿ àâòîìàòîâ íàä áåñêî-
íå÷íûìè ñëîâàìè [11], óñëîâèÿ ÷åòíîñòè, èñïîëüçóþùèå ðàñêðàñêó âåðøèí ãðà-
6 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2014, òîì 50, ¹ 4
ôà [12], è äð. Â ðàññìàòðèâàåìîì âàðèàíòå èãðû óñëîâèå âûèãðûøà çàäàåòñÿ
ôîðìóëîé � tf t( ) ÿçûêà L ñ ìíîæåñòâîì ïðåäèêàòíûõ ñèìâîëîâ P. Äëÿ âñÿêîãî
äîïóñòèìîãî ïðîöåññà
� 0 1 2� îòîáðàæåíèå L îïðåäåëÿåò áåñêîíå÷íîå ñëî-
âî L L L L( ) ( ) ( ) ( )
� 0 1 2 � â àëôàâèòå �( )P . Ñòðàòåãèÿ �1 íàçûâàåòñÿ âûèã-
ðûøíîé, åñëè äëÿ ëþáîãî ïðîöåññà
� , îãðàíè÷èâàåìîãî ñòðàòåãèåé �1, ñóùåñ-
òâóåò òàêàÿ ìîäåëü äëÿ ôîðìóëû �tf t( ) , êîòîðàÿ èìååò 0-ñóôôèêñ, ñîâïàäà-
þùèé ñ L( )
� .
ÑÎÃËÀÑÎÂÀÍÈÅ ÀÂÒÎÌÀÒÎÂ, ÑÏÅÖÈÔÈÖÈÐÎÂÀÍÍÛÕ Â ßÇÛÊÅ L
 ðàìêàõ àâòîìàòíîãî ïîäõîäà èãðà ðàññìàòðèâàåòñÿ êàê âçàèìîäåéñòâèå äâóõ àâ-
òîìàòîâ, îïðåäåëÿåìîå èõ öèêëè÷åñêîé êîìïîçèöèåé. Òàêàÿ êîìïîçèöèÿ ñîîòâåò-
ñòâóåò ñòðóêòóðå, â êîòîðîé âõîäû è âûõîäû îäíîãî èç àâòîìàòîâ ñîåäèíåíû ñî-
îòâåòñòâåííî ñ âûõîäàìè è âõîäàìè äðóãîãî. Ïîñòðîåíèå âûèãðûøíîé ñòðàòåãèè
èãðîêà ñâîäèòñÿ ê ñîãëàñîâàíèþ ñïåöèôèêàöèè îäíîãî èç âçàèìîäåéñòâóþùèõ
àâòîìàòîâ ñî ñïåöèôèêàöèåé äðóãîãî [9]. Ðàññìîòðèì âêðàòöå ïðîöåäóðó ñîãëàñî-
âàíèÿ íåäåòåðìèíèðîâàííîãî àâòîìàòà Ìóðà A X Y QA A A�
�, , , ,� � ñ íåäåòåð-
ìèíèðîâàííûì àâòîìàòîì Ìóðà B Y X QB B B�
�, , , ,� � . Çàìåòèì, ÷òî ïîíÿòèå
ñîãëàñîâàííîñòè íå ñèììåòðè÷íî: èç ñîãëàñîâàííîñòè àâòîìàòà A ñ àâòîìàòîì B
íå ñëåäóåò ñîãëàñîâàííîñòü àâòîìàòà B ñ àâòîìàòîì A .
Ïóñòü s QA , q QB . Åñëè â êàæäîì òàêòå ñíà÷àëà ñâîå ñîñòîÿíèå èçìåíÿåò
àâòîìàò A , à çàòåì àâòîìàò B, èõ âçàèìîäåéñòâèå îïðåäåëÿåòñÿ ñîîòíîøåíèÿìè
s t s t q tA B( ) ( ( ), ( ( ))) � �� �1 1 è q t q t s tB A( ) ( ( ), ( ( ))) �� �1 . Åñëè ïîðÿäîê èçìå-
íåíèÿ ñîñòîÿíèé àâòîìàòîâ ïðîòèâîïîëîæíûé, òî ñîîòâåòñòâóþùèå ñîîòíîøå-
íèÿ èìåþò âèä s t s t q tA B( ) ( ( ), ( ( ))) �� �1 è q t q t s tB A( ) ( ( ), ( ( ))) � �� �1 1 . Ýòè
ñîîòíîøåíèÿ îïðåäåëÿþò âèä ñïåöèôèêàöèé ñîîòâåòñòâóþùèõ àâòîìàòîâ.
Ñîãëàñîâàííîñòü àâòîìàòà A ñ àâòîìàòîì B îïðåäåëÿåòñÿ êàê ñâîéñòâî ïà-
ðàëëåëüíîé öèêëè÷åñêîé êîìïîçèöèè ñîîòâåòñòâóþùèì îáðàçîì ñïåöèôèöèðî-
âàííûõ àâòîìàòîâ. Ïàðàëëåëüíàÿ öèêëè÷åñêàÿ êîìïîçèöèÿ X Y� -àâòîìàòà A è
Y X� -àâòîìàòà B ïðåäñòàâëÿåò ñîáîé ìàêñèìàëüíûé öèêëè÷åñêèé ïîäàâòîìàò
ïðÿìîãî ïðîèçâåäåíèÿ ñîîòâåòñòâóþùèõ �-àâòîìàòîâ ñ àëôàâèòîì � � �X Y .
Ïðåäïîëàãàåòñÿ, ÷òî àâòîìàòû A è B çàäàíû ñîîòâåòñòâåííî ñïåöèôèêàöèÿìè
�tF tA ( ) è �tF tB ( ). Àâòîìàòû, ñïåöèôèöèðîâàííûå ýòèìè ôîðìóëàìè, ðàññìàò-
ðèâàþòñÿ â îáùåì äëÿ íèõ ïðîñòðàíñòâå ñîñòîÿíèé, îïðåäåëÿåìîì ñèãíàòóðîé è
ìàêñèìàëüíîé ãëóáèíîé ôîðìóë, ñïåöèôèöèðóþùèõ àâòîìàòû A è B. Çàìåòèì,
÷òî ñïåöèôèêàöèÿ ïàðàëëåëüíîé öèêëè÷åñêîé êîìïîçèöèè àâòîìàòîâ ÿâëÿåòñÿ
êîíúþíêöèåé ñïåöèôèêàöèé ýòèõ àâòîìàòîâ. Êàæäîå ñîñòîÿíèå êîìïîçèöèè
èìååò âèä
�s q, , ãäå s QA , q QB . Òàê êàê àâòîìàòû è èõ êîìïîçèöèÿ
öèêëè÷åñêèå, ñîñòîÿíèÿì s è q ñîîòâåòñòâóåò îäíî è òî æå ñîñòîÿíèå îáùåãî äëÿ
íèõ ïðîñòðàíñòâà ñîñòîÿíèé [9].
Íåîáõîäèìîñòü ñîãëàñîâàíèÿ ñïåöèôèêàöèé àâòîìàòîâ âîçíèêàåò â ñèëó
òîãî, ÷òî ïîâåäåíèå êîìïîçèöèè àâòîìàòîâ äîëæíî óäîâëåòâîðÿòü óñëîâèþ âû-
èãðûøà, êîòîðîå ìîæåò îãðàíè÷èâàòü ïîâåäåíèå àâòîìàòà B.
Ðàññìîòðèì ïðîöåäóðó ñîãëàñîâàíèÿ àâòîìàòà A ñ àâòîìàòîì B. Â ñïåöèôè-
êàöèþ àâòîìàòà A äîáàâëÿåòñÿ ôîðìóëà, çàäàþùàÿ óñëîâèå âûèãðûøà. Â ïîëó-
÷åííîé òàêèì îáðàçîì ñïåöèôèêàöèè àâòîìàòà A îïðåäåëÿþòñÿ òå óñëîâèÿ, êîòî-
ðûå îãðàíè÷èâàþò ïîâåäåíèå àâòîìàòà B. Äëÿ ýòîãî ñïåöèôèêàöèÿ ïðåäñòàâëÿåò-
ñÿ â âèäå ïîïîëíåííîãî ìíîæåñòâà äèçúþíêòîâ, â êîòîðîì âûäåëÿþòñÿ
äèçúþíêòû, õàðàêòåðèçóþùèå ÷àñòè÷íîñòü àâòîìàòà A [9]. Îòðèöàíèÿ òàêèõ äèçúþíê-
òîâ çàäàþò ñîñòîÿíèÿ â ðàññìàòðèâàåìîì ïðîñòðàíñòâå ñîñòîÿíèé. Äëÿ îïðåäåëå-
íèÿ, â êàêèõ èç ýòèõ ñîñòîÿíèé îãðàíè÷èâàåòñÿ ïîâåäåíèå àâòîìàòà B, ôîðìóëà,
çàäàþùàÿ èõ, óìíîæàåòñÿ íà ôîðìóëó F tB ( ) , çàäàþùóþ ìíîæåñòâî âñåõ ñîñòîÿ-
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2014, òîì 50, ¹ 4 7
íèé àâòîìàòà B. Ôîðìóëó F tB ( ) óäîáíî ïðåäñòàâëÿòü â äèçúþíêòèâíîé íîðìàëü-
íîé ôîðìå. Êàæäàÿ ýëåìåíòàðíàÿ êîíúþíêöèÿ â òàêîì ïðåäñòàâëåíèè ñîîòâåò-
ñòâóåò îäíîìó èëè íåñêîëüêèì ïåðåõîäàì â àâòîìàòå B. Ïîëó÷åííîå ïðîèçâåäå-
íèå îïðåäåëÿåò ìíîæåñòâî ñîñòîÿíèé àâòîìàòà B, ïåðåõîäû â êîòîðûå
íåäîïóñòèìû. Ïîýòîìó â àâòîìàòå A, ðàññìàòðèâàåìîì â îáùåì ïðîñòðàíñòâå ñî-
ñòîÿíèé, óäàëÿþòñÿ ïåðåõîäû â òàêèå ñîñòîÿíèÿ. Ýòî çíà÷èò, ÷òî êîìïîçèöèÿ àâ-
òîìàòîâ A è B íå ìîæåò ïåðåéòè â ñîîòâåòñòâóþùèå ñîñòîÿíèÿ. Óäàëåíèå ñîñòîÿ-
íèé â àâòîìàòå A îñóùåñòâëÿåòñÿ ïóòåì óìíîæåíèÿ åãî ñïåöèôèêàöèè íà îòðè-
öàíèå äèçúþíêöèè ôîðìóë, çàäàþùèõ óäàëÿåìûå ñîñòîÿíèÿ, ò.å. äîáàâëåíèåì
â ñïåöèôèêàöèþ ñîîòâåòñòâóþùåé ôîðìóëû. Òàêîå èçìåíåíèå ñïåöèôèêàöèè
ìîæåò ïðèâåñòè ê ïîÿâëåíèþ íîâûõ îãðàíè÷åíèé íà ïîâåäåíèå àâòîìàòà B.
 ýòîì ñëó÷àå îïèñàííûé ïðîöåññ áóäåò ïîâòîðÿòüñÿ äî òåõ ïîð, ïîêà ëèáî íå
áóäåò íîâûõ îãðàíè÷åíèé, ëèáî ñïåöèôèêàöèÿ àâòîìàòà A ñòàíåò ïðîòèâîðå÷è-
âîé, ÷òî âûÿñíÿåòñÿ ïðè ïîïîëíåíèè ñïåöèôèêàöèè äëÿ îïðåäåëåíèÿ ìíîæåñòâà
äèçúþíêòîâ, õàðàêòåðèçóþùèõ ÷àñòè÷íîñòü íîâîãî àâòîìàòà A .
 íàñòîÿùåé ðàáîòå äëÿ ïîñòðîåíèÿ êîìïîçèöèè è óäàëåíèÿ ñîñòîÿíèé èñ-
ïîëüçîâàëàñü ñèñòåìà Dual ñèíòåçà àâòîìàòîâ ïî ñïåöèôèêàöèè â ÿçûêå L.
ÏÎÑÒÐÎÅÍÈÅ ÂÛÈÃÐÛØÍÎÉ ÑÒÐÀÒÅÃÈÈ Â ÈÃÐÅ ÍÈÌ
 èãðå ÍÈÌ èñïîëüçóåòñÿ n2 ôèøåê (n � 2 3 4, , ,�), ðàñïîëîæåííûõ â n ðÿäàõ.
Ïåðâûé ðÿä ñîäåðæèò îäíó ôèøêó, âòîðîé — òðè, i-é ðÿä — 2 1i � ôèøêó.
Èãðàþò äâà èãðîêà, ïî î÷åðåäè óäàëÿþùèå èç êàêîãî-ëèáî ðÿäà ïðîèçâîëüíîå
(íåíóëåâîå) êîëè÷åñòâî ôèøåê. Ïðîèãðûâàåò èãðîê, çàáèðàþùèé ïîñëåäíþþ
ôèøêó. Áåñêîíå÷íàÿ èãðà ðàçáèâàåòñÿ íà ïàðòèè. Èãðó ìîæåò íà÷èíàòü ëþáîé
èç èãðîêîâ: Èãðîê 1 èëè Èãðîê 2. Î÷åðåäíóþ ïàðòèþ íà÷èíàåò âûèãðàâøèé
èãðîê. Ïîñëå òîãî êàê èãðîê çàáèðàåò ïîñëåäíþþ ôèøêó, èãðà ïåðåõîäèò
â íà÷àëüíîå ñîñòîÿíèå. Äëÿ óïðîùåíèÿ èçëîæåíèÿ ðàññìîòðèì èãðó ïðè n � 2
è äâóõ ôèøêàõ âî âòîðîì ðÿäó.
Èãðà ìîäåëèðóåòñÿ äâóìÿ âçàèìîäåéñòâóþùèìè àâòîìàòàìè. Îäèí èç íèõ
(Players) ìîäåëèðóåò ïîâåäåíèå èãðîêîâ, à âòîðîé (Arena) — àðåíû. Âûõîäíûå
ïåðåìåííûå àâòîìàòà Arena A, R, Q1, Q2 ÿâëÿþòñÿ âõîäíûìè äëÿ àâòîìàòà
Players, à âõîäíûå ïåðåìåííûå àâòîìàòà Arena F, S1, S2 — âûõîäíûìè äëÿ àâòî-
ìàòà Players. Âõîäíûì è âûõîäíûì ïåðåìåííûì àâòîìàòîâ ñîîòâåòñòâóþò âõîä-
íûå è âûõîäíûå ïðåäèêàòíûå ñèìâîëû èõ ñïåöèôèêàöèé. Ðàññìîòðèì èíòåðïðå-
òàöèþ (ñìûñë) ýòèõ ïðåäèêàòíûõ ñèìâîëîâ. Çíà÷åíèå ñèìâîëà A â ñîñòîÿíèè àâ-
òîìàòà Arena îïðåäåëÿåò, êàêîé èç èãðîêîâ äåëàåò ñëåäóþùèé õîä: åäèíè÷íîå
çíà÷åíèå A ñîîòâåòñòâóåò õîäó Èãðîêà 1, à íóëåâîå — õîäó Èãðîêà 2. Î÷åðåä-
íîñòü õîäîâ èãðîêîâ îïðåäåëÿåòñÿ ôîðìóëàìè A t A t( ) ( ),� � �1 � � �A t A t( ) ( ).1
Ñèìâîë R ñîîòâåòñòâóåò íàëè÷èþ ôèøêè â ïåðâîì ðÿäó, à Q1, Q2 — ñîîòâåò-
ñòâåííî íàëè÷èþ îäíîé èëè äâóõ ôèøåê âî âòîðîì ðÿäó. Ñèìâîë F
ñîîòâåòñòâóåò óäàëåíèþ ôèøêè èç ïåðâîãî ðÿäà, à S1, S2 — ñîîòâåòñòâåííî
óäàëåíèþ îäíîé èëè äâóõ ôèøåê èç âòîðîãî.
Ñîñòîÿíèÿ àâòîìàòîâ Players è Arena â òå÷åíèå îäíîãî òàêòà èçìåíÿþòñÿ
â òàêîì ïîðÿäêå: ñíà÷àëà èçìåíÿåò ñîñòîÿíèå àâòîìàò Players, çàòåì — àâòîìàò
Arena. Ïîýòîìó ñïåöèôèêàöèÿ àâòîìàòà Players óäîâëåòâîðÿåò âûðàæåíèþ
s t s t q tA B( ) ( ( ), ( ( ))) � �� �1 1 , ïðè÷åì ñîñòîÿíèå ýòîãî àâòîìàòà çàâèñèò òîëüêî
îò âõîäíîãî ñèãíàëà â ïðåäûäóùèé ìîìåíò âðåìåíè. Ñïåöèôèêàöèÿ àâòîìàòà
Players èìååò ñëåäóþùèé âèä.
Inputs: A, R, Q1, Q2.
Outputs: F, S1, S2.
F(t) � R(t-1). S1(t) � (Q1(t-1) | Q2(t-1)). S2(t) � Q2(t-1).
F(t) | S1(t) | S2(t). ~F(t) | ~S1(t). ~F(t) | ~S2(t). ~S1(t) | ~S2(t).
8 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2014, òîì 50, ¹ 4
Ýòè ôîðìóëû çàïèñàíû â ñîîòâåòñòâèè ñ ñèíòàêñèñîì ÿçûêà L, ðåàëèçîâàí-
íîãî â ñèñòåìå Dual. Çäåñü è äàëåå ñèìâîë ~ îáîçíà÷àåò îòðèöàíèå, ñèìâîë | —
äèçúþíêöèþ, à ñèìâîëû � è � — ñîîòâåòñòâåííî èìïëèêàöèþ è ýêâèâàëåíò-
íîñòü. Ôîðìóëû ãëóáèíû 0 îïðåäåëÿþò îãðàíè÷åíèÿ íà âûõîäíîé àëôàâèò àâòî-
ìàòà Players, ïðè êîòîðûõ íèêàêèå äâà äåéñòâèÿ àâòîìàòà íå ìîãóò âûïîëíÿòüñÿ
îäíîâðåìåííî è â êàæäîì òàêòå âûïîëíÿåòñÿ îäíî èç íèõ. Ñèìâîëàìè âõîäíîãî
àëôàâèòà àâòîìàòà Players ÿâëÿþòñÿ ñîñòîÿíèÿ àâòîìàòà Arena, ò.å. êîíñòèòóåíòû
åäèíèöû îò áóëåâûõ ïåðåìåííûõ A, R, Q1, Q2. Õîäû Èãðîêà 1 ñîîòâåòñòâóþò
âûõîäíûì ñèãíàëàì àâòîìàòà Players ïðè ïîñòóïëåíèè íà åãî âõîä ñîñòîÿíèÿ,
â îòìåòêå êîòîðîãî èìååòñÿ ñèìâîë A, à õîäû Èãðîêà 2 îïðåäåëÿþòñÿ ñîñòîÿíèÿ-
ìè àâòîìàòà Arena, èìåþùèìè îòìåòêè ñ ñèìâîëîì ~A. Ñîñòîÿíèÿ àâòîìàòà
Arena ðàçîáüåì íà äâà ìíîæåñòâà: ñîñòîÿíèÿ òèïà A, îïðåäåëÿþùèå õîäû Èãðî-
êà 1, è ñîñòîÿíèÿ òèïà ~A, îïðåäåëÿþùèå õîäû Èãðîêà 2. Òàêèì îáðàçîì, âûõîä-
íîé ñèãíàë àâòîìàòà Players, ñîîòâåòñòâóþùèé õîäó Èãðîêà 1, ïåðåâîäèò àâòîìàò
Arena â ñîñòîÿíèå òèïà ~A, ÷òî ñîîòâåòñòâóåò ñëåäóþùåìó õîäó Èãðîêà 2.
Ñïåöèôèêàöèÿ àâòîìàòà Arena èìååò òàêîé âèä:
Inputs: F, S1, S2.
Outputs: A, R, Q1, Q2.
~Q1(t) | ~Q2(t). R(t) | Q1(t) | Q2(t). A(t-1) � ~A(t). ~A(t-1) � A(t).
R(t) � (R(t-1)&~F(t) | R(t-1)&~Q1(t-1)&~Q2(t-1)&F(t) | ~R(t-1)&Q1(t-1)&S1(t) |
~R(t-1)&Q2(t-1)&S2(t)).
Q1(t) � (Q1(t-1)&~S1(t) | Q2(t-1)&S1(t)).
Q2(t) � (Q2(t-1)&~S1(t)&~S2(t) | R(t-1)&~Q1(t-1)&~Q2(t-1)&F(t) |
~R(t-1)&Q1(t-1)&S1(t)| ~R(t-1)&Q2(t-1)&S2(t)).
Ïåðâûå äâå ôîðìóëû îãðàíè÷èâàþò ìíîæåñòâî âîçìîæíûõ ñîñòîÿíèé
àâòîìàòà.
Íà÷àëüíîìó ñîñòîÿíèþ èãðû ñîîòâåòñòâóåò îäíî èç íà÷àëüíûõ ñîñòîÿíèé
àâòîìàòà Arena: A(t)&R(t)&~Q1(t)&Q2(t) èëè ~A(t)&R(t)&~Q1(t)&Q2(t), îïðåäå-
ëÿþùåå, êàêîé èç èãðîêîâ äåëàåò ïåðâûé õîä.
Ðàññìàòðèâàåìàÿ çàäà÷à ñîñòîèò â ïîñòðîåíèè âûèãðûøíîé ñòðàòåãèè Èãðîêà 1,
äëÿ ÷åãî ôîðìóëèðóåòñÿ óñëîâèå âûèãðûøà, êîòîðîìó äîëæíî óäîâëåòâîðÿòü ïîâåäå-
íèå êîìïîçèöèè âçàèìîäåéñòâóþùèõ àâòîìàòîâ. Ïîñòðîåíèå âûèãðûøíîé ñòðàòåãèè
(åñëè îíà ñóùåñòâóåò) ñîñòîèò â íàõîæäåíèè òàêèõ îãðàíè÷åíèé íà ïåðåõîäû â àâòî-
ìàòå Players, ñîîòâåòñòâóþùèå õîäàì Èãðîêà 1, ÷òîáû óñëîâèÿ âûèãðûøà âûïîëíÿ-
ëèñü íåçàâèñèìî îò ïîâåäåíèÿ Èãðîêà 2, íà êîòîðîå íåïîñðåäñòâåííî âëèÿòü íåëüçÿ.
Óñëîâèå âûèãðûøà ôîðìóëèðóåòñÿ êàê íåäîïóñòèìîñòü (ïîñëå õîäà Èãðîêà 2) ñîñòîÿ-
íèé àðåíû, ïîñëå êîòîðûõ áåçóñëîâíî ñëåäóåò ïðîèãðûø Èãðîêà 1. Òàêèå ñîñòîÿíèÿ
õàðàêòåðèçóþòñÿ íàëè÷èåì åäèíñòâåííîé ôèøêè è îïèñûâàþòñÿ ôîðìóëàìè
A(t)&R(t)&~Q1(t)&~Q2(t) è A(t)&~R(t)&Q1(t)&~Q2(t). Ñëåäîâàòåëüíî, óñëîâèå âûèã-
ðûøà èìååò âèä ~A(t-1) � ~(R(t)&~Q1(t)&~Q2(t) | ~R(t)&Q1(t)&~Q2(t)). Äîáàâëåíèå
ýòîé ôîðìóëû â ñïåöèôèêàöèþ àâòîìàòà Players íàëàãàåò îãðàíè÷åíèÿ íà ïîâåäåíèå
àðåíû, à çíà÷èò, è Èãðîêà 2. Äðóãèìè ñëîâàìè, â àâòîìàòå Players çàïðåùàþòñÿ òàêèå
ïåðåõîäû, êîòîðûå ïðèâîäÿò ê ñîñòîÿíèÿì àðåíû A(t)&~R(t)&Q1(t)&~Q2(t) èëè
A(t)&R(t)&~Q1(t)&~Q2(t).
Ïîñêîëüêó óñëîâèå âûèãðûøà õàðàêòåðèçóåò ìíîæåñòâî íåäîïóñòèìûõ ñîñòîÿ-
íèé àðåíû, ò.å. ñîñòîÿíèé A(t)&~R(t)&Q1(t)&~Q2(t) è A(t)&R(t)&~Q1(t)&~Q2(t),
â äàííîì ñëó÷àå èõ íå íóæíî íàõîäèòü, èñïîëüçóÿ äèçúþíêòû âòîðîãî ðîäà â ïîïîë-
íåííîì ìíîæåñòâå äèçúþíêòîâ ñïåöèôèêàöèè àâòîìàòà Players ñ äîáàâëåííûì â íåå
óñëîâèåì âûèãðûøà (êàê ýòî ñëåäóåò èç àëãîðèòìà, ïðèâåäåííîãî â [9]).
Ïðåæäå ÷åì ðàññìîòðåòü áîëåå ïîäðîáíî ïîñòðîåíèå âûèãðûøíîé ñòðàòåãèè
Èãðîêà 1, íàïîìíèì, ÷òî ñîñòîÿíèÿìè âçàèìîäåéñòâóþùèõ àâòîìàòîâ è èõ êîì-
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2014, òîì 50, ¹ 4 9
ïîçèöèè ÿâëÿþòñÿ ñîñòîÿíèÿ îáùåãî äëÿ íèõ ïðîñòðàíñòâà ñîñòîÿíèé. Ïðè ýòîì
âñå àâòîìàòû ðàññìàòðèâàþòñÿ êàê àâòîìàòû Ìóðà, ïðåäñòàâëåííûå â ýòîì ïðî-
ñòðàíñòâå ñîñòîÿíèé. Ïîñêîëüêó ãëóáèíà ôîðìóë ñïåöèôèêàöèè ðàâíà 1, ýëåìåí-
òàðíûå êîíúþíêöèè, çàäàþùèå ñîñòîÿíèÿ, èìåþò âèä s t s t0 1 1( )& ( )� , ãäå s t1 1( )�
è s t0 ( ) — êîíúþíêöèè àòîìîâ ñîîòâåòñòâåííî ðàíãîâ –1 è 0, îáðàçîâàííûõ ïðå-
äèêàòíûìè ñèìâîëàìè ñèãíàòóðû ñïåöèôèêàöèè. Åñëè ñîñòîÿíèå s t s t0 1 1( )& ( )�
ðàññìàòðèâàòü êàê ïåðåõîä â àâòîìàòå, òî êîíúþíêöèÿ s t1 ( ) çàäàåò ñîñòîÿíèå àâ-
òîìàòà, èç êîòîðîãî îñóùåñòâëÿåòñÿ ïåðåõîä â ñîñòîÿíèå s t0 ( ) ïîä äåéñòâèåì
âõîäíîãî ñèìâîëà, îïðåäåëÿåìîãî âõîäíûìè àòîìàìè â ñîñòîÿíèè s t0 ( ) .
Ñïåöèôèêàöèÿ êîìïîçèöèè àâòîìàòîâ Players è Arena ïðåäñòàâëÿåò ñîáîé
êîíúþíêöèþ èõ ñïåöèôèêàöèé. Ïðèâåä¸ííûé àâòîìàò êîìïîçèöèè, ïîëó÷åííûé
â ðåçóëüòàòå ñèíòåçà â ñèñòåìå Dual, èìååò ñëåäóþùèé âèä:
(A,R,Q2) 3: S2 � 0 (R), (R,Q2) 1: S2 � 2 (A, R),
S1 � 4 (R, Q1), S1 � 5 (A, R, Q1),
F � 8 (Q2). F � 9 (A, Q2).
(R,Q1) 4: S1 � 2 (A, R), (A,R,Q1) 5: S1 � 0 (R),
F � 7 (A, Q1). F � 6 (Q1).
(Q2) 8: S2 � 3 (A, R, Q2), (A,Q2) 9: S2 � 1 (R, Q2),
S1 � 7 (A, Q1). S1 � 6 (Q1).
(R) 0: F � 3 (A, R, Q2). (A,R) 2: F � 1 (R, Q2).
(A,Q1) 7: S1 � 1 (R, Q2). (Q1) 6: S1 � 3 (A, R, Q2).
Çäåñü ïàðàëëåëüíàÿ êîìïîçèöèÿ ïðåäñòàâëåíà â âèäå X Y� -àâòîìàòà Ìóðà
ñ âõîäíûì è âûõîäíûì àëôàâèòàìè, òàêèìè æå, êàê ó àâòîìàòà Arena. Îòìåò-
êè ñîñòîÿíèé ïðèâåäåíû â ñêîáêàõ, ãäå óêàçàíû òîëüêî òå ïåðåìåííûå, êîòî-
ðûå âõîäÿò â îòìåòêó áåç îòðèöàíèÿ. Òàê, íàïðèìåð, (R) ñîîòâåòñòâóåò îòìåò-
êå (~A&R&~Q1&~Q2). Óñëîâèå âûèãðûøà îãðàíè÷èâàåò ïîâåäåíèå ýòîãî àâ-
òîìàòà, çàïðåùàÿ â íåì ïîä÷åðêíóòûå ïåðåõîäû â íåäîïóñòèìûå ñîñòîÿíèÿ.
Êîìïîçèöèÿ àâòîìàòîâ Players è Arena îïðåäåëÿåò ìíîæåñòâî âñåõ äîïóñòè-
ìûõ ïîâåäåíèé èãðû. Ïîýòîìó äëÿ îïðåäåëåíèÿ ìíîæåñòâà âñåõ ñîñòîÿíèé àâòî-
ìàòà Arena, èç êîòîðûõ èìååòñÿ ïåðåõîä â íåäîïóñòèìûå ñîñòîÿíèÿ, ñëåäóåò èñ-
ïîëüçîâàòü ñïåöèôèêàöèþ ïðèâåäåííîãî âûøå àâòîìàòà êîìïîçèöèè.
Ïîñòðîåíèå ñòðàòåãèè Èãðîêà 1 íà÷èíàåòñÿ ñ íàõîæäåíèÿ âñåõ ñîñòîÿíèé
êîìïîçèöèè, èç êîòîðûõ èìåþòñÿ ïåðåõîäû â íåäîïóñòèìûå ñîñòîÿíèÿ. Ýòî ñî-
ñòîÿíèÿ 1 , 4 è 8 òèïà ~A. Ïåðåõîäû â íèõ (ñîîòâåòñòâóþùèå õîäàì Èãðîêà 1)
äîëæíû áûòü óäàëåíû, ÷òî ïðèâîäèò ê óäàëåíèþ â êîìïîçèöèè ñàìèõ ñîñòîÿíèé.
Ðàññìîòðèì, íàïðèìåð, ïîñëåäîâàòåëüíîñòü ñîñòîÿíèé àðåíû A&R&~Q1&Q2,
~A&R&Q1&~Q2, A&~R&Q1&~Q2, íà÷èíàþùóþñÿ íà÷àëüíûì ñîñòîÿíèåì è
îïðåäåëÿåìóþ ïîñëåäîâàòåëüíîé ãåíåðàöèåé àâòîìàòîì Players ñèãíàëîâ ~F&
S1&~S2 è F&~S1&~S2. Ïåðâûé èç íèõ ñîîòâåòñòâóåò õîäó Èãðîêà 1, à âòîðîé —
õîäó Èãðîêà 2. Ñîñòîÿíèå A&~R&Q1&~Q2 íåäîïóñòèìî, ïîýòîìó âñå ïåðåõîäû
â ñîñòîÿíèå ~A&R&Q1&~Q2, èç êîòîðîãî èìååòñÿ ïåðåõîä â A&~R&Q1&~Q2,
äîëæíû áûòü óäàëåíû, â ÷àñòíîñòè, íåîáõîäèìî óäàëèòü ïåðåõîä èç ñîñòîÿíèÿ
A&R&~Q1&Q2 ïîä äåéñòâèåì ñèãíàëà ~F&S1&~S2.
Èòàê, ñíà÷àëà íàõîäÿòñÿ ñîñòîÿíèÿ êîìïîçèöèè, èç êîòîðûõ îñóùåñòâëÿåòñÿ
ïåðåõîä â íåäîïóñòèìûå ñîñòîÿíèÿ. Äëÿ ðàññìàòðèâàåìîãî ïðèìåðà â ñîñòîÿ-
íèå 7, êîòîðîìó ñîîòâåòñòâóåò ôîðìóëà A(t)&~R(t)&Q1(t)&~Q2(t), èìåþòñÿ ïå-
ðåõîäû èç ñîñòîÿíèé 4 è 8, çàäàâàåìûõ ôîðìóëàìè ~A(t)&R(t)&Q1(t)&~Q2(t) è
~A(t)&~R(t)&~Q1(t)&Q2(t). Â ñîñòîÿíèå 2 èìåþòñÿ ïåðåõîäû èç ñîñòîÿíèé 1 è 4,
çàäàâàåìûõ ôîðìóëàìè ~A(t)&R(t)&~Q1(t)&Q2(t) è ~A(t)&R(t)&Q1(t)&~Q2(t).
Çàòåì îïðåäåëÿþòñÿ âñå ïåðåõîäû â ñîñòîÿíèÿ ~A(t)&R(t)&Q1(t)&~Q2(t), ~A(t) &
10 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2014, òîì 50, ¹ 4
~R(t)&~Q1(t)&Q2(t) è ~A(t)&R(t)&~Q1(t)&Q2(t), ñîîòâåòñòâóþùèå õîäàì Èãðîêà
1. Òàê, ïåðåõîä èç ñîñòîÿíèÿ A(t)&R(t)&~Q1(t)&Q2(t) â ñîñòîÿíèå
~A(t)&R(t)&Q1(t)&~Q2(t) ïîä äåéñòâèåì ñèãíàëà S1 (~F(t)&S1(t)&~S2(t)) îïðåäå-
ëÿåòñÿ ôîðìóëîé S1(t)&~S2(t)&A(t-1)&R(t-1)&~Q1(t-1)&Q2(t-1). Êðîìå òîãî, áó-
äóò ïîñòðîåíû ïåðåõîäû F(t)&A(t-1)&R(t-1)&~Q1(t-1)&Q2(t-1), F(t)&A(t-1)&
R(t-1)&~Q1(t-1)&~Q2(t-1), S1(t)&A(t-1)&~R(t-1)&Q1(t-1)&~Q2(t-1) è S2(t)&A(t-1)&
~R(t-1)&~Q1(t-1)&Q2(t-1).
Äîáàâëåíèå â ñïåöèôèêàöèþ àâòîìàòà Players äèçúþíêòîâ
~S1(t) | ~A(t-1) | ~R(t-1) | Q1(t-1) | ~Q2(t-1), ~F(t) | ~A(t-1) | ~R(t-1) | Q1(t-1),
~S1(t) | ~A(t-1) | R(t-1) | ~Q1(t-1) è ~S2(t) | ~A(t-1) | R(t-1) | Q1(t-1) | ~Q2(t-1),
ïðåäñòàâëÿþùèõ îòðèöàíèÿ ôîðìóë, çàäàþùèõ óêàçàííûå ïåðåõîäû, óäàëÿåò
â íåì ñîîòâåòñòâóþùèå ïåðåõîäû. Ïîñëå äîáàâëåíèÿ ýòèõ äèçúþíêòîâ èç ñïåöè-
ôèêàöèè óäàëÿåòñÿ óñëîâèå âûèãðûøà è ïåðâûé öèêë ïîñòðîåíèÿ âûèãðûøíîé
ñòðàòåãèè Èãðîêà 1 çàêàí÷èâàåòñÿ.
Åñëè èç íåêîòîðîãî ñîñòîÿíèèÿ êîìïîçèöèè âñå ïåðåõîäû áóäóò óäàëåíû,
îíî ñòàíîâèòñÿ òóïèêîâûì è ïðè ïîñòðîåíèè êîìïîçèöèè òàêæå áóäåò óäàëåíî.
Ýòî îçíà÷àåò, ÷òî ïåðåõîä â òàêîå ñîñòîÿíèå â ðåçóëüòàòå õîäà Èãðîêà 2 îòñóò-
ñòâóåò, ò.å. ïîâåäåíèå àâòîìàòà Players, ñîîòâåòñòâóþùåå Èãðîêó 2, â ñîñòîÿíèè,
èç êîòîðîãî ýòîò ïåðåõîä áûë îïðåäåëåí, îãðàíè÷èâàåòñÿ. Òàêèì îáðàçîì, ïîñëå
ïåðâîãî öèêëà ðàáîòû àëãîðèòìà ìîãóò ïîÿâèòüñÿ íîâûå íåäîïóñòèìûå ñîñòîÿ-
íèÿ, ÷òî âëå÷åò î÷åðåäíîé öèêë. Ñëåäîâàòåëüíî, ïîñëå îêîí÷àíèÿ ïåðâîãî öèêëà
íåîáõîäèìî âûÿñíèòü, íå ïîÿâèëèñü ëè íîâûå íåäîïóñòèìûå ñîñòîÿíèÿ. Äëÿ ýòî-
ãî ñèíòåçèðóåòñÿ íîâàÿ êîìïîçèöèÿ, îïðåäåëÿåìàÿ ïðåîáðàçîâàííîé ñïåöèôèêà-
öèåé àâòîìàòà Players è èñõîäíîé ñïåöèôèêàöèåé àâòîìàòà Arena.
 ïåðâîì öèêëå íåäîïóñòèìûå ñîñòîÿíèÿ èçíà÷àëüíî èçâåñòíû.  îñòàëüíûõ
öèêëàõ íåîáõîäèìî îïðåäåëÿòü íàëè÷èå íîâûõ íåäîïóñòèìûõ ñîñòîÿíèé. Ýòè ñî-
ñòîÿíèÿ íàõîäÿòñÿ ïóòåì ñðàâíåíèÿ ìíîæåñòâ ïåðåõîäîâ â êàæäîì èç îñòàâøèõ-
ñÿ ñîñòîÿíèé òèïà ~A â ïðåäûäóùåé êîìïîçèöèè è â íîâîé. Åñëè èìåþòñÿ ñîñòî-
ÿíèÿ, êîëè÷åñòâî ïåðåõîäîâ èç êîòîðûõ óìåíüøèëîñü (óìåíüøèëñÿ íåäåòåðìè-
íèçì), òî âñå ïåðåõîäû â òàêèå ñîñòîÿíèÿ (èç ñîñòîÿíèé òèïà A) äîëæíû áûòü
óäàëåíû.
 ðàññìàòðèâàåìîì ïðèìåðå (ïðè íà÷àëüíîì ñîñòîÿíèè A(t)&R(t)&
~Q1(t)&Q2(t)) ïîñëå ïåðâîãî öèêëà ïîñòðîåíèÿ ñòðàòåãèè îñòàåòñÿ îäíî ñîñòîÿ-
íèå òèïà ~A, à èìåííî ~A(t)&R(t)&~Q1(t)&~Q2(t), âñå ïåðåõîäû èç êîòîðîãî ñî-
õðàíåíû. Íà ýòîì ïîñòðîåíèå ñòðàòåãèè çàêàí÷èâàåòñÿ.
Çàìåòèì, ÷òî ñîñòîÿíèå òèïà A óäàëÿåòñÿ ïîñëå âûïîëíåíèÿ î÷åðåäíîãî
öèêëà ïî äâóì ïðè÷èíàì: îíî ñòàíîâèòñÿ òóïèêîâûì â ðåçóëüòàòå óäàëåíèÿ èç
íåãî âñåõ ïåðåõîäîâ; îíî ñòàíîâèòñÿ «èñòî÷íèêîì» çà ñ÷åò óäàëåíèÿ âñåõ ïåðå-
õîäîâ â íåãî â ðåçóëüòàòå óäàëåíèÿ ñîñòîÿíèé òèïà ~A. Óäàëåíèå «èñòî÷íèêà» íå
ïðèâîäèò ê óâåëè÷åíèþ ÷àñòè÷íîñòè íèêàêîãî èç îñòàâøèõñÿ ñîñòîÿíèé òèïà ~A.
Òàê, ïîñëå óäàëåíèÿ âñåõ ïåðåõîäîâ â ñîñòîÿíèÿ ~A(t)&R(t)&Q1(t)&~Q2(t),
~A(t)&~R(t)&~Q1(t)&Q2(t) è ~A(t)&R(t)&~Q1(t)&Q2(t) îíè ñòàíîâÿòñÿ «èñòî÷íè-
êàìè» è â êîìïîçèöèè, ÿâëÿþùåéñÿ öèêëè÷åñêèì àâòîìàòîì, îòñóòñòâóþò.
Âìåñòî óäàëåíèÿ ïåðåõîäîâ â ýòè ñîñòîÿíèÿ ìîæíî óäàëèòü ñàìè ñîñòîÿíèÿ. Äëÿ
ýòîãî íóæíî äîáàâèòü äèçúþíêöèè A(t) | ~R(t) | ~Q1(t) è A(t) | ~Q2(t). Ñëåäîâàòåëü-
íî, êàæäûé öèêë ïîñòðîåíèÿ ñòðàòåãèè óïðîùàåòñÿ. Òàêèì îáðàçîì, ïîñòðîåíèå
âûèãðûøíîé ñòðàòåãèè îñóùåñòâëÿåòñÿ òîëüêî ïóòåì ïðåîáðàçîâàíèÿ êîìïîçè-
öèè àâòîìàòîâ.
Ïîñëå î÷åðåäíîãî öèêëà ïîñòðîåíèÿ ñòðàòåãèè íàõîæäåíèå íîâûõ íåäîïóñ-
òèìûõ ñîñòîÿíèé ìîæíî îñóùåñòâëÿòü ñëåäóþùèì îáðàçîì. Â ñèíòåçèðîâàííîì
àâòîìàòå êîìïîçèöèè àíàëèçèðóþòñÿ âñå ñîñòîÿíèÿ òèïà ~A. Êàæäîå ñîñòîÿíèå
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2014, òîì 50, ¹ 4 11
îïðåäåëÿåò êîëè÷åñòâî òåîðåòè÷åñêè âîçìîæíûõ ïåðåõîäîâ èç íåãî. Òàê, íàïðè-
ìåð, êîëè÷åñòâî âîçìîæíûõ ïåðåõîäîâ èç ñîñòîÿíèÿ ~A(t)&R(t)&~Q1(t)&Q2(t)
ðàâíî òðåì. Åñëè ðåàëüíîå êîëè÷åñòâî ïåðåõîäîâ ìåíüøå, òî ýòî ñîñòîÿíèå íåäî-
ïóñòèìî, ïîýòîìó íå íóæíî âûïîëíÿòü ñðàâíåíèå ñ ïðåäûäóùèì èëè èñõîäíûì
âàðèàíòîì êîìïîçèöèè.
ÇÀÊËÞ×ÅÍÈÅ
 ðàáîòå ðàññìîòðåí ìåòîä íàõîæäåíèÿ âûèãðûøíîé ñòðàòåãèè îäíîãî èç èãðî-
êîâ â áåñêîíå÷íîé èãðå äâóõ ëèö ñ íóëåâîé ñóììîé ïðè àâòîìàòíîé èíòåðïðå-
òàöèè îñíîâíûõ ïîíÿòèé ñîîòâåòñòâóþùåé ìîäåëè èãðû. Àâòîìàòíàÿ èíòåðïðå-
òàöèÿ ïîíÿòèé «èãðîêè» è «àðåíà» ïîçâîëèëà äëÿ íàõîæäåíèÿ âûèãðûøíîé
ñòðàòåãèè èñïîëüçîâàòü ìåòîäû ñîãëàñîâàíèÿ àâòîìàòîâ, ïðåäëîæåííûå â [8, 9]
äëÿ îáåñïå÷åíèÿ êîððåêòíîãî ïîâåäåíèÿ âçàèìîäåéñòâóþùèõ àâòîìàòîâ. Ïîíÿ-
òèå êîððåêòíîñòè âçàèìîäåéñòâèÿ âîçíèêàåò â ñëó÷àå, åñëè îäèí èëè îáà âçàè-
ìîäåéñòâóþùèõ àâòîìàòà ÷àñòè÷íûå. Ïðè ýòîì êîððåêòíîñòü îïðåäåëÿåòñÿ òðå-
áîâàíèåì, ÷òîáû àâòîìàòû íèêîãäà íå ìîãëè îêàçàòüñÿ â òàêèõ ñîñòîÿíèÿõ, êîã-
äà ïåðåõîä â îäíîì èç íèõ ïîä äåéñòâèåì ñèãíàëà, ïîñòóïàþùåãî èç äðóãîãî,
áóäåò íå îïðåäåëåí.
Îáû÷íî â èãðîâîé ìîäåëè ðåàêòèâíîé ñèñòåìû îäèí èç èãðîêîâ ïðåäñòàâëÿ-
åò ñèñòåìó, à äðóãîé — ñðåäó. Ñîãëàñîâàíèå ñèñòåìû ñî ñðåäîé ñîñòîèò â òàêîì
ïðåîáðàçîâàíèè ïîâåäåíèÿ ñèñòåìû, ïðè êîòîðîì åå âçàèìîäåéñòâèå ñî ñðåäîé
ñòàíîâèòñÿ êîððåêòíûì è ñîõðàíÿåò çàäàííûå ñâîéñòâà. Îñîáåííîñòüþ ðàññìàò-
ðèâàåìîé ìîäåëè èãðû ÿâëÿåòñÿ òî, ÷òî îáà èãðîêà ìîäåëèðóþòñÿ îäíèì è òåì
æå àâòîìàòîì. Ïðè ýòîì â ïðîöåññå ñîãëàñîâàíèÿ ñëåäóåò óäàëÿòü èç ïðîåêòèðóå-
ìîãî àâòîìàòà íå ïåðåõîäû â íåäîïóñòèìûå ñîñòîÿíèÿ òèïà A, à ïåðåõîäû
â ñîñòîÿíèÿ, èç êîòîðûõ èìåþòñÿ ïåðåõîäû â íåäîïóñòèìûå ñîñòîÿíèÿ.
Ðàññìîòðåíà ïðîöåäóðà ñîãëàñîâàíèÿ, îñíîâàííàÿ íà ñèíòåçå àâòîìàòà ïî
åãî ñïåöèôèêàöèè â ÿçûêå L. Â ýòîé ïðîöåäóðå íåîáõîäèìî ñèíòåçèðîâàòü àâòî-
ìàò Arena è åãî êîìïîçèöèþ ñ àâòîìàòîì Players. Ïîñòðîåíèå âûèãðûøíîé ñòðà-
òåãèè ñîñòîèò â ïðåîáðàçîâàíèè êîìïîçèöèè àâòîìàòîâ ïóòåì óäàëåíèÿ â àâòî-
ìàòå Players íåêîòîðûõ ïåðåõîäîâ, ñîîòâåòñòâóþùèõ õîäàì Èãðîêà 1. Âñå ýòè
ïðåîáðàçîâàíèÿ ìîæíî âûïîëíÿòü íà óðîâíå ñïåöèôèêàöèé, íå ñèíòåçèðóÿ ñîîò-
âåòñòâóþùèõ àâòîìàòîâ. Îäíàêî ïðè ýòîì äëÿ íàõîæäåíèÿ íåäîïóñòèìûõ ñîñòî-
ÿíèé íåîáõîäèìî îñóùåñòâëÿòü ïðîâåðêó íåïðîòèâîðå÷èâîñòè (ò.å. ïîïîëíåíèå)
ñïåöèôèêàöèè àâòîìàòà Players ïîñëå êàæäîé åå ìîäèôèêàöèè. Çàìåòèì, ÷òî ïî-
ïîëíÿòü ñëåäóåò òîëüêî ñïåöèôèêàöèþ àâòîìàòà Players, à ñèíòåçèðóåòñÿ êîìïî-
çèöèÿ àâòîìàòîâ, ñïåöèôèêàöèÿ êîòîðîé âêëþ÷àåò â ñåáÿ ñïåöèôèêàöèè îáîèõ
àâòîìàòîâ. Îäíàêî ýòî íå ñèëüíî âëèÿåò íà âðåìåííóþ ñëîæíîñòü ñèíòåçà, ïî-
ñêîëüêó îíà â îñíîâíîì îïðåäåëÿåòñÿ ðàçìåðíîñòüþ çàäà÷è, ò.å. êîëè÷åñòâîì
ïðåäèêàòíûõ ñèìâîëîâ â ñïåöèôèêàöèè è åå ãëóáèíîé, à ýòè ïàðàìåòðû ó ñïåöè-
ôèêàöèé àâòîìàòîâ è èõ êîìïîçèöèè îäíè è òå æå. Êàêîé èç âàðèàíòîâ ïðîöåäó-
ðû ñîãëàñîâàíèÿ ïðîùå, çàâèñèò îò èñïîëüçóåìûõ àëãîðèòìîâ ñèíòåçà è ïîïîë-
íåíèÿ ìíîæåñòâà äèçúþíêòîâ, à òàêæå îò èõ ðåàëèçàöèè â âèäå ïðîãðàìì.
Ïî-âèäèìîìó, ïðè ðåàëèçàöèè ïðîöåäóðû íà ðàñïðåäåëåííûõ (ïàðàëëåëüíûõ)
êîìïüþòåðíûõ ñèñòåìàõ ïðåèìóùåñòâî áóäåò èìåòü âàðèàíò íà îñíîâå ñèíòåçà,
ïîñêîëüêó áîëüøèíñòâî àëãîðèòìîâ ñèíòåçà äîïóñêàåò âûñîêóþ ñòåïåíü ðàñïà-
ðàëëåëèâàíèÿ.
Çàìåòèì, ÷òî â ñòàòüå ðàññìàòðèâàåòñÿ êîìïîçèöèÿ èíèöèàëüíûõ àâòîìàòîâ,
êîòîðàÿ òàêæå ÿâëÿåòñÿ èíèöèàëüíûì àâòîìàòîì. Ïîýòîìó ïðè îïðåäåëåíèè íå-
äîïóñòèìûõ ñîñòîÿíèé àíàëèçèðóþòñÿ íå âñå ñîñòîÿíèÿ êîìïîçèöèè òèïà ~A,
à òîëüêî òå, êîòîðûå ïðèíàäëåæàò åå èíèöèàëüíîìó ïîäàâòîìàòó. Òàêèì îáðà-
12 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2014, òîì 50, ¹ 4
çîì, ìåòîäû, îñíîâàííûå íà ïîíÿòèè ñîãëàñîâàííîñòè íåèíèöèàëüíûõ àâòîìà-
òîâ [8, 9], ìîãóò ïîòðåáîâàòü çíà÷èòåëüíî áîëüøåãî êîëè÷åñòâà âû÷èñëåíèé, ÷åì
îïèñàííûé âûøå ñïîñîá ïðåîáðàçîâàíèÿ èíèöèàëüíîãî àâòîìàòà.
ÑÏÈÑÎÊ ËÈÒÅÐÀÒÓÐÛ
1. 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.
2. 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. Colloq. on Automata, Languages, and Programming; Lect. Notes Comput. Sci. —
1989. — 372. — P. 1–17.
3. D i l l D . L . Trace theory for automatic hierarchical verification of speed independent circuits // Adv.
Res. in VLSI / J. Allen and F.T. Leighton (eds). — Cambridge: MIT Press, 1988. — P. 51–65.
4. A l f a r o L . d e , F a e l l a M . , M a j u m d a r R . , R a m a n V . Code aware resource management //
Proc. 5th Intern. ACM Conf. on Embedded Software (EMSOFT 05). — New York: ACM Press,
2005. — P. 191–202.
5. K r e m e r S . , R a s k i n J . - F . A game-based upsilon erification of non-repudiation and fair
exchange protocols // Proc. 12th Intern. Conf. on Concurrency Theory (CONCUR 01); Lect. Notes
Comput. Sci. — 2001. — 2154. — P. 551–565.
6. A l f a r o L . d e , H e n z i n g e r T . A . Interface theories for component-based design // 1st Intern.
Workshop on Embedded Software (EMSOFT 01); Lect. Notes Comput. Sci. — 2001. — 2211. —
P. 148–165.
7. × å á î ò à ð å â À . Í . Ðåãóëÿðíàÿ ôîðìà ñïåöèôèêàöèè äåòåðìèíèðîâàííûõ àâòîìàòîâ â ÿçûêå L
// Ïðèêëàä. äèñêðåò. ìàòåìàòèêà. — 2010. — ¹ 4. — Ñ. 64–72.
8. × å á î ò à ð å â À . Í . Âçàèìîäåéñòâèå àâòîìàòîâ // Êèáåðíåòèêà è ñèñòåìíûé àíàëèç. —
1991. — ¹ 6. — Ñ. 17–29.
9. × å á î ò à ð å â À . Í . Îáùèé ìåòîä ïðîâåðêè ñîãëàñîâàííîñòè âçàèìîäåéñòâóþùèõ àâòîìàòîâ
ñ êîíå÷íîé ïàìÿòüþ // Òàì æå. — 1999. — ¹ 6. — Ñ. 25–37.
10. L i c h t e n s t e i n O . , P n u e l i A . Checking that finite state concurrent programs satisfy their linear
specification // Proc. 12th ACM Symp. on Principles of Programming Languages. — New York:
ACM Press, 1985. — P. 97–107.
11. T h o m a s W . Automata on infinite objects // Handbook of Theoret. Comput. Sci. / J. van Leeuven
(ed.). — 1990. — P. 134–191.
12. F r i e d m a n n O . , L a n g e M . Solving parity games in practice // Lect. Notes Comput. Sci. —
2009. — 5799. — P. 182–196.
Ïîñòóïèëà 23.04.2013
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2014, òîì 50, ¹ 4 13
|