Проектирование реактивных алгоритмов путем решения уравнений над автоматами
Розглядається задача розв’язання нерівностей над автоматами, яка виникає при композиційному підході до проектування реактивних систем. Задача формулюється та розв’язується на рівні специфікацій автоматів логічною мовою L. Показано, як одержати максимальний розв’язок нерівності відносно операції синх...
Збережено в:
| Опубліковано в: : | Кибернетика и системный анализ |
|---|---|
| Дата: | 2012 |
| Автор: | |
| Формат: | Стаття |
| Мова: | Російська |
| Опубліковано: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2012
|
| Теми: | |
| Онлайн доступ: | https://nasplib.isofts.kiev.ua/handle/123456789/84120 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Цитувати: | Проектирование реактивных алгоритмов путем решения уравнений над автоматами / А.Н. Чеботарев // Кибернетика и системный анализ. — 2012. — Т. 48, № 4. — С. 3-13. — Бібліогр.: 9 назв. — рос. |
Репозитарії
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1860107524917690368 |
|---|---|
| author | Чеботарев, А.Н. |
| author_facet | Чеботарев, А.Н. |
| citation_txt | Проектирование реактивных алгоритмов путем решения уравнений над автоматами / А.Н. Чеботарев // Кибернетика и системный анализ. — 2012. — Т. 48, № 4. — С. 3-13. — Бібліогр.: 9 назв. — рос. |
| collection | DSpace DC |
| container_title | Кибернетика и системный анализ |
| description | Розглядається задача розв’язання нерівностей над автоматами, яка виникає при композиційному підході до проектування реактивних систем. Задача формулюється та розв’язується на рівні специфікацій автоматів логічною мовою L. Показано, як одержати максимальний розв’язок нерівності відносно операції синхронної композиції автоматів. Іл.: 3. Бібліогр.: 9 назв.
The problem of solving inequalities over finite state machines (FSMs) is considered. This problem arises in the compositional approach to the design of reactive systems. The problem is formulated and solved at the level of FSM specifications in the logical language L. We show how to compute the maximal solution to the inequality with respect to the operation of synchronous composition of FSMs.
|
| first_indexed | 2025-12-07T17:32:29Z |
| format | Article |
| fulltext |
À.Í. ×ÅÁÎÒÀÐÅÂ
ÓÄÊ 519.731.1 ÏÐÎÅÊÒÈÐÎÂÀÍÈÅ ÐÅÀÊÒÈÂÍÛÕ ÀËÃÎÐÈÒÌÎÂ
ÏÓÒÅÌ ÐÅØÅÍÈß ÓÐÀÂÍÅÍÈÉ
ÍÀÄ ÀÂÒÎÌÀÒÀÌÈ
Êëþ÷åâûå ñëîâà: ðåàêòèâíàÿ ñèñòåìà, ñïåöèôèêàöèÿ â ÿçûêå L, �-àâòîìàò,
ñèíõðîííàÿ êîìïîçèöèÿ �-àâòîìàòîâ, íåðàâåíñòâî íàä �-àâòîìàòàìè, ìàêñè-
ìàëüíîå ðåøåíèå.
ÂÂÅÄÅÍÈÅ
Ïðîåêòèðîâàíèå ñîâðåìåííûõ ñèñòåì îáðàáîòêè èíôîðìàöèè âñå áîëüøå óñëîæ-
íÿåòñÿ â ñâÿçè ñ óñëîæíåíèåì ýòèõ ñèñòåì. Îäíèì èç îñíîâíûõ ñïîñîáîâ áîðüáû
ñî ñëîæíîñòüþ ïðîåêòèðîâàíèÿ ÿâëÿåòñÿ ìîäóëüíûé ïîäõîä, ñâÿçàííûé ñ äå-
êîìïîçèöèåé ïðîåêòèðóåìîé ñèñòåìû íà ïîäñèñòåìû, êîòîðûå âçàèìîäåéñòâóþò
ìåæäó ñîáîé â ñîîòâåòñòâèè ñ îïðåäåëåííûìè ïðàâèëàìè êîìïîçèöèè [1–3].
Ìíîãèå çàäà÷è, âîçíèêàþùèå ïðè òàêîì ïîäõîäå ê ïðîåêòèðîâàíèþ, ìîãóò
áûòü ñôîðìóëèðîâàíû ñëåäóþùèì îáðàçîì. Çàäàíû ñïåöèôèêàöèÿ ñèñòåìû,
êîòîðàÿ ðåàëèçóåòñÿ â âèäå êîìïîçèöèè äâóõ ìîäóëåé, è ñïåöèôèêàöèÿ îäíîãî
èç ýòèõ ìîäóëåé. Òðåáóåòñÿ îïðåäåëèòü (ñïåöèôèöèðîâàòü) äðóãîé ìîäóëü òàê,
÷òîáû åãî êîìïîçèöèÿ ñ çàäàííûì ìîäóëåì óäîâëåòâîðÿëà ñïåöèôèêàöèè ñèñ-
òåìû. Äëÿ óòî÷íåíèÿ ýòîé çàäà÷è íåîáõîäèìî:
1) îïðåäåëèòü ñïîñîá ïðåäñòàâëåíèÿ ñïåöèôèêàöèé îòäåëüíûõ ìîäóëåé è
âñåé ñèñòåìû â öåëîì;
2) óòî÷íèòü ïîíÿòèå êîìïîçèöèè ìîäóëåé;
3) óòî÷íèòü îòíîøåíèå, ñîîòâåòñòâóþùåå ïîíÿòèþ «ìîäóëü óäîâëåòâîðÿåò
ñïåöèôèêàöèè».
Óêàçàííûå óòî÷íåíèÿ áóäóò ñäåëàíû äëÿ ðåàêòèâíûõ ñèñòåì [4], ò.å. ñèñòåì,
ïîñòîÿííî âçàèìîäåéñòâóþùèõ ñ îêðóæàþùåé ñðåäîé. Äëÿ èõ ñïåöèôèêàöèè áó-
äåò èñïîëüçîâàòüñÿ ÿçûê L [5], ïðåäñòàâëÿþùèé ñîáîé ôðàãìåíò ëîãèêè ïðåäèêà-
òîâ ïåðâîãî ïîðÿäêà ñ îäíîìåñòíûìè ïðåäèêàòàìè, êîòîðûå èíòåðïðåòèðóþòñÿ
íà ìíîæåñòâå Z öåëûõ ÷èñåë. Ðàññìàòðèâàåìàÿ çàäà÷à ñâîäèòñÿ ê ðåøåíèþ óðàâ-
íåíèé (íåðàâåíñòâ) íàä àâòîìàòíûìè ìîäåëÿìè âçàèìîäåéñòâóþùèõ ìîäóëåé,
ïðåäñòàâëåííûõ ñïåöèôèêàöèÿìè â ÿçûêå L . Ïîñêîëüêó àâòîìàòíûå ìîäåëè
îïðåäåëÿþò ïîâåäåíèå ìîäóëÿ, ðàáîòàþùåãî ïîòåíöèàëüíî áåñêîíå÷íî, ðàññìàò-
ðèâàþòñÿ àâòîìàòû íàä áåñêîíå÷íûìè âõîäíûìè ïîñëåäîâàòåëüíîñòÿìè, ÷òî ñî-
îòâåòñòâóåò ïîíÿòèþ öèêëè÷åñêîãî àâòîìàòà.
ßÇÛÊ ÑÏÅÖÈÔÈÊÀÖÈÈ L
Ñïåöèôèêàöèÿ â ÿçûêå L èìååò âèä �tF t( ), ãäå F t( ) — ôîðìóëà, ïîñòðîåííàÿ
ñ ïîìîùüþ ëîãè÷åñêèõ ñâÿçîê èç àòîìàðíûõ ôîðìóë (àòîìîâ) âèäà p t k( )� ,
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2012, ¹ 4 3
© À.Í. ×åáîòàðåâ, 2012
ãäå p — îäíîìåñòíûé ïðåäèêàòíûé ñèìâîë, t — ïåðåìåííàÿ, ïðèíèìàþùàÿ
çíà÷åíèÿ èç ìíîæåñòâà öåëûõ ÷èñåë, ðàññìàòðèâàåìîãî êàê ìíîæåñòâî ìîìåí-
òîâ äèñêðåòíîãî âðåìåíè, à k — öåëî÷èñëåííàÿ êîíñòàíòà, íàçûâàåìàÿ ðàíãîì
àòîìà. Ðàçíîñòü ìåæäó ìàêñèìàëüíûì è ìèíèìàëüíûì çíà÷åíèÿìè ðàíãîâ àòî-
ìîâ, âñòðå÷àþùèõñÿ â ôîðìóëå, íàçûâàåòñÿ åå ãëóáèíîé.  äàëüíåéøåì ôîð-
ìóëû ÿçûêà L âèäà �tF t( ) áóäåì íàçûâàòü L-ôîðìóëàìè.
Ïðè îïðåäåëåíèè ñåìàíòèêè ÿçûêîâ ñïåöèôèêàöèè ðåàêòèâíûõ ñèñòåì òàêèå
ÿçûêè ðàññìàòðèâàþòñÿ êàê ôîðìàëèçìû äëÿ çàäàíèÿ ìíîæåñòâ ñâåðõñëîâ (áåñ-
êîíå÷íûõ ñëîâ) â àëôàâèòå äâîè÷íûõ âåêòîðîâ, äëèíà êîòîðûõ ðàâíà êîëè÷åñòâó
ðàçëè÷íûõ ïðåäèêàòíûõ ñèìâîëîâ, âñòðå÷àþùèõñÿ â ñïåöèôèêàöèè. Îïðåäåëèì
íåîáõîäèìûå ïîíÿòèÿ, êàñàþùèåñÿ ñâåðõñëîâ.
Ïóñòü � — êîíå÷íûé àëôàâèò, 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 u u k( ) ( )... ( )� � �� �1
äâóñòîðîííåãî ñâåðõñëîâà u îáîçíà÷àåòñÿ u k( , )� � � . Áåñêîíå÷íûé îòðåçîê
u k( , )�
1 áóäåì íàçûâàòü k-ñóôôèêñîì äâóñòîðîííåãî ñâåðõñëîâà u . Ìíîæåñòâî
âñåõ äâóñòîðîííèõ ñâåðõñëîâ â àëôàâèòå � áóäåì îáîçíà÷àòü �Z .
Ïåðåéäåì ê îïèñàíèþ ñåìàíòèêè ÿçûêà L . Êàæäîé L -ôîðìóëå F tF t� � ( )
ñòàâèòñÿ â ñîîòâåòñòâèå ìíîæåñòâî ìîäåëåé äëÿ ýòîé ôîðìóëû, ò.å. ìíîæåñòâî
òàêèõ èíòåðïðåòàöèé, íà êîòîðûõ F èñòèííà. Ïóñòü � � { }p pm1, ..., — ìíîæåñò-
âî âñåõ ïðåäèêàòíûõ ñèìâîëîâ, âñòðå÷àþùèõñÿ â ôîðìóëå F (ñèãíàòóðà ôîðìó-
ëû). Èíòåðïðåòàöèÿ ôîðìóëû F — ýòî óïîðÿäî÷åííûé íàáîð îïðåäåëåííûõ íà Z
îäíîìåñòíûõ ïðåäèêàòîâ � �1� �� m , ñîîòâåòñòâóþùèõ ïðåäèêàòíûì ñèìâîëàì
èç � . Ïóñòü � — ìíîæåñòâî âñåõ äâîè÷íûõ âåêòîðîâ äëèíû m , òîãäà èíòåðïðå-
òàöèþ I m�
� � �� �1 � ìîæíî ïðåäñòàâèòü â âèäå äâóñòîðîííåãî ñâåðõñëîâà â àë-
ôàâèòå � , à ìíîæåñòâî âñåõ ìîäåëåé äëÿ F — â âèäå ìíîæåñòâà M F( ) äâóñòî-
ðîííèõ ñâåðõñëîâ â ýòîì àëôàâèòå.  äàëüíåéøåì íå áóäåì ðàçëè÷àòü èíòåðïðå-
òàöèè è ñîîòâåòñòâóþùèå èì äâóñòîðîííèå ñâåðõñëîâà, ïîýòîìó áóäåì ãîâîðèòü
îá èñòèííîñòè ôîðìóëû F íà äâóñòîðîííåì ñâåðõñëîâå u ��Z .
Ïðè èíòåðïðåòàöèè ôîðìóë âèäà �tF t( ) íà ìíîæåñòâå öåëûõ ÷èñåë äëÿ ëþáî-
ãî k �Z ñïðàâåäëèâà ýêâèâàëåíòíîñòü � � � �tF t tF t k( ) ( ) , ãäå F t k( )� îáîçíà÷à-
åò ôîðìóëó, ïîëó÷åííóþ èç F t( ) ïóòåì äîáàâëåíèÿ k ê ðàíãàì âñåõ åå àòîìîâ
(ñäâèã íà k). Òàêèì îáðàçîì, ìîæíî îãðàíè÷èòüñÿ ðàññìîòðåíèåì ôîðìóë, ó êîòî-
ðûõ ìàêñèìàëüíûé ðàíã àòîìîâ ðàâåí íóëþ. Áóäåì ñ÷èòàòü, ÷òî L-ôîðìóëà
F tF t� � ( ) çàäàåò ìíîæåñòâî 0-ñóôôèêñîâ âñåõ äâóñòîðîííèõ ñâåðõñëîâ èç M F( ).
Îáîçíà÷èì ýòî ìíîæåñòâî W F( ).
ÀÂÒÎÌÀÒÍÀß ÑÅÌÀÍÒÈÊÀ ßÇÛÊÀ L
Îïðåäåëåíèå 1. Êîíå÷íûé íåèíèöèàëüíûé X Y -àâòîìàò A — ýòî ÷åòâåðêà
�X Y Q A, , , � , ãäå X Y Q, , — êîíå÷íûå ìíîæåñòâà ñîîòâåòñòâåííî âõîäíûõ
ñèìâîëîâ, âûõîäíûõ ñèìâîëîâ è ñîñòîÿíèé, à �A
QQ X Y: � � � 2 — ôóíêöèÿ
ïåðåõîäîâ àâòîìàòà. X Y -àâòîìàò A íàçûâàåòñÿ êâàçèäåòåðìèíèðîâàííûì, åñëè
äëÿ ëþáûõ q Q� x X� , y Y� | ( , , ) |�A q x y � 1. Êâàçèäåòåðìèíèðîâàííûå
X Y -àâòîìàòû óäîáíî ðàññìàòðèâàòü êàê äåòåðìèíèðîâàííûå ÷àñòè÷íûå àâòîìà-
òû áåç âûõîäà, ñ âõîäíûì àëôàâèòîì � � �X Y . Òàêîé àâòîìàò A Q A�
��, , � ,
ãäå �A Q Q: � �� — ÷àñòè÷íàÿ ôóíêöèÿ, áóäåì íàçûâàòü �-àâòîìàòîì.
Îïðåäåëåíèå 2. �-àâòîìàò A Q A�
��, , � íàçûâàåòñÿ öèêëè÷åñêèì, åñëè äëÿ
êàæäîãî q Q� ñóùåñòâóþò òàêèå � �1 2, �� è q q Q1 2, � , ÷òî q qA1 1� � �( , ) è
q qA� � �( , )2 2 .
4 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2012, ¹ 4
 äàëüíåéøåì ïîä àâòîìàòîì áóäåì ïîíèìàòü öèêëè÷åñêèé �-àâòîìàò. Òàêîé
àâòîìàò ìîæíî îäíîçíà÷íî îõàðàêòåðèçîâàòü â òåðìèíàõ äîïóñòèìûõ ñâåðõñëîâ.
Îïðåäåëåíèå 3. Ñâåðõñëîâî 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 , åñëè îíî äîïóñòèìî õîòÿ áû â îäíîì èç åãî ñîñòîÿíèé. Ìíîæåñòâî âñåõ
ñâåðõñëîâ, äîïóñòèìûõ äëÿ àâòîìàòà A, îáîçíà÷èì W A( ).
Äâà �-àâòîìàòà: A1 è A2 , áóäåì íàçûâàòü ýêâèâàëåíòíûìè (ñëàáî ýêâèâàëåí-
òíûìè), åñëè W A W A( ) ( )1 2� .
Ïðåäïîëàãàåòñÿ, ÷òî ñèìâîëû àëôàâèòà � ïðåäñòàâëÿþò ñîáîé äâîè÷íûå âåê-
òîðû äëèíû m , ÷òî ñîîòâåòñòâóåò êîäèðîâàíèþ àáñòðàêòíûõ ñèìâîëîâ íàáîðàìè
çíà÷åíèé äâîè÷íûõ ïåðåìåííûõ èç � � { }x xm1, ..., . Ýòèì ïåðåìåííûì ñîîòâå-
òñòâóþò ïðåäèêàòíûå ñèìâîëû â ñïåöèôèêàöèè àâòîìàòîâ.
Àâòîìàòíàÿ ñåìàíòèêà ÿçûêà L îïðåäåëÿåòñÿ ñëåäóþùåé òåîðåìîé.
Òåîðåìà 1 [5]. Äëÿ âñÿêîé íåïðîòèâîðå÷èâîé ôîðìóëû F âèäà �tF t( ) ñóùåñò-
âóåò â îáùåì ñëó÷àå ÷àñòè÷íûé íåèíèöèàëüíûé öèêëè÷åñêèé àâòîìàò A ñ êîíå÷-
íîé ïàìÿòüþ [6], äëÿ êîòîðîãî ìíîæåñòâî âñåõ äîïóñòèìûõ ñâåðõñëîâ ñîâïàäàåò
ñ ìíîæåñòâîì ñâåðõñëîâ, çàäàâàåìûõ ôîðìóëîé F .
Òàêîé àâòîìàò íàçîâåì àâòîìàòîì, ñïåöèôèöèðóåìûì ôîðìóëîé F .
Áóäåì ãîâîðèòü, ÷òî àâòîìàò A óäîâëåòâîðÿåò ñïåöèôèêàöèè F , åñëè
W A W F( ) ( )� .
Ïðè îïðåäåëåíèè ìíîæåñòâà ñâåðõñëîâ, çàäàâàåìîãî ôîðìóëîé F tF t� � ( ),
à ñëåäîâàòåëüíî, è ìíîæåñòâà ñâåðõñëîâ, äîïóñòèìûõ äëÿ ñïåöèôèöèðóåìîãî
åþ àâòîìàòà, óäîáíî èñïîëüçîâàòü ïîíÿòèå ïðîñòðàíñòâà ñîñòîÿíèé äëÿ ýòîé
ôîðìóëû [5]. Ïóñòü � — ñèãíàòóðà ôîðìóëû F t( ), à r — åå ãëóáèíà. Îáîçíà÷èì
� �( ) ìíîæåñòâî âñåõ äâîè÷íûõ âåêòîðîâ äëèíû | |� , ãäå | |� — ìîùíîñòü ìíî-
æåñòâà � . Ïîñëåäîâàòåëüíîñòü s s sr0 1... âåêòîðîâ èç � �( ) íàçîâåì ñîñòîÿíèåì
ãëóáèíû r, à ìíîæåñòâî Q r( , )� âñåõ òàêèõ ïîñëåäîâàòåëüíîñòåé — ïðîñòðàí-
ñòâîì ñîñòîÿíèé ãëóáèíû r äëÿ ôîðìóëû F t( ) . Íà ìíîæåñòâå Q r( , )� îïðåäåëèì
îòíîøåíèå N íåïîñðåäñòâåííîãî ñëåäîâàíèÿ òàê, ÷òî çà êàæäûì ñîñòîÿíèåì
q s s sr� 0 1... íåïîñðåäñòâåííî ñëåäóþò 2| |� ñîñòîÿíèé âèäà s s sr1... , ãäå s�� �( ) .
Ìíîæåñòâî âñåõ ñîñòîÿíèé, íåïîñðåäñòâåííî ñëåäóþùèõ çà q, îáîçíà÷èì N q( ).
Åñëè êîìïîíåíòû âåêòîðà si â ñîñòîÿíèè q s s sr� 0 1... ðàññìàòðèâàòü êàê èñòèí-
íîñòíûå çíà÷åíèÿ ñîîòâåòñòâóþùèõ àòîìîâ ðàíãà i r ïðè íåêîòîðîì óïîðÿäî÷å-
íèè ìíîæåñòâà � , òî ìîæíî ãîâîðèòü î çíà÷åíèè ôîðìóëû F t( ) íà ñîñòîÿíèè q.
Ôîðìóëó F t( ) áóäåì ðàññìàòðèâàòü êàê ïðåäñòàâëåíèå ìíîæåñòâà Q F t( ( )) ñîñòî-
ÿíèé èç Q r( , )� , à èìåííî, òåõ ñîñòîÿíèé, íà êîòîðûõ îíà èñòèííà. Àíàëîãè÷íî
ïðè r r1 � è � �1 � ìîæíî ãîâîðèòü î ìíîæåñòâå ñîñòîÿíèé, çàäàâàåìîì ôîðìó-
ëîé F t( ) â ïðîñòðàíñòâå Q r( , )1 1� . Îáîçíà÷èì ýòî ìíîæåñòâî Q F t r( ( ), , )1 1� .
Ïóñòü G F t( ( )) — ãðàô îãðàíè÷åíèÿ îòíîøåíèÿ N íà ìíîæåñòâî Q F t( ( )) . Ñîîò-
âåòñòâóþùèé ãðàô â ïðîñòðàíñòâå ñîñòîÿíèé Q r( , )1 1� áóäåì îáîçíà÷àòü
G F t r( ( ), , )1 1� . Ãðàô G V E�
�, , ãäå V — ìíîæåñòâî âåðøèí, à E — ìíîæåñòâî
äóã ãðàôà, íàçîâåì öèêëè÷åñêèì, åñëè äëÿ êàæäîé åãî âåðøèíû q ñóùåñòâóþò òà-
êèå âåðøèíû q1 è q2 , ÷òî äóãè ( , )q q1 è ( , )q q2 ïðèíàäëåæàò E .
Íåñëîæíî óáåäèòüñÿ â ñïðàâåäëèâîñòè ñëåäóþùåé ëåììû, êîòîðóþ ïðèâå-
äåì áåç äîêàçàòåëüñòâà.
Ëåììà 1. Ïóñòü G F t* ( ( )) — ìàêñèìàëüíûé öèêëè÷åñêèé ïîäãðàô ãðàôà
G F t( ( )), òîãäà � � �tF t tF t* ( ) ( ) , ãäå F t* ( ) — ôîðìóëà, çàäàþùàÿ ìíîæåñòâî
ñîñòîÿíèé, ñîîòâåòñòâóþùåå âñåì âåðøèíàì ãðàôà G F t* ( ( )).
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2012, ¹ 4 5
Åñëè ñâåðõñëîâî l ïðèíàäëåæèò W F( ) , òî åìó ñîîòâåòñòâóåò áåñêîíå÷íûé ìàð-
øðóò â ãðàôå G F t* ( ( )) è, íàîáîðîò, êàæäîìó áåñêîíå÷íîìó ìàðøðóòó â G F t* ( ( ))
ñîîòâåòñòâóåò ñâåðõñëîâî, ïðèíàäëåæàùåå W F( ) . Òàêèì îáðàçîì, ìíîæåñòâî
ñâåðõñëîâ, äîïóñòèìûõ äëÿ � -àâòîìàòà, ñïåöèôèöèðîâàííîãî ôîðìóëîé
F tF t� � ( ), îäíîçíà÷íî îïðåäåëÿåòñÿ ìíîæåñòâîì V F* ( ) âåðøèí ãðàôà G F t* ( ( )).
ÑÈÍÕÐÎÍÍÀß ÊÎÌÏÎÇÈÖÈß ÀÂÒÎÌÀÒÎÂ
Ïóñòü A Q1 1 1�
��, , � è A Q2 2 2�
��, , � — öèêëè÷åñêèå �-àâòîìàòû ñ îäíèì
è òåì æå âõîäíûì àëôàâèòîì � . Ñèíõðîííîé êîìïîçèöèåé àâòîìàòîâ A1 è A2
(îáîçíà÷àåòñÿ A A1 2� ) íàçîâåì ìàêñèìàëüíûé öèêëè÷åñêèé ïîäàâòîìàò àâòî-
ìàòà C QC C�
��, , � , îïðåäåëÿåìîãî ñëåäóþùèì îáðàçîì: Q Q QC � �1 2 , çíà-
÷åíèå � �C q q( , , )
�1 2 , ãäå q Q1 1� , q Q2 2� , � �� , îïðåäåëåíî è ðàâíî
�� � � �1 1 2 2( , ), ( , )q q òîãäà è òîëüêî òîãäà, êîãäà çíà÷åíèÿ � �1 1( , )q è
� �2 2( , )q îïðåäåëåíû. Ïóñòü FA è FB — ñïåöèôèêàöèè â ÿçûêå L ñîîòâå-
òñòâåííî àâòîìàòîâ A è B, òîãäà ôîðìóëà F FA B& ñïåöèôèöèðóåò àâòîìàò
A B� . Çàìåòèì, ÷òî �-àâòîìàòû A QA A A�
�� , , � è B QB B B�
�� , , � , ãäå
� � �A A� ( ), à � � �B B� ( ), ìîæíî ðàññìàòðèâàòü êàê �-àâòîìàòû íàä îäíèì
è òåì æå àëôàâèòîì � � � �� �( )A B . Ïðè ýòîì êàæäûé ñèìâîë � �� �( )A
ðàññìàòðèâàåòñÿ êàê ìíîæåñòâî { }� � �� � � �| ( \ )� � �B A . Àíàëîãè÷íûì îáðà-
çîì ðàññìàòðèâàþòñÿ ñèìâîëû àëôàâèòà � �( )B Ýòî ïîçâîëÿåò ïðèâåäåííîå
âûøå îïðåäåëåíèå ñèíõðîííîé êîìïîçèöèè àâòîìàòîâ åñòåñòâåííûì îáðàçîì
ðàñïðîñòðàíèòü íà �-àâòîìàòû ñ ðàçëè÷àþùèìèñÿ àëôàâèòàìè. Ïóñòü A — àâ-
òîìàò íàä àëôàâèòîì � �( ) è � �� 1. Ìíîæåñòâî ñâåðõñëîâ, äîïóñòèìûõ äëÿ
àâòîìàòà A, ðàññìàòðèâàåìîãî êàê àâòîìàò íàä � �( )1 , îáîçíà÷èì W A�1
( ) .
Âåêòîð � �� �( ) áóäåì ðàññìàòðèâàòü êàê îòîáðàæåíèå � : ,� � { }0 1 . Ïðî-
åêöèåé � �� �( ) íà � �1 � (îáîçíà÷àåòñÿ [ ]� �1
) íàçûâàåòñÿ îãðàíè÷åíèå îòîáðà-
æåíèÿ � íà ìíîæåñòâî �1. Ïîíÿòèå ïðîåêöèè ñèìâîëà àëôàâèòà � �( ) ðàñïðîñ-
òðàíèì íà ñâåðõñëîâà è ìíîæåñòâà ñâåðõñëîâ â ýòîì àëôàâèòå. Ïóñòü l � � �1 2� ,
ãäå � i �� �( ) . Ïðîåêöèþ ýòîãî ñâåðõñëîâà íà � �1 � îïðåäåëèì êàê
[ ] [ ] [ ]l � � �1 1 11 2� � � � . Ïðîåêöèþ ìíîæåñòâà ñâåðõñëîâ W â àëôàâèòå � �( ) íà
�1 îáîçíà÷èì [ ]W �1
.
Îïðåäåëåíèå 4. Îãðàíè÷åíèåì àâòîìàòà A Q�
�� �( ), , � íà ìíîæåñòâî ïå-
ðåìåííûõ (ïðåäèêàòíûõ ñèìâîëîâ) � �1 � áóäåì íàçûâàòü àâòîìàò
A Q1 1 1�
�� , , � , ãäå � � �1 1� ( ), è q q1 1 1�� �( , ) òîãäà è òîëüêî òîãäà, êîãäà ñó-
ùåñòâóåò òàêîå � �� �( ) , ÷òî [ ]� ��1 1� è � �( , )q q� 1. Îãðàíè÷åíèå àâòîìàòà A
íà �1îáîçíà÷èì [ ]A �1
.
Íåòðóäíî âèäåòü, ÷òî W A W A([ ] ) [ ( )]� �1 1
� , ò.å. ìíîæåñòâî ñâåðõñëîâ, äî-
ïóñòèìûõ äëÿ îãðàíè÷åíèÿ àâòîìàòà A íà �1, ñîâïàäàåò ñ ïðîåêöèåé íà �1 ìíî-
æåñòâà ñâåðõñëîâ, äîïóñòèìûõ äëÿ àâòîìàòà A . Çà-
ìåòèì òàêæå, ÷òî W A W A( ) ([ ] )� � �1
.
Ðàññìîòðèì ñòðóêòóðó, ïðåäñòàâëåííóþ íà
ðèñ. 1. Çäåñü I I U1 2, , è ò.ä. — ìíîæåñòâà äâîè÷-
íûõ ïåðåìåííûõ, ïðè÷åì ïåðåñå÷åíèÿ I I1 2� ,
U O� 1, V O� 2 ìîãóò áûòü íåïóñòûìè.
Ïóñòü A QA A A�
�� �( ), , � , ãäå � A I� �1
� � �O V U1 , à B QB B B�
�� �( ), , � , ãäå
� B I O V U� � � �2 2 . Äëÿ òàêîé ñòðóêòóðû
âíåøíåé ñèíõðîííîé êîìïîçèöèåé àâòîìàòîâ A è
B (îáîçíà÷àåòñÿ A B� ) áóäåì íàçûâàòü îãðàíè÷åíèå �-àâòîìàòà A B� íà ìíîæå-
ñòâî ïåðåìåííûõ �C I I O O� � � �1 2 1 2 .
6 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2012, ¹ 4
A
B
U V
I1
I2
O1
O2
Ðèñ. 1
ÍÅÐÀÂÅÍÑÒÂÀ ÍÀÄ ÀÂÒÎÌÀÒÀÌÈ
Íà ìíîæåñòâå �-àâòîìàòîâ ñ îäíèì è òåì æå âõîäíûì àëôàâèòîì îïðåäåëèì
îòíîøåíèå «�» ñëåäóþùèì îáðàçîì: A B� òîãäà è òîëüêî òîãäà, êîãäà
W A W B( ) ( )� .
Ïóñòü äëÿ ïðèâåäåííîé âûøå ñòðóêòóðû çàäàíû �-àâòîìàòû
A QA A A�
�� �( ), , � è C QC C C�
�� �( ), , � , ãäå �C I I O O� � � �1 2 1 2 . Ðàñ-
ñìîòðèì íåðàâåíñòâî A X C� � . Çäåñü X — íåèçâåñòíîå, ïðèíèìàþùåå çíà÷å-
íèÿ èç ìíîæåñòâà öèêëè÷åñêèõ � -àâòîìàòîâ ñ âõîäíûì àëôàâèòîì
� ( )I O V U2 2� � � . Òàêèì îáðàçîì, � -àâòîìàò B åñòü ðåøåíèå ðàññìàòðèâàåìî-
ãî íåðàâåíñòâà, åñëè W A B W C
C
([ ] ) ( )� �� . Çàäà÷à ñîñòîèò â íàõîæäåíèè ìàêñè-
ìàëüíîãî ðåøåíèÿ íåðàâåíñòâà A X C� � èëè óðàâíåíèÿ A X C� � . Ïîñêîëüêó
çàäà÷à ðàññìàòðèâàåòñÿ íà óðîâíå ñïåöèôèêàöèé àâòîìàòîâ â ÿçûêå L, ðåøåíèå
èùåòñÿ â êëàññå öèêëè÷åñêèõ àâòîìàòîâ ñ êîíå÷íîé ïàìÿòüþ.  ýòîì ñëó÷àå ìàê-
ñèìàëüíûì ðåøåíèåì íàçîâåì òàêîå ðåøåíèå B, ÷òî íå ñóùåñòâóåò íèêàêîãî äðó-
ãîãî, íåýêâèâàëåíòíîãî åìó àâòîìàòà B1, òàêæå ÿâëÿþùåãîñÿ ðåøåíèåì, è òàêîãî,
÷òî B B� 1. ×òîáû ñôîðìóëèðîâàòü ýòó çàäà÷ó íà óðîâíå ñïåöèôèêàöèé, îïðåäå-
ëèì ïîíÿòèå ìèíèìàëüíîé ôîðìû ôîðìóëû F t( ) â ñïåöèôèêàöèè F tF t� � ( ).
Ïóñòü F tF t� � ( ) — íåïðîòèâîðå÷èâàÿ ôîðìóëà ãëóáèíû r ñ ñèãíàòóðîé
� � { }p pq1, ..., . Ôîðìóëó F t( ) áóäåì ðàññìàòðèâàòü êàê ïðîïîçèöèîíàëüíóþ
ôîðìóëó ñ ïðîïîçèöèîíàëüíûìè ïåðåìåííûìè p t p t p tq1 1 1( ), ..., ( ), ( ), ...
..., ( )p tq 1 , …, p t r p t rq1 ( ), ..., ( ) . Ìèíèìàëüíîé ôîðìîé ôîðìóëû F t( ) â ïðî-
ñòðàíñòâå ñîñòîÿíèé Q r( , )1 1� , ãäå r r1 � è � �1 � , íàçûâàåòñÿ ôîðìóëà
min ( ( ), , )F t r1 1� , çàäàþùàÿ ìíîæåñòâî âñåõ âåðøèí ãðàôà G F t r* ( ( ), , )1 1� . Ïðè
� �1 � áóäåì ãîâîðèòü î ìèíèìàëüíîé ôîðìå ïîðÿäêà r1 ôîðìóëû F t( ) è îáîçíà-
÷àòü åå min ( ( ))
r
F t1 , à åñëè, êðîìå òîãî, r r1 � , òî áóäåì ïèñàòü ïðîñòî min( ( ))F t
1.
Åñëè F tmin ( ) — ìèíèìàëüíàÿ ôîðìà ôîðìóëû F t( ), òî F t F tmin ( ) ( )� .
Ïîñòðîåíèå ìèíèìàëüíîé ôîðìû ôîðìóëû F t( ) ñîñòîèò â åå ïðåîáðàçîâàíèè,
îïèñàííîì â [7].
Òåïåðü îïðåäåëèì îòíîøåíèå íà ñïåöèôèêàöèÿõ, ñîîòâåòñòâóþùåå îòíîøå-
íèþ A B� íà öèêëè÷åñêèõ �-àâòîìàòàõ. Ïóñòü F tF tA A� � ( ) è F tF tB B� � ( ) —
ôîðìóëû îäíîé è òîé æå ñèãíàòóðû, ñïåöèôèöèðóþùèå ñîîòâåòñòâåííî àâòîìà-
òû A è B. Îòíîøåíèþ W A W B( ) ( )� ñîîòâåòñòâóåò îòíîøåíèåV F V FA B
* *( ) ( )�
íà ìíîæåñòâàõ âåðøèí ãðàôîâ G F tA
* ( ( )) è G F tB
* ( ( )). Â òåðìèíàõ ñïåöèôèêà-
öèé ýòî âûãëÿäèò êàê min( ( )) min( ( ))F t F tA B� èëè, ÷òî òî æå ñàìîå,
min ( ( )) ( )F t F tA B� , ãäå F tA ( ) è F tB ( ) ðàññìàòðèâàþòñÿ êàê ïðîïîçèöèîíàëü-
íûå ôîðìóëû. Åñëè ãëóáèíà r ôîðìóëû F tB ( ) ïðåâûøàåò ãëóáèíó ôîðìóëû
F tA ( ), òî äëÿ F tA ( ) ñëåäóåò ðàññìàòðèâàòü ìèíèìàëüíóþ ôîðìó ïîðÿäêà r.
Ïóñòü F tF tA A� � ( ) è F tF tC C� � ( ) — ñïåöèôèêàöèè ñîîòâåòñòâåííî àâòî-
ìàòîâ A QA A A�
�� �( ), , � è C QC C C�
�� �( ), , � , ãäå � �C A� . Óñëîâèþ
[ ]A C
C� � ñîîòâåòñòâóåò óñëîâèå W A W C
C
([ ] ) ( )� � . Ïîêàæåì, ÷òî ýòî âêëþ÷å-
íèå ðàâíîñèëüíî W A W C
A
( ) ( )� � . Ïðåäâàðèòåëüíî ïðèâåäåì äâà äîñòàòî÷íî
î÷åâèäíûõ óòâåðæäåíèÿ.
Óòâåðæäåíèå 1. Ïóñòü A è B — àâòîìàòû íàä � �( ) è � �� 1, òîãäà èç
W A W B( ) ( )� ñëåäóåò W A W B� �1 1
( ) ( )� .
Óòâåðæäåíèå 2. Ïóñòü A è B — àâòîìàòû íàä � �( ) è � �1 � , òîãäà èç
W A W B( ) ( )� ñëåäóåò [ ( )] [ ( )]W A W B� �1 1
� .
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2012, ¹ 4 7
1 Áîëåå òî÷íî ñëåäóåò ãîâîðèòü î ìèíèìàëüíîé ôîðìå ôîðìóëû �tF t( ), êîòîðàÿ èìååò âèä
�t F tmin ( ).
Ñîãëàñíî óòâåðæäåíèþ 1 èç W A W C
C
([ ] ) ( )� � ñëåäóåò W A W C
A C A� � �([ ] ) ( )� ,
èç ÷åãî â ñèëó W A W A
A C
( ) ([ ] )� � � ñëåäóåò W A W C
A
( ) ( )� � .  ñâîþ î÷åðåäü, èç
W A W C
A
( ) ( )� � ñîãëàñíî óòâåðæäåíèþ 2 ñëåäóåò [ ( )] [ ( )]W A W C
C A C� � �� , ÷òî
ðàâíîñèëüíî W A W C
C
([ ] ) ( )� � . Ýòî äîêàçûâàåò ðàâíîñèëüíîñòü ðàññìàòðèâàå-
ìûõ âêëþ÷åíèé. Òàêèì îáðàçîì, óñëîâèþ [ ]A C
C� � íà óðîâíå ñïåöèôèêàöèé ñî-
îòâåòñòâóåò ôîðìóëà min ( ( )) ( )r
A CF t F t� , ãäå r — íàèáîëüøàÿ èç ãëóáèí ôîð-
ìóë F tA ( ) è F tC ( ) . Çàìåòèì, ÷òî ôîðìóëà F tC ( ) , â çàâèñèìîñòè îò ðàññìàòðèâàå-
ìîé ñèãíàòóðû, çàäàåò êàê ìíîæåñòâî ñâåðõñëîâ W C( ), òàê è ìíîæåñòâî W C
A� ( ) .
Òåïåðü ðàññìàòðèâàåìóþ çàäà÷ó ìîæíî ïåðåôîðìóëèðîâàòü ñëåäóþùèì îá-
ðàçîì: íàéòè ìàêñèìàëüíîå ðåøåíèå F tX ( ) ñèãíàòóðû � B I O V U� � � �2 2 ,
óäîâëåòâîðÿþùåå ôîðìóëå min ( ( )& ( )) ( )F t F t F tA X C� . Çäåñü ïîíÿòèå ìàêñè-
ìàëüíîñòè ðåøåíèÿ èìååò äâà àñïåêòà. Ïåðâûé ñâÿçàí ñ ïîñòðîåíèåì êîìïîçè-
öèè, ñïåöèôèöèðóþùåé ìàêñèìàëüíóþ ÷àñòü àâòîìàòà C, ÷òî ñîîòâåòñòâóåò ðå-
øåíèþ óðàâíåíèÿ min ( ( )& ( )) min ( ( )& ( ))F t F t F t F tA X A C� , ãäå âñå ôîðìóëû
ðàññìàòðèâàþòñÿ â îäíîì è òîì æå ïðîñòðàíñòâå ñîñòîÿíèé ñèãíàòóðû
� � �� �A B . Î÷åâèäíî, ÷òî òàêèå çíà÷åíèÿ äëÿ F tX ( ) ñóùåñòâóþò — äîñòà-
òî÷íî â êà÷åñòâå çíà÷åíèÿ F tX ( ) âçÿòü ôîðìóëó F tC ( ) , ðàññìàòðèâàåìóþ íàä
� � �� �A B . Âñÿêîå òàêîå çíà÷åíèå F tX ( ) äàåò ìàêñèìàëüíîå çíà÷åíèå äëÿ
min ( ( )& ( ))F t F tA X , óäîâëåòâîðÿþùåå ñîîòâåòñòâóþùåé èìïëèêàöèè. Âòîðîé
àñïåêò ñâÿçàí ñ íåîäíîçíà÷íîñòüþ ñïåöèôèêàöèè àâòîìàòà ôîðìóëîé ÿçûêà L .
Ïîýòîìó èùåòñÿ òàêîå ðåøåíèå F tB ( ) ïðèâåäåííîãî âûøå óðàâíåíèÿ, ÷òî íå ñó-
ùåñòâóåò íèêàêîé äðóãîé, íåýêâèâàëåíòíîé åìó ôîðìóëû F t( ) , òàêæå ÿâëÿþ-
ùåéñÿ ðåøåíèåì ýòîãî óðàâíåíèÿ è òàêîé, ÷òî F t F tB ( ) ( )� . Èñêîìóþ ôîðìóëó
F tB ( ) áóäåì ñòðîèòü ñëåäóþùèì îáðàçîì. Ñíà÷àëà ïîëó÷èì ìàêñèìàëüíîå ðåøå-
íèå �F tB ( ) ñ ñèãíàòóðîé � � �� �A B , à çàòåì ïîñòðîèì ìàêñèìàëüíóþ ôîðìóëó
F tB ( ) ñèãíàòóðû � B , èìïëèöèðóþùóþ �F tB ( ) .
Âñÿêàÿ ôîðìóëà F t( ) ãëóáèíû r çàäàåò ìíîæåñòâî ñîñòîÿíèé â ñîîòâåòñòâó-
þùåì ïðîñòðàíñòâå ñîñòîÿíèé. Ìàêñèìàëüíîé ôîðìîé ôîðìóëû F t( ) íàçîâåì
òàêóþ ôîðìóëó, ÷òî äîáàâëåíèå ëþáîãî ñîñòîÿíèÿ ïðîñòðàíñòâà ñîñòîÿíèé ê çà-
äàâàåìîìó åþ ìíîæåñòâó ñîñòîÿíèé ïðèâîäèò ê ñïåöèôèêàöèè, íå ýêâèâàëåí-
òíîé ôîðìóëå �tF t( ) . Ñóùåñòâóåò îäíî (ñ òî÷íîñòüþ äî ýêâèâàëåíòíîñòè) ìèíè-
ìàëüíîå ïðåäñòàâëåíèå ñïåöèôèêàöèè îïðåäåëåííîé ãëóáèíû è ìíîãî ðàçëè÷-
íûõ ìàêñèìàëüíûõ ïðåäñòàâëåíèé. Ìíîæåñòâî âñåõ ìàêñèìàëüíûõ
ïðåäñòàâëåíèé ôîðìóëû F t( ) îáîçíà÷èì MAX( ( ))F t .
Òåïåðü ïîêàæåì, ÷òî ôîðìóëà
� � � �F t F t F t F tB A A C( ) (min ( ( ))) max (min ( ( ) & ( ))) ,
ãäå max ( ( ))F t — ëþáîå ìàêñèìàëüíîå ïðåäñòàâëåíèå ñîîòâåòñòâóþùåé ôîðìóëû,
åñòü ðåøåíèå, ò.å., ÷òî ôîðìóëà min ( ( )& ( )) ( )F t F t F tA B C� � òîæäåñòâåííî èñòèí-
íà. Ïðåäâàðèòåëüíî ïðèâåäåì íåêîòîðûå èñïîëüçóåìûå ïðè ýòîì ñîîòíîøåíèÿ:
min (min ( ( ))) min ( ( ))F t F t� ; (1)
min (max ( ( ))) min ( ( ))F t F t� ; (2)
min (min ( ( )) & ( )) min ( ( ) & ( ))F t F t F t F t1 2 1 2� ; (3)
min ( ( ) & ( )) (min ( ( )) & min ( ( )))F t F t F t F t1 2 1 2� ; (4)
(min ( ( )) min ( ( ))) min ( ( ) ( ))F t F t F t F t1 2 1 2� � � . (5)
8 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2012, ¹ 4
Î÷åâèäíî, ÷òî ôîðìóëà min ( ( ) & ( )) ( )F t F t F tA B C� � ðàâíîñèëüíà ôîðìóëå
min ( ( )& ( )) min ( ( )& ( ))F t F t F t F tA B A C� � . Ïîýòîìó ïîêàæåì, ÷òî ïðèâåäåííîå
âûøå çíà÷åíèå äëÿ �F tB ( ) óäîâëåòâîðÿåò ôîðìóëå
min ( ( )& ( )) min ( ( )& ( ))F t F t F t F tA B A C� � .
Ñîãëàñíî (3)
min ( ( )& ( )) min (min ( ( ))& ( ))F t F t F t F tA B A B� � � .
Ïîäñòàâèâ ôîðìóëó �F tB ( ) â ïðàâóþ ÷àñòü ýòîé ýêâèâàëåíòíîñòè, ïîëó÷èì
min (min ( ( ))& max (min ( ( ) & ( ))))F t F t F tA A C .
 ñèëó (4) èìååì
min (min( ( )) & max (min ( ( ) & ( ))))F t F t F tA A C �
� min (min ( ( ))) & min (max (min ( ( ) & ( ))))F t F t F tA A C .
 ñèëó (1) è (2) ïðàâàÿ ÷àñòü ýòîé èìïëèêàöèè ðàâíà
min ( ( )) &min ( ( ) & ( ))F t F t F tA A C .
Î÷åâèäíî, ÷òî
min ( ( )) & min ( ( ) & ( )) min ( ( ) & ( ))F t F t F t F t F tA A C A C� .
Òàêèì îáðàçîì, min ( ( ) & ( )) min ( ( ) & ( ))F t F t F t F tA B A C� � , ÷òî è òðåáîâàëîñü
ïîêàçàòü.
Äîêàæåì, ÷òî ëþáîå òàêîå ðåøåíèå óäîâëåòâîðÿåò ïåðâîìó óñëîâèþ ìàêñè-
ìàëüíîñòè, ò.å., ÷òî min ( ( ) & ( )) min ( ( ) & ( ))F t F t F t F tA B A C� � . Äëÿ ýòîãî äîñòà-
òî÷íî ïîêàçàòü ñïðàâåäëèâîñòü ñîîòâåòñòâóþùåé èìïëèêàöèè â îáðàòíóþ ñòîðî-
íó, ò.å. min ( ( ) & ( )) min ( ( ) & ( ))F t F t F t F tA C A B� � . Äåéñòâèòåëüíî, â ñèëó (5)
èìååì
(min ( ( ) & (min ( ( )))) min ( ( ) & max (min ( ( ) &F t F t F t F tA A A A� � F tC ( ))))) �
� �min ( ( )& ( ))F t F tA B .
Ïîñêîëüêó min ( (min ( ( ))))� �F tA 0 , òî â ñèëó (4)
min ( ( ) & (min ( ( ))))F t F tA A� � 0 .
Îñòàåòñÿ ïîêàçàòü, ÷òî
min ( ( ) & max (min ( ( ) & ( )))) min ( ( ) & ( ))F t F t F t F t F tA A C A C� .
Òàê êàê min ( ( ) & ( ))F t F tA C âëå÷åò F tA ( ) è max (min ( ( ) & ( ))F t F tA C , òî
min ( ( ) & ( ))F t F tA C âëå÷åò F t F t F tA A C( ) & max (min ( ( ) & ( ))), à ñëåäîâàòåëüíî, è
min ( ( ) & max(min ( ( ) & ( ))))F t F t F tA A C .
 ñèëó (4)
min ( ( ) & max (min ( ( ) & ( ))))F t F t F tA A C �
� (min (( ( )) & min (max (min ( ( ) & ( )))))F t F t F tA A C .
Ñîãëàñíî (1) è (2) min (max (min ( ( ) & ( )))) min ( ( ) & ( ))F t F t F t F tA C A C� . Òàêèì
îáðàçîì, ïðàâàÿ ÷àñòü ðàññìàòðèâàåìîé èìïëèêàöèè ðàâíà
min ( ( )) & min ( ( ) & ( )) min( ( ) & ( ))F t F t F t F t F tA A C A C� .
Ýòî çàâåðøàåò äîêàçàòåëüñòâî òîãî, ÷òî ðåøåíèå �F tB ( ) óäîâëåòâîðÿåò ïåðâîìó
óñëîâèþ ìàêñèìàëüíîñòè.
Òåïåðü ïîêàæåì, ÷òî äëÿ ëþáîãî ðåøåíèÿ F tB ( ) ñèãíàòóðû � , óäîâëåòâîðÿþùå-
ãî ïåðâîìó óñëîâèþ ìàêñèìàëüíîñòè, ñóùåñòâóåò òàêàÿ ìàêñèìàëüíàÿ ôîðìà ôîðìó-
ëû min ( ( ) & ( ))F t F tA B , ÷òî F t F t F t F tB A A C( ) ( (min ( ( ))) max(min ( ( ) & ( ))))� � � ,
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2012, ¹ 4 9
ò.å., ÷òî ìàêñèìàëüíîå ðåøåíèå â ñìûñëå îáîèõ àñïåêòîâ ýòîãî ïîíÿòèÿ ñîäåð-
æèòñÿ ñðåäè � �(min ( ( ))) (min ( ( ) & ( )))F t F t F tA A CMAX . Ïóñòü F tB ( ) — ïðîèç-
âîëüíîå ðåøåíèå, äëÿ êîòîðîãî min ( ( ) & ( )) min ( ( ) & ( ))F t F t F t F tA B A C� . ßñíî,
÷òî äëÿ ëþáîé ìàêñèìàëüíîé ôîðìû max (min ( ( ) & ( )))F t F tA C �
� max (min ( ( ) & ( )))F t F tA B . Ïðåäñòàâèì ýòî ðåøåíèå â âèäå
F t F t F t F t F tB A B A B( ) min ( ( )) & ( ) (min ( ( ))) & ( )� � � .
Äîñòàòî÷íî ïîêàçàòü, ÷òî min ( ( ))& ( ) max (min ( ( ) & ( )))F t F t F t F tA B A C� .
Ñëåäóåò îòìåòèòü, ÷òî äëÿ ëþáîé ôîðìóëû F t( ) ñóùåñòâóåò òàêàÿ ìàêñè-
ìàëüíàÿ ôîðìà ôîðìóëû min( ( ))F t , ÷òî F t F t( ) max (min ( ( )))� . Òàêèì îáðà-
çîì, äëÿ min( ( ))& ( )F t F tA B ñóùåñòâóåò òàêàÿ ìàêñèìàëüíàÿ ôîðìà
max (min (min ( ( )) & ( )))F t F tA B , ÷òî
min( ( )) & ( ) max(min(min( ( )) & ( )))F t F t F t F tA B A B� .
 ñèëó (3) ïðàâàÿ ÷àñòü ýòîé èìïëèêàöèè ðàâíà max (min ( ( ) & ( )))F t F tA B ,
à ñëåäîâàòåëüíî,
min ( ( )) & ( ) max(min (( ( )) & ( )))F t F t F t F tA B A C� .
Äðóãèìè ñëîâàìè, ñóùåñòâóåò òàêàÿ ìàêñèìàëüíàÿ ôîðìà ôîðìóëû
min ( ( ) & ( ))F t F tA C , ÷òî ôîðìóëà � �(min ( ( ))) max (min (( ( )) & ( )))F t F t F tA A C
áóäåò ìàêñèìàëüíûì ðåøåíèåì. Âû÷èñëåíèå âñåõ ìàêñèìàëüíûõ ôîðì ôîðìóëû
âåñüìà ñëîæíî, ïîýòîìó áóäåì ñòðîèòü ðåøåíèå, êîòîðîå íå òðåáóåò âû÷èñëåíèÿ
ìàêñèìàëüíîé ôîðìû è íå ñèëüíî îòëè÷àåòñÿ îò ìàêñèìàëüíîãî ðåøåíèÿ.  êà-
÷åñòâå òàêîãî ðåøåíèÿ �F tB ( ) ìîæíî âçÿòü ôîðìóëó � �(min ( ( ))) ( )F t F tA C , êî-
òîðàÿ òàêæå óäîâëåòâîðÿåò ïåðâîìó óñëîâèþ ìàêñèìàëüíîñòè.
Òåïåðü äëÿ ïîëó÷åíèÿ ðåøåíèÿ F tB ( ) ñèãíàòóðû � B íåîáõîäèìî âçÿòü
�-ïðîåêöèþ ôîðìóëû �F tB ( ) íà åå ïåðåìåííûå, îïðåäåëÿåìûå ñèãíàòóðîé � B .
Ïóñòü F x x y ym n( , ..., , , ..., )1 1 — ïðîïîçèöèîíàëüíàÿ ôîðìóëà îò ïåðåìåííûõ
x x y ym n1 1, ..., , , ..., . Åå �-ïðîåêöèåé íà ìíîæåñòâî ïåðåìåííûõ { }x xm1, ..., íàçû-
âàåòñÿ ôîðìóëà
� � �y y F x x y yn m n1 1 1� ( , ..., , , ..., )
� F x x F x x Fm m( , ..., , , , ..., ) & ( , ..., , , , ..., ) & &1 10 0 0 0 0 1 � ( , ..., , , ,..., )x xm1 1 1 1 .
Åñëè � B kp p� { }1, ..., , òî äëÿ ôîðìóëû �F tB ( ) ãëóáèíû r ñòðîèòñÿ ïðîåêöèÿ
åå íà ìíîæåñòâî ïåðåìåííûõ {p t p t p t p t p t rk k1 1 11 1( ), ..., ( ), ( ), ..., ( ), ..., ( ), . ..
..., ( )p t rk }. Äëÿ âû÷èñëåíèÿ ïðîåêöèè ôîðìóëû íà ïîäìíîæåñòâî åå àðãóìåí-
òîâ åå óäîáíî ïðåäñòàâëÿòü â òàê íàçûâàåìîé íîðìàëüíîé ôîðìå [8]. Íîðìàëüíàÿ
ôîðìà èìååò âèä �
�
i
n
i iF t f t
1
1( ) & ( ) , ãäå f ti ( ) — ôîðìóëà, ïîñòðîåííàÿ èç àòî-
ìîâ íóëåâîãî ðàíãà, à F ti ( ) 1 — èç àòîìîâ, ðàíã êîòîðûõ íå ïðåâûøàåò –1. Êðî-
ìå òîãî, äëÿ âñåõ i j n, , ...,�1 ( )i j� F t F ti j( ) & ( ) �1 1 0 (óñëîâèå îðòîãîíàëü-
íîñòè). Ïðåîáðàçîâàíèå ôîðìóëû ê âèäó, óäîâëåòâîðÿþùåìó óñëîâèþ îðòîãî-
íàëüíîñòè, áóäåì íàçûâàòü îðòîãîíàëèçàöèåé. Íîðìàëüíàÿ ôîðìà âèäà
�
�
i
n
i iF t f t
1
1( ) & ( ) íàçûâàåòñÿ ïîëíîé, åñëè �
�
�
i
n
iF t
1
1 1( ) . Îòðèöàíèå ôîðìóëû
F t( ) , ïðåäñòàâëåííîé â ïîëíîé íîðìàëüíîé ôîðìå, èìååò âèä
�
�
�
i
n
i iF t f t
1
1( ) & ( ) , ÷òî òàêæå ÿâëÿåòñÿ íîðìàëüíîé ôîðìîé. Íîðìàëüíàÿ
ôîðìà ôîðìóëû � �(min ( ( ))) ( )F t F tA C ñòðîèòñÿ èç íîðìàëüíûõ ôîðì ôîðìóë
� (min ( ( )))F tA è F tC ( ) ñ ïîìîùüþ îïåðàöèè äèçúþíêòèâíîãî ïðîèçâåäåíèÿ [8].
10 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2012, ¹ 4
Óòâåðæäåíèå 3. ×òîáû ïîëó÷èòü ä.í.ô. ôîðìóëû � �y y F x xn m1 1� ( , ..., ,
y yn1, ..., ) , íåîáõîäèìî â ä.í.ô. ôîðìóëû F x x y ym n( , ..., , , ..., )1 1 ïîñëåäîâàòåëüíî
îñóùåñòâëÿòü ñêëåèâàíèÿ ïî ïåðåìåííûì y yn1, ..., è ïîñëå êàæäîãî òàêîãî ñêëå-
èâàíèÿ ïî yi óäàëÿòü âñå êîíúþíêöèè, ñîäåðæàùèå yi èëè � yi .
Îñíîâíàÿ èäåÿ èñïîëüçîâàíèÿ íîðìàëüíîé ôîðìû äëÿ ïîñòðîåíèÿ �-ïðîåê-
öèè ôîðìóëû ñîñòîèò â òîì, ÷òîáû çàäà÷ó áîëüøîé ðàçìåðíîñòè ñâåñòè ê ðÿäó
çàäà÷ ñóùåñòâåííî ìåíüøåé ðàçìåðíîñòè.
Ïóñòü { }x x y ym n1 1, ..., , , ..., — ñèãíàòóðà ôîðìóëû F t( ) , è íåîáõîäèìî ïîñòðî-
èòü ïðîåêöèþ ýòîé ôîðìóëû (ðàññìàòðèâàåìîé êàê ïðîïîçèöèîíàëüíàÿ ôîðìóëà) íà
ìíîæåñòâî ïåðåìåííûõ, ñîîòâåòñòâóþùèõ ñèìâîëàì x xm1, ..., . Îáîçíà÷èì ìíîæåñ-
òâî ýòèõ ïåðåìåííûõ � ( )t . ×òîáû óïðîñòèòü ðàññìîòðåíèå, áóäåì ñ÷èòàòü, ÷òî F t( )
èìååò ãëóáèíó 1. Òàêèì îáðàçîì, � ( ) ( ), ..., ( ), ( ), ..., ( )t x t x t x t x tm m� { }1 11 1 .
Ïîñòðîåíèå ïðîåêöèè íà � ( )t ñîñòîèò èç äâóõ ýòàïîâ: ñíà÷àëà ñòðîèòñÿ ïðîåêöèÿ
íà ìíîæåñòâî � � � ( ) ( ), ..., ( ), ( ), ..., ( ), (t x t x t y t y t xm n{ 1 1 11 1 1 1 t x tm), ..., ( )},
à çàòåì — ïðîåêöèÿ ðåçóëüòàòà íà � ( )t . Â íîðìàëüíîé ôîðìå ôîðìóëû F t( ) âèäà
�
�
i
n
i iF t f t
1
1( ) & ( ) òîëüêî ôîðìóëû f ti ( ) ( , ..., )i n�1 çàâèñÿò îò ïåðåìåííûõ ðàí-
ãà 0. Ïîñêîëüêó äëÿ ëþáûõ i j, ( )i j� F t F ti j( ) & ( ) �1 1 0, òî äëÿ ïîëó÷åíèÿ
ïðîåêöèè íà ìíîæåñòâî ïåðåìåííûõ �� ( )t ñêëåèâàíèÿ ïî ïåðåìåííûì
y t y tn1 ( ), ..., ( ) ìîæíî îñóùåñòâëÿòü íåçàâèñèìî â êàæäîé ôîðìóëå f ti ( )
( , ..., )i n�1 . Òàêèì îáðàçîì, ïîñòðîåíèå ïðîåêöèè ôîðìóëû F t( ) íà ìíîæåñòâî
ïåðåìåííûõ �� ( )t ñâîäèòñÿ ê ïîñòðîåíèþ ïðîåêöèé n ñóùåñòâåííî áîëåå ïðî-
ñòûõ ôîðìóë f t f tn1 ( ), ..., ( ) íà ýòî ìíîæåñòâî ïåðåìåííûõ.
Ïîñëå ïîëó÷åíèÿ ïðîåêöèè F t( ) íà �� ( )t íóæíî ïîñòðîèòü ïðîåêöèþ ýòîé
ôîðìóëû íà ìíîæåñòâî ïåðåìåííûõ � ( )t . Äëÿ ýòîãî åå ñëåäóåò ïðåîáðàçîâàòü â
òàêóþ ôîðìóëó âèäà �
�
i
n
i iF t f t
1
1( ) & ( ) , ÷òîáû äëÿ ëþáûõ i j, ( )i j� âûïîëíÿ-
ëîñü f t f ti j( ) & ( ) � 0 . Ïîñêîëüêó ôóíêöèè F ti ( ) 1 ( , ..., )i n�1 çàâèñÿò òîëüêî îò
ïåðåìåííûõ x t x t y t y tm n1 11 1 1 1( ), ..., ( ), ( ), ..., ( ) , ïîñòðîåíèå �-ïðîåêöèè
âñåé ôîðìóëû ñâîäèòñÿ ê ïîñòðîåíèþ �-ïðîåêöèé ôîðìóë F ti ( ) 1 â êîíúþí-
êöèÿõ F t f ti i( ) & ( ) 1 íà ìíîæåñòâî { }x t x tm1 1 1( ), ..., ( ) .
Ïðèìåð. Ïóñòü â ñòðóêòóðå, èçîáðàæåííîé íà ðèñ. 1, I i1 � { }, O o1 � { },
U u� { }, V � { }� è I O2 2� � � . Òàêèì îáðàçîì, �C i o� { }, , � A i u o� { }, , ,� ,
� B u� { }, � .
Äëÿ óïðîùåíèÿ çàïèñè ñïåöèôèêàöèé àâòîìàòîâ ïðèìåì ñëåäóþùèå ñîãëà-
øåíèÿ: àòîì íóëåâîãî ðàíãà âèäà p t( ) çàïèñûâàåòñÿ êàê p, äëÿ àòîìà ðàíãà –1
âèäà p t( ) 1 áóäåì èñïîëüçîâàòü çàïèñü [ ]p , çíàêè êîíúþíêöèè è êâàíòîðà âñåîá-
ùíîñòè â ôîðìóëàõ îïóñêàþòñÿ. Îáîçíà÷åíèå [ ]p ðàñïðîñòðàíèì íà ôîðìóëû,
ïîñòðîåííûå èç àòîìîâ ðàíãà –1, íàïðèìåð, ôîðìóëó p t p t1 21 1( ) ( ) & �
& ( )p t3 1 áóäåì çàïèñûâàòü êàê [ ]p p p1 2 3� .  òàêèõ îáîçíà÷åíèÿõ ñïåöèôèêà-
öèè àâòîìàòîâ A è C, ïðåäñòàâëåííûå â íîðìàëüíîé ôîðìå, èìåþò âèä
F t o u io i o o uo u o o u oA ( ) [ ] ( ) [ ]( ) [ ] (� � � � � � � � � � � � � � �� � � � � � �� o) ,
F t o io i o o oC ( ) [ ]( ) [ ]� � � � � � .
Àâòîìàò C, ñïåöèôèöèðóåìûé ôîðìóëîé
�tF tC ( ) , èçîáðàæåí íà ðèñ. 2.
Ñïåöèôèêàöèþ àâòîìàòà B ñèãíàòóðû
� � �� �A B áóäåì ñòðîèòü â âèäå
� � � �F t F t F tB A C( ) (min ( ( ))) ( ) .
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2012, ¹ 4 11
�i�o
1 2
o
io
Ðèñ. 2
Ìèíèìàëüíàÿ ôîðìà ôîðìóëû F tA ( ) èìååò âèä
min ( ( )) [ ( )] ( )F t o i u u io i oA � � � � � � �
� � � � � � � � � � � � � � � �[ ( )]( ) [ ] ( )� � � � � �o i u uo u o u o u o o .
Äëÿ ïîëó÷åíèÿ ïîëíîé íîðìàëüíîé ôîðìû ñëåäóåò äîáàâèòü êîíúþíêöèþ
[ ]( )� �� � � � � � �u o iuo i u o 0 . Òåïåðü îòðèöàíèå ôîðìóëû min( ( ))F tA ïîëó-
÷àåòñÿ ïóòåì èíâåðòèðîâàíèÿ âñåõ ïîäôîðìóë âèäà f ti ( ) :
� � � � � � � � � �(min ( ( ))) [ ( )]( )F t o i u u i o ioA
� � � � � � � � � � � �[ ( )]( )� � �o i u u uo o
� � � � � � � � � � � � � �[ ]( ) [ ]( )� � � � �u o o o u u o iuo i u o 1 .
Äèçúþíêòèâíîå ïðîèçâåäåíèå ôîðìóë � (min( ( )))F tA è F tC ( ) äàåò:
� � � � � � � � � � � � � � � �F t o i u o i u u o u oB ( ) [ ( )]( ) [ ( )]( ) [ ](1 � � � u o� � ��)
� � � � � � � � � � � � � �[ ]( ) [ ]( )� � � �u o iuo i u o o u i u1 1
� � � � � � � � � � � � � � � �[ ]( ) [ ]( )i o u o u o u o u o� � � � � .
Ïîñòðîèì òåïåðü �-ïðîåêöèþ ôîðìóëû �F tB ( ) íà { }[ ], [ ], ,� �u u .
Íà ïåðâîì ýòàïå ïîëó÷èì
[ ]( ) [ ]( ) [ ]( )o u i u i o u o u u o u� � � � � � � � � � � � � � � � � �� � � � � � �1 .
Îðòîãîíàëèçàöèÿ ôîðìóë f ti ( ) äàåò
[ ]( ) [ ]( ) [ ]( )o u u u u o iu u� � � � � � � � � � � � �� � � � � �1 .
Íà âòîðîì ýòàïå ïîëó÷èì
F t u u u u uB ( ) [ ]( ) [ ]( ) [ ]( )� � � � � � � � � � �� � � � � �1 .
Ïîêàæåì, ÷òî ïîëó÷åííàÿ ôîðìóëà ñïåöèôèöèðóåò àâòîìàò, ÿâëÿþùèéñÿ ðåøå-
íèåì óðàâíåíèÿ A X C� � . Äëÿ ýòîãî ïîñòðîèì ñïåöèôèêàöèþ êîìïîçèöèè àâòîìà-
òîâ A è B, ò.å. F t F tA B( ) & ( ) . Ïåðåìíîæèâ ñîîòâåòñòâóþùèå ôîðìóëû, ïîëó÷èì
[ ]( ) [ ]( )� � � � � � � � � � �� � � �o uo u o u o
� � � � � � � � � � � �[ ] ( ) [ ]( ) [ ] ( )o u io i o o uo o u io i o� � � � � .
Ýòà ôîðìóëà ñïåöèôèöèðóåò àâòîìàò,
èçîáðàæåííûé íà ðèñ. 3.
Íåòðóäíî âèäåòü, ÷òî îãðàíè÷åíèå
ýòîãî àâòîìàòà íà ìíîæåñòâî ïåðåìåí-
íûõ { }i o, ýêâèâàëåíòíî àâòîìàòó C.
ÇÀÊËÞ×ÅÍÈÅ
Ðàññìîòðåíà çàäà÷à ðåøåíèÿ íåðà-
âåíñòâ íàä �-àâòîìàòàìè, âîçíèêàþùàÿ
ïðè êîìïîçèöèîííîì ïîäõîäå ê ïðîåê-
òèðîâàíèþ ðåàêòèâíûõ ñèñòåì. Òàêèå
íåðàâåíñòâà õàðàêòåðèçóþòñÿ îïåðàöèåé êîìïîçèöèè àâòîìàòîâ è áèíàðíûì
îòíîøåíèåì «� », îïðåäåëåííûì íà ìíîæåñòâå àâòîìàòîâ. Çàäà÷à ôîðìóëèðó-
åòñÿ è ðåøàåòñÿ íà óðîâíå ñïåöèôèêàöèé àâòîìàòîâ â ëîãè÷åñêîì ÿçûêå L,
ïîýòîìó ñîîòâåòñòâóþùèå ïîíÿòèÿ îïðåäåëÿþòñÿ äëÿ ñïåöèôèêàöèé. Ïðè ðå-
øåíèè íåðàâåíñòâ òàêîãî ðîäà îáû÷íî èíòåðåñ ïðåäñòàâëÿþò íàèáîëüøèå
12 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2012, ¹ 4
��u �i �o
1 2
��u �i �o
�u �uo
��uio
�uio
3
��uio
�u �i �o
u �uo
4
Ðèñ. 3
â ñìûñëå óêàçàííîãî îòíîøåíèÿ ðåøåíèÿ, îäíàêî â íàøåì ñëó÷àå îòíîøåíèå �
ÿâëÿåòñÿ ÷àñòè÷íûì ïîðÿäêîì, äëÿ êîòîðîãî íàèáîëüøåãî ðåøåíèÿ ìîæåò íå
ñóùåñòâîâàòü.  ñâÿçè ñ ýòèì ðàññìàòðèâàåòñÿ çàäà÷à îòûñêàíèÿ ìàêñèìàëüíîãî
ðåøåíèÿ. Âûáîð äëÿ ñïåöèôèêàöèè äîñòàòî÷íî ïðîñòîãî ÿçûêà ïîçâîëèë ñâåñòè
ðåøåíèå ýòîé çàäà÷è ê ïðåîáðàçîâàíèþ ïðîïîçèöèîíàëüíûõ ôîðìóë.
 ïðèëîæåíèÿõ, îðèåíòèðîâàííûõ íà ñõåìíóþ ðåàëèçàöèþ ïðîåêòèðóåìîé
ñèñòåìû, èñïîëüçóþòñÿ äðóãèå âèäû êîìïîçèöèè, îáåñïå÷èâàþùèå íåâîçìîæ-
íîñòü îáðàçîâàíèÿ ïîðî÷íîãî öèêëà ïðè èçìåíåíèè âõîäíûõ è âûõîäíûõ ñèãíà-
ëîâ âçàèìîäåéñòâóþùèõ ìîäóëåé. Êàê ïîêàçàíî â [9], ìíîãèå èç òàêèõ âèäîâ
êîìïîçèöèè ìîãóò áûòü ñâåäåíû ê ðàññìîòðåííîé â íàñòîÿùåé ñòàòüå ñèíõðîí-
íîé êîìïîçèöèè öèêëè÷åñêèõ �-àâòîìàòîâ ïóòåì ïðîñòîãî ïðåîáðàçîâàíèÿ îä-
íîé èëè îáåèõ ñïåöèôèêàöèé, ó÷àñòâóþùèõ â êîìïîçèöèè.
Îñíîâíàÿ èäåÿ ïðåäëîæåííîãî ïîäõîäà ñîñòîèò â òîì, ÷òîáû ñíà÷àëà ïî-
ñòðîèòü ðåøåíèå äëÿ ñèíõðîííîé êîìïîçèöèè, ò.å. â âèäå ôîðìóëû, ñèãíàòóðà
êîòîðîé ñîñòîèò èç âñåõ ïðåäèêàòíûõ ñèìâîëîâ, âñòðå÷àþùèõñÿ â ñïåöèôèêàöè-
ÿõ, à çàòåì ïîëó÷èòü ðåøåíèå äëÿ âíåøíåé êîìïîçèöèè, âçÿâ �-ïðîåêöèþ ïîëó-
÷åííîé ôîðìóëû íà ñîîòâåòñòâóþùåå ìíîæåñòâî ïåðåìåííûõ. Ïðåäëîæåí ïîä-
õîä ê ïîñòðîåíèþ òàêîé ïðîåêöèè ïóòåì ñâåäåíèÿ çàäà÷è áîëüøîé ðàçìåðíîñòè
ê ðÿäó çàäà÷ ñóùåñòâåííî ìåíüøåé ðàçìåðíîñòè.
Âîîáùå ãîâîðÿ, ëþáàÿ ôîðìóëà, óäîâëåòâîðÿþùàÿ óðàâíåíèþ
min ( ( ) & ( )) min( ( ) & ( ))F t F t F t F tA X A C� , ÿâëÿåòñÿ ìàêñèìàëüíûì ðåøåíèåì â
ïðîñòðàíñòâå ñîñòîÿíèé ñèãíàòóðû � � �� �A B . Ïîñêîëüêó òðåáóåìîå ðåøå-
íèå ïîëó÷àåòñÿ ïóòåì âçÿòèÿ �-ïðîåêöèè ðåøåíèÿ ñ ñèãíàòóðîé � � �� �A B ,
ïîñòðîåíèå ñïåöèôèêàöèè â âèäå ìàêñèìàëüíîé ôîðìû òàêîãî ðåøåíèÿ óâåëè÷è-
âàåò âîçìîæíîñòè îïòèìèçàöèè ðåøåíèÿ ñ ñèãíàòóðîé � B .
Ñëåäóåò çàìåòèòü, ÷òî çàäà÷à ðåøàåòñÿ äëÿ íåèíèöèàëüíûõ ñïåöèôèêàöèé,
õîòÿ íà ïðàêòèêå, êàê ïðàâèëî, ðàññìàòðèâàþòñÿ èíèöèàëüíûå ñèñòåìû. Îáû÷íî
èíèöèàëèçàöèÿ ñïåöèôèêàöèé â ÿçûêå L îñóùåñòâëÿåòñÿ ïóòåì çàäàíèÿ íà÷àëü-
íîãî óñëîâèÿ â âèäå ôîðìóëû F t( ) ýòîãî æå ÿçûêà, èñïîëüçóåìîé äëÿ âûäåëåíèÿ
íà÷àëüíîãî ñîñòîÿíèÿ ïîñëå ïåðåõîäà ê ïðîöåäóðíîìó ïðåäñòàâëåíèþ àâòîìàòà.
Íîðìàëüíàÿ ôîðìà ïðåäñòàâëåíèÿ ñïåöèôèêàöèé äàåò âîçìîæíîñòü ñðàçó ó÷èòû-
âàòü èõ èíèöèàëüíîñòü, ÷òî â ðÿäå ñëó÷àåâ ñîêðàùàåò îáúåì âû÷èñëåíèé, íåîá-
õîäèìûõ äëÿ ðåøåíèÿ çàäà÷è.
ÑÏÈÑÎÊ ËÈÒÅÐÀÒÓÐÛ
1. S o l u t i o n of synchronous language equations for logic synthesis / N. Yevtushenko, T. Villa, R. Brayton,
A. Petrenko, A. Sangiovanni-Vincentelli // Âåñòí. Òîìñê. ãîñ. óí-òà. — 2002. — ¹ 1. — Ñ. 132–138.
2. B u f f a l o v S . , E l - F a k i h K h a l e d , Y e v t u s h e n k o N . , B o c h m a n n G . Progressive solutions
to a parallel automata equation // Lect. Notes Comput. Sci. — 2003. — 2767. — P. 367–382.
3. Y e v t u s h e n k o N . , Z h a r i k o v a S . , V e t r o v a M . Multi component digital circuit optimization by
solving FSM equations // Proc. Euromicro Symp. on Digital System Design. — IEEE Comput. Soc., 2003.
— P. 62–68.
4. H a r e l D . , P n u e l i A . On the development of reactive systems / K.R. Apt, ed. // NATO ASI Series.
Logic and Models of Concurrent Systems. — Berlin: Springer, 1985. — F13. — P. 477–498.
5. × å á î ò à ð å â À . Í . Îá îäíîì ïîäõîäå ê ôóíêöèîíàëüíîé ñïåöèôèêàöèè àâòîìàòíûõ ñèñòåì. I //
Êèáåðíåòèêà è ñèñòåìíûé àíàëèç. — 1993. — ¹ 3. — Ñ. 31–42.
6. Á ð à ó ý ð  . Ââåäåíèå â òåîðèþ êîíå÷íûõ àâòîìàòîâ. — Ì.: Ðàäèî è ñâÿçü, 1987. — 392 ñ.
7. × å á î ò à ð å â À . Í . , Ê ó ð è â ÷ à ê Î . È . Àïïðîêñèìàöèÿ ìíîæåñòâ ñâåðõñëîâ ôîðìóëàìè ÿçûêà L
// Êèáåðíåòèêà è ñèñòåìíûé àíàëèç. — 2007. — ¹ 6. — Ñ. 18–26.
8. Ê à ï è ò î í î â à Þ . Â . , × å á î ò à ð å â À . Í . Èíäóêòèâíûé ñèíòåç àâòîìàòà ïî ñïåöèôèêàöèè
â ëîãè÷åñêîì ÿçûêå L // Òàì æå. — 2000. — ¹6. — Ñ. 3–13.
9. × å á î ò à ð å â À . Í . Âçàèìîäåéñòâèå àâòîìàòîâ // Òàì æå. — 1991. — ¹ 6. — Ñ. 17–29.
Ïîñòóïèëà 12.01.2011
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2012, ¹ 4 13
|
| id | nasplib_isofts_kiev_ua-123456789-84120 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 0023-1274 |
| language | Russian |
| last_indexed | 2025-12-07T17:32:29Z |
| publishDate | 2012 |
| publisher | Інститут кібернетики ім. В.М. Глушкова НАН України |
| record_format | dspace |
| spelling | Чеботарев, А.Н. 2015-07-03T09:01:00Z 2015-07-03T09:01:00Z 2012 Проектирование реактивных алгоритмов путем решения уравнений над автоматами / А.Н. Чеботарев // Кибернетика и системный анализ. — 2012. — Т. 48, № 4. — С. 3-13. — Бібліогр.: 9 назв. — рос. 0023-1274 https://nasplib.isofts.kiev.ua/handle/123456789/84120 519.731.1 Розглядається задача розв’язання нерівностей над автоматами, яка виникає при композиційному підході до проектування реактивних систем. Задача формулюється та розв’язується на рівні специфікацій автоматів логічною мовою L. Показано, як одержати максимальний розв’язок нерівності відносно операції синхронної композиції автоматів. Іл.: 3. Бібліогр.: 9 назв. The problem of solving inequalities over finite state machines (FSMs) is considered. This problem arises in the compositional approach to the design of reactive systems. The problem is formulated and solved at the level of FSM specifications in the logical language L. We show how to compute the maximal solution to the inequality with respect to the operation of synchronous composition of FSMs. ru Інститут кібернетики ім. В.М. Глушкова НАН України Кибернетика и системный анализ Кибернетика Проектирование реактивных алгоритмов путем решения уравнений над автоматами Проектування реактивних алгоритмів шляхом розв’язання рівнянь над автоматами Design of reactive algorithms by solving equations over finite state machines Article published earlier |
| spellingShingle | Проектирование реактивных алгоритмов путем решения уравнений над автоматами Чеботарев, А.Н. Кибернетика |
| title | Проектирование реактивных алгоритмов путем решения уравнений над автоматами |
| title_alt | Проектування реактивних алгоритмів шляхом розв’язання рівнянь над автоматами Design of reactive algorithms by solving equations over finite state machines |
| title_full | Проектирование реактивных алгоритмов путем решения уравнений над автоматами |
| title_fullStr | Проектирование реактивных алгоритмов путем решения уравнений над автоматами |
| title_full_unstemmed | Проектирование реактивных алгоритмов путем решения уравнений над автоматами |
| title_short | Проектирование реактивных алгоритмов путем решения уравнений над автоматами |
| title_sort | проектирование реактивных алгоритмов путем решения уравнений над автоматами |
| topic | Кибернетика |
| topic_facet | Кибернетика |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/84120 |
| work_keys_str_mv | AT čebotarevan proektirovaniereaktivnyhalgoritmovputemrešeniâuravneniinadavtomatami AT čebotarevan proektuvannâreaktivnihalgoritmívšlâhomrozvâzannârívnânʹnadavtomatami AT čebotarevan designofreactivealgorithmsbysolvingequationsoverfinitestatemachines |