Определение фиктивных состояний в Σ-автомате, синтезированном по спецификации в языке LP
Синтез детерминированного Σ-автомата, специфицированного в языке LP, состоит в последовательном выполнении двух процедур. Первая строит автомат, имеющий подавтомат, совпадающий со специфицированным автоматом, а вторая удаляет состояния, не принадлежащие этому подавтомату. Такие состояния называются...
Gespeichert in:
| Datum: | 2019 |
|---|---|
| 1. Verfasser: | |
| Format: | Artikel |
| Sprache: | Russian |
| Veröffentlicht: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2019
|
| Schriftenreihe: | Кибернетика и системный анализ |
| Schlagworte: | |
| Online Zugang: | https://nasplib.isofts.kiev.ua/handle/123456789/181029 |
| 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: | Определение фиктивных состояний в Σ-автомате, синтезированном по спецификации в языке LP / А.Н. Чеботарев // Кибернетика и системный анализ. — 2019. — Т. 55, № 5. — С. 47-57. — Бібліогр.: 7 назв. — рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
nasplib_isofts_kiev_ua-123456789-181029 |
|---|---|
| record_format |
dspace |
| spelling |
nasplib_isofts_kiev_ua-123456789-1810292025-02-09T09:39:08Z Определение фиктивных состояний в Σ-автомате, синтезированном по спецификации в языке LP Визначення фіктивних станів в Σ-автоматі, що синтезований за специфікацією у мові LP Detecting fictitious states in Σ -automaton synthesized from the specification in the language LP Чеботарев, А.Н. Кібернетика Синтез детерминированного Σ-автомата, специфицированного в языке LP, состоит в последовательном выполнении двух процедур. Первая строит автомат, имеющий подавтомат, совпадающий со специфицированным автоматом, а вторая удаляет состояния, не принадлежащие этому подавтомату. Такие состояния называются фиктивными. Рассмотрен способ определения фиктивных состояний. Полученные результаты позволяют соответствующий процесс свести к нахождению так называемых основных циклов в автомате и, в конечном счете, к проверке принадлежности периодического обратного сверхслова некоторому ω-регулярному множеству. Синтез детермінованого Σ-автомата, специфікованого мовою LP, полягає у послідовному виконанні двох процедур. Перша будує автомат, який містить у собі підавтомат, що збігається зі специфікованим автоматом, а друга видаляє стани, які не належать цьому підавтомату. Такі стани називаються фіктивними. Розглянуто спосіб визначення фіктивних станів. Отримані результати дозволяють відповідний процес звести до знаходження так званих основних циклів в автоматі і, врешті-решт, до перевірки належності періодичного зворотного надслова деякій ω-регулярній множині. Synthesis of a deterministic Σ-automaton specified in the language LP consists in the execution of two consecutive procedures. The first one constructs the automaton that has a subautomaton, which is identical to the specified automaton, and the other deletes the states that do not belong to this subautomaton. Such states are called fictitious. The method for detecting fictitious states is considered. The obtained results allow reducing detection of fictitious states to finding so-called basic cycles and eventually to checking the membership of a periodic -word in some ω-regular set. 2019 Article Определение фиктивных состояний в Σ-автомате, синтезированном по спецификации в языке LP / А.Н. Чеботарев // Кибернетика и системный анализ. — 2019. — Т. 55, № 5. — С. 47-57. — Бібліогр.: 7 назв. — рос. 1019-5262 https://nasplib.isofts.kiev.ua/handle/123456789/181029 519.713.1 ru Кибернетика и системный анализ application/pdf Інститут кібернетики ім. В.М. Глушкова НАН України |
| institution |
Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| collection |
DSpace DC |
| language |
Russian |
| topic |
Кібернетика Кібернетика |
| spellingShingle |
Кібернетика Кібернетика Чеботарев, А.Н. Определение фиктивных состояний в Σ-автомате, синтезированном по спецификации в языке LP Кибернетика и системный анализ |
| description |
Синтез детерминированного Σ-автомата, специфицированного в языке LP, состоит в последовательном выполнении двух процедур. Первая строит автомат, имеющий подавтомат, совпадающий со специфицированным автоматом, а вторая удаляет состояния, не принадлежащие этому подавтомату. Такие состояния называются фиктивными. Рассмотрен способ определения фиктивных состояний. Полученные результаты позволяют соответствующий процесс свести к нахождению так называемых основных циклов в автомате и, в конечном счете, к проверке принадлежности периодического обратного сверхслова некоторому ω-регулярному множеству. |
| format |
Article |
| author |
Чеботарев, А.Н. |
| author_facet |
Чеботарев, А.Н. |
| author_sort |
Чеботарев, А.Н. |
| title |
Определение фиктивных состояний в Σ-автомате, синтезированном по спецификации в языке LP |
| title_short |
Определение фиктивных состояний в Σ-автомате, синтезированном по спецификации в языке LP |
| title_full |
Определение фиктивных состояний в Σ-автомате, синтезированном по спецификации в языке LP |
| title_fullStr |
Определение фиктивных состояний в Σ-автомате, синтезированном по спецификации в языке LP |
| title_full_unstemmed |
Определение фиктивных состояний в Σ-автомате, синтезированном по спецификации в языке LP |
| title_sort |
определение фиктивных состояний в σ-автомате, синтезированном по спецификации в языке lp |
| publisher |
Інститут кібернетики ім. В.М. Глушкова НАН України |
| publishDate |
2019 |
| topic_facet |
Кібернетика |
| url |
https://nasplib.isofts.kiev.ua/handle/123456789/181029 |
| citation_txt |
Определение фиктивных состояний в Σ-автомате, синтезированном по спецификации в языке LP / А.Н. Чеботарев // Кибернетика и системный анализ. — 2019. — Т. 55, № 5. — С. 47-57. — Бібліогр.: 7 назв. — рос. |
| series |
Кибернетика и системный анализ |
| work_keys_str_mv |
AT čebotarevan opredeleniefiktivnyhsostoânijvsavtomatesintezirovannompospecifikaciivâzykelp AT čebotarevan viznačennâfíktivnihstanívvsavtomatíŝosintezovanijzaspecifíkacíêûumovílp AT čebotarevan detectingfictitiousstatesinsautomatonsynthesizedfromthespecificationinthelanguagelp |
| first_indexed |
2025-11-25T10:50:37Z |
| last_indexed |
2025-11-25T10:50:37Z |
| _version_ |
1849759198877843456 |
| fulltext |
ÓÄÊ 519.713.1
À.Í. ×ÅÁÎÒÀÐÅÂ
ÎÏÐÅÄÅËÅÍÈÅ ÔÈÊÒÈÂÍÛÕ ÑÎÑÒÎßÍÈÉ Â �-ÀÂÒÎÌÀÒÅ,
ÑÈÍÒÅÇÈÐÎÂÀÍÍÎÌ ÏÎ ÑÏÅÖÈÔÈÊÀÖÈÈ Â ßÇÛÊÅ LP
Àííîòàöèÿ. Ñèíòåç äåòåðìèíèðîâàííîãî �-àâòîìàòà, ñïåöèôèöèðîâàííîãî
â ÿçûêå LP, ñîñòîèò â ïîñëåäîâàòåëüíîì âûïîëíåíèè äâóõ ïðîöåäóð. Ïåð-
âàÿ ñòðîèò àâòîìàò, èìåþùèé ïîäàâòîìàò, ñîâïàäàþùèé ñî ñïåöèôèöèðî-
âàííûì àâòîìàòîì, à âòîðàÿ óäàëÿåò ñîñòîÿíèÿ, íå ïðèíàäëåæàùèå ýòîìó
ïîäàâòîìàòó. Òàêèå ñîñòîÿíèÿ íàçûâàþòñÿ ôèêòèâíûìè. Ðàññìîòðåí ñïîñîá
îïðåäåëåíèÿ ôèêòèâíûõ ñîñòîÿíèé. Ïîëó÷åííûå ðåçóëüòàòû ïîçâîëÿþò ñî-
îòâåòñòâóþùèé ïðîöåññ ñâåñòè ê íàõîæäåíèþ òàê íàçûâàåìûõ îñíîâíûõ
öèêëîâ â àâòîìàòå è, â êîíå÷íîì ñ÷åòå, ê ïðîâåðêå ïðèíàäëåæíîñòè ïåðèî-
äè÷åñêîãî îáðàòíîãî ñâåðõñëîâà íåêîòîðîìó ��-ðåãóëÿðíîìó ìíîæåñòâó.
Êëþ÷åâûå ñëîâà: �-àâòîìàò, ôèêòèâíîå ñîñòîÿíèå, íà÷àëüíûé ñèëüíî ñâÿçíûé
ïîäàâòîìàò, íîðìàëüíàÿ ôîðìà, ��-ðåãóëÿðíîå ìíîæåñòâî, îñíîâíîé öèêë.
ÂÂÅÄÅÍÈÅ
 ðàáîòå [1] ïðåäëîæåíû ìåòîäû ñèíòåçà �-àâòîìàòîâ, ñïåöèôèöèðîâàííûõ
â ëîãè÷åñêèõ ÿçûêàõ LP èëè LF ïåðâîãî ïîðÿäêà. Ñèíòåç àâòîìàòà ñîñòîèò
â ïîñëåäîâàòåëüíîì âûïîëíåíèè äâóõ ïðîöåäóð. Ïåðâàÿ èç íèõ ïî ñïåöèôèêà-
öèè G tF t� � ( ) ñòðîèò òàêîé �-àâòîìàò �A G( ), ÷òî ñïåöèôèöèðóåìûé àâòîìàò
ÿâëÿåòñÿ åãî ïîäàâòîìàòîì. Äëÿ ýòîãî ñïåöèôèêàöèÿ ýêâèâàëåíòíî ïðåîáðàçî-
âûâàåòñÿ ê âèäó, ãäå ôîðìóëà F t( ) ïðåäñòàâëåíà â òàê íàçûâàåìîé íîðìàëü-
íîé ôîðìå, êîòîðîé ñîîòâåòñòâóåò ãðàô �-àâòîìàòà �A G( ). Íîðìàëüíàÿ ôîðìà
ôîðìóëû F t( ) èìååò âèä � �
�i
n
i iF t f t
1
1( ) ( ), è àâòîìàò �A G( ) èìååò n ñîñòîÿíèé,
ñîîòâåòñòâóþùèõ ôîðìóëàì F t F tn1 ( ), , ( )� . Òàêîå ïðåäñòàâëåíèå ôîðìóëû F t( )
ìîæåò ñîäåðæàòü êîìïîíåíòû âèäà F t f ti i( ) ( )�1 , òîæäåñòâåííî ëîæíûå íà
âñåõ ìîäåëÿõ äëÿ ôîðìóëû G. Óäàëåíèå èõ èç ñïåöèôèêàöèè íå èçìåíÿåò
ìíîæåñòâî åå ìîäåëåé, à ñëåäîâàòåëüíî, è ñïåöèôèöèðóåìûé àâòîìàò. Ñîñòîÿ-
íèÿ, ñîîòâåòñòâóþùèå òàêèì êîìïîíåíòàì, íàçûâàþòñÿ ôèêòèâíûìè è äîëæíû
áûòü óäàëåíû èç àâòîìàòà �A G( ). Âòîðàÿ ïðîöåäóðà âûäåëÿåò â àâòîìàòå �A G( )
ñïåöèôèöèðóåìûé ïîäàâòîìàò A G( ), óäàëÿÿ ôèêòèâíûå ñîñòîÿíèÿ. Ðàçáèåíèå
àëãîðèòìà ñèíòåçà íà äâå ïîñëåäîâàòåëüíûå ïðîöåäóðû ïîçâîëèëî â ïåðâîé èç
íèõ óñòðàíèòü ñëîæíîñòè, ñâÿçàííûå ñ ïðîâåðêîé íåïðîòèâîðå÷èâîñòè ôîðìóë
ïåðâîãî ïîðÿäêà. ×àñòè÷íî îíè ïåðåíåñåíû íà âòîðóþ ïðîöåäóðó, îäíàêî
â ýòîì ñëó÷àå âìåñòî ïðîâåðêè íåïðîòèâîðå÷èâîñòè ôîðìóë îñóùåñòâëÿåòñÿ
ïðîâåðêà èõ âûïîëíèìîñòè íà èíòåðïðåòàöèÿõ, îïðåäåëÿåìûõ �-àâòîìàòîì �A G( ).
Îïèñàíèå è îáîñíîâàíèå ïðîöåäóðû ïîñòðîåíèÿ íîðìàëüíîé ôîðìû ôîðìóëû F t( )
ïðèâåäåíî â [1]. Íàñòîÿùàÿ ðàáîòà ïîñâÿùåíà ïðîáëåìå íàõîæäåíèÿ ôèê-
òèâíûõ ñîñòîÿíèé â àâòîìàòå �A G( ).
Àíàëîãè÷íûé ïîäõîä ê ñèíòåçó �-àâòîìàòà, ñïåöèôèöèðîâàííîãî â ìåíåå
âûðàçèòåëüíîì ÿçûêå L* , èñïîëüçîâàëñÿ â [2]. Âî âòîðîé ÷àñòè ïðåäëîæåííîãî
òàì àëãîðèòìà ðåøàëàñü çàäà÷à ïðîâåðêè âûïîëíèìîñòè ôîðìóëû â ñîñòîÿíèè
àâòîìàòà. Îäíàêî, â îòëè÷èå îò äàííîé ðàáîòû, ýòà çàäà÷à ðåøàëàñü àâòîìàòíû-
ìè ìåòîäàìè è ñâîäèëàñü ê ïðîâåðêå íåïóñòîòû ïðÿìîãî ïðîèçâåäåíèÿ äâóõ èíè-
öèàëüíûõ àâòîìàòîâ. Ïðè ýòîì ïîñòðîåíèå èíèöèàëüíîãî àâòîìàòà, ñîîòâåòñòâó-
þùåãî ôîðìóëå F ti ( ), îñóùåñòâëÿëîñü äîâîëüíî ñëîæíîé ïðîöåäóðîé, èñïîëüçó-
þùåé ïðåäñòàâëåíèå ôîðìóëû â âèäå ðàçìå÷åííîé êîíôèãóðàöèè.
ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2019, òîì 55, ¹ 5 47
� À.Í. ×åáîòàðåâ, 2019
 íàñòîÿùåé ðàáîòå ôîðìóëàì F t F tn1 ( ), , ( )� ñòàâÿòñÿ â ñîîòâåòñòâèå
� �-ðåãóëÿðíûå âûðàæåíèÿ è çàäà÷à ñâîäèòñÿ ê ïðîâåðêå ïðèíàäëåæíîñòè íåêî-
òîðîãî ïåðèîäè÷åñêîãî îáðàòíîãî ñâåðõñëîâà ìíîæåñòâó îáðàòíûõ ñâåðõñëîâ, çà-
äàâàåìîìó � �-ðåãóëÿðíûì âûðàæåíèåì. Òàêàÿ ïðîâåðêà çíà÷èòåëüíî ïðîùå
ïðîöåäóðû, èñïîëüçóåìîé â [2]. Åäèíñòâåííàÿ ñëîæíîñòü ìîæåò âîçíèêíóòü ïðè
ïåðåõîäå îò ôîðìóëû F ti ( ) ê ñîîòâåòñòâóþùåìó åé � �-ðåãóëÿðíîìó âûðàæå-
íèþ. Âî ìíîãèõ ñëó÷àÿõ ýòîò ïåðåõîä îñóùåñòâëÿåòñÿ äîñòàòî÷íî ïðîñòî, ÷òî
ïðèâîäèò ê ïðîñòîìó ðåøåíèþ çàäà÷è.
ÎÑÍÎÂÍÛÅ ÏÎÍßÒÈß
Áåñêîíå÷íûå ñëîâà. Ïóñòü � — êîíå÷íûé àëôàâèò, Z — ìíîæåñòâî öåëûõ
÷èñåë. Êîíå÷íàÿ ïîñëåäîâàòåëüíîñòü � � �1 2� n , ãäå äëÿ âñåõ i (1 i n) � i
�,
íàçûâàåòñÿ ñëîâîì äëèíû n â àëôàâèòå �. Áåñêîíå÷íóþ âïðàâî ïîñëåäîâàòåëü-
íîñòü l � � �1 2 � íàçîâåì ñâåðõñëîâîì, èëè �-ñëîâîì, áåñêîíå÷íóþ âëåâî ïî-
ñëåäîâàòåëüíîñòü g � � �� � � �2 1 0 — îáðàòíûì ñâåðõñëîâîì, à áåñêîíå÷íóþ
â îáå ñòîðîíû ïîñëåäîâàòåëüíîñòü u � �� �� � � �1 0 1 2 — äâóñòîðîííèì ñâåðõ-
ñëîâîì, èëè Z-ñëîâîì. Ìíîæåñòâî âñåõ ñëîâ â àëôàâèòå �, âêëþ÷àÿ ïóñòîå
ñëîâî, îáîçíà÷àåòñÿ �* , ìíîæåñòâî âñåõ ñâåðõñëîâ — �
� , ìíîæåñòâî âñåõ
îáðàòíûõ ñâåðõñëîâ — �
�� , à ìíîæåñòâî âñåõ äâóñòîðîííèõ ñâåðõñëîâ — �
Z .
Íà ìíîæåñòâå � � �
*
� �
�� � îáû÷íûì îáðàçîì îïðåäåëåíà (÷àñòè÷íàÿ) îïåðà-
öèÿ êîíêàòåíàöèè « �», êîòîðóþ ðàñïðîñòðàíèì òàêæå íà ïîäìíîæåñòâà ìíîæåñòâ
�* , �
� è �
�� . Íàïðèìåð, åñëè R
�
�
� , Q
�* , òî R Q r q r R� � �
{ | , q Q
}.
Äëÿ Z-ñëîâà u áåñêîíå÷íûå åãî îòðåçêè � � �k k�1 è � �k k� �1 2�, ãäå k
Z, íà-
çîâåì ñîîòâåòñòâåííî k-ïðåôèêñîì è k-ñóôôèêñîì Z-ñëîâà u. Åñëè çíà÷åíèå
ïîçèöèè k â Z-ñëîâå íåñóùåñòâåííî, òî áóäåì ãîâîðèòü ïðîñòî î ïðåôèêñå è
ñóôôèêñå Z-ñëîâà u. Àíàëîãè÷íî îáðàòíîå ñâåðõñëîâî g1 íàçûâàåòñÿ ïðåôèê-
ñîì îáðàòíîãî ñâåðõñëîâà g, à ñëîâî l — åãî ñóôôèêñîì, åñëè g l g1 � � . Ñâåðõ-
ñëîâî (îáðàòíîå ñâåðõñëîâî), ïðåäñòàâëÿþùåå ñîáîé áåñêîíå÷íîå ïîâòîðåíèå
(êîíêàòåíàöèþ) îäíîãî è òîãî æå íåïóñòîãî ñëîâà r, ò.å. r r r r r r� � � �� �( ),
îáîçíà÷èì r r� �( )� . Òàêèå ñâåðõñëîâà íàçûâàþòñÿ ïåðèîäè÷åñêèìè ñ ïåðèî-
äîì r. Ñâåðõñëîâà âèäà r r1 �
� è îáðàòíûå ñâåðõñëîâà âèäà r r�
�
�
1, ãäå
r
�* \ { }� , à r1
�* , íàçîâåì êâàçèïåðèîäè÷åñêèìè. Êàæäîìó îáðàòíîìó
ñâåðõñëîâó (ñâåðõñëîâó) ñîîòâåòñòâóåò ñèììåòðè÷íîå åìó ñâåðõñëîâî (îáðàò-
íîå ñâåðõñëîâî), íàçûâàåìîå åãî èíâåðñèåé. Èíâåðñèåé îáðàòíîãî ñâåðõñëîâà
g � � �� � � �2 1 0 ÿâëÿåòñÿ ñâåðõñëîâî g �
� � � �0 1 2 � , ãäå � �i i� � . Äëÿ
W
�
� (��� ) îáîçíà÷èì W w w W� �
�
{ }| .
Àâòîìàòû.  êà÷åñòâå ñèíòåçèðóåìûõ àâòîìàòîâ íàä áåñêîíå÷íûìè ñëî-
âàìè ðàññìàòðèâàþòñÿ äåòåðìèíèðîâàííûå �-àâòîìàòû âèäà A Q� � ��, , � ,
ãäå � — âõîäíîé àëôàâèò, Q — êîíå÷íîå ìíîæåñòâî ñîñòîÿíèé, à � :Q Q� �� —
÷àñòè÷íàÿ ôóíêöèÿ ïåðåõîäîâ.
Ïóñòü q q Q1 2,
, à �
�. Òðîéêó � �q q1 2, ,� , òàêóþ ÷òî q q2 1� � �( , ), íàçî-
âåì ïåðåõîäîì â àâòîìàòå A, à ñèìâîë � — îòìåòêîé ýòîãî ïåðåõîäà.
�-àâòîìàò A Q�� ��, , � íàçûâàåòñÿ öèêëè÷åñêèì, åñëè äëÿ êàæäîãî q Q
ñó-
ùåñòâóþò òàêèå � �1 2,
� è q q Q1 2,
, ÷òî q q1 1� � �( , ) è q q� � �( , )2 2 .
Ñâåðõñëîâî l � � �1 2� â àëôàâèòå � äîïóñòèìî â ñîñòîÿíèè q àâòîìàòà A,
åñëè ñóùåñòâóåò òàêîå ñâåðõñëîâî ñîñòîÿíèé q q q0 1 2�, ãäå q q0 � , ÷òî äëÿ ëþ-
áîãî i � �0 1 2, , , q qi A i i� ��1 1� �( , ). Âñÿêîå òàêîå ñâåðõñëîâî l íàçîâåì ñîîò-
âåòñòâóþùèì ñâåðõñëîâó ñîñòîÿíèé q q q0 1 2� Ñâåðõñëîâî l äîïóñòèìî äëÿ àâòî-
ìàòà A, åñëè îíî äîïóñòèìî õîòÿ áû â îäíîì èç åãî ñîñòîÿíèé.
Îáðàòíîå ñâåðõñëîâî � � � �� �2 1 0 ïðåäñòàâèìî ñîñòîÿíèåì q àâòîìàòà A,
åñëè ñóùåñòâóåò òàêîå îáðàòíîå ñâåðõñëîâî ñîñòîÿíèé � q q q� �2 1 0 , ãäå q q0 � ,
÷òî äëÿ êàæäîãî i � � �1 2, ,� q qi A i i� ��1 1� �( , ).
48 ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2019, òîì 55, ¹ 5
Ôîðìóëû è àâòîìàòû. Ñïåöèôèêàöèÿ â ÿçûêå (ëîãèêå) LP ïðåäñòàâëÿåò ñî-
áîé ôîðìóëó âèäà G tF t� � ( ), ãäå F t( ) — ôîðìóëà ñ îäíîé ñâîáîäíîé ïåðåìåí-
íîé. Ñ ôîðìóëîé G, èíòåðïðåòèðóåìîé íà ìíîæåñòâå Z, àññîöèèðóåòñÿ ìíîæåñ-
òâî Z-ñëîâ â àëôàâèòå �, êàæäîå èç êîòîðûõ ÿâëÿåòñÿ ìîäåëüþ äëÿ G. Ìåæäó îä-
íîìåñòíûìè ïðåäèêàòíûìè ñèìâîëàìè ëîãèêè LP è ñèìâîëàìè àëôàâèòà �
èìååòñÿ âçàèìíî îäíîçíà÷íîå ñîîòâåòñòâèå. Òàêèì îáðàçîì, ìîæíî ñ÷èòàòü, ÷òî
ïðåäèêàòíûå ñèìâîëû ñîâïàäàþò ñ ñèìâîëàìè àëôàâèòà �. Ïðè óñòàíîâëåíèè ñî-
îòâåòñòâèÿ ìåæäó àâòîìàòàìè è ëîãè÷åñêèìè ôîðìóëàìè òå è äðóãèå ðàññìàòðè-
âàþòñÿ êàê ôîðìàëèçìû äëÿ çàäàíèÿ ìíîæåñòâ ñâåðõñëîâ (�-ÿçûêîâ) â îäíîì è
òîì æå àëôàâèòå. Äëÿ �-àâòîìàòà A àññîöèèðóåìûé ñ íèì �-ÿçûê — ýòî ìíîæåñ-
òâî W A( ) ñâåðõñëîâ, äîïóñòèìûõ äëÿ A. Ïåðåõîä îò Z-ñëîâ, àññîöèèðóåìûõ
ñ ôîðìóëàìè, ê ñâåðõñëîâàì îñóùåñòâëÿåòñÿ ïóòåì ðàññìîòðåíèÿ âñåõ ñóôôèê-
ñîâ Z-ñëîâ. Òàêèì îáðàçîì äëÿ ôîðìóëû G, èìåþùåé ìíîæåñòâî ìîäåëåé M G( ),
ïîëó÷àåòñÿ ìíîæåñòâî ñâåðõñëîâ W G w w u
u M G
( ) | ( )
( )
�
{ Suf }� , ãäå Suf ( )u — ìíî-
æåñòâî âñåõ ñóôôèêñîâ Z-ñëîâà u. Àíàëîãè÷íî îïðåäåëÿåòñÿ ìíîæåñòâî îáðàò-
íûõ ñâåðõñëîâ P G g g u
u M G
( ) | ( )
( )
�
{ Pref }� , ãäå Pref ( )u — ìíîæåñòâî âñåõ ïðå-
ôèêñîâ Z-ñëîâà u. Î÷åâèäíî, ÷òî ìíîæåñòâî P G( ) ïðåôèêñíî çàìêíóòîå, ò.å. ïðå-
ôèêñ êàæäîãî îáðàòíîãî ñâðõñëîâà, ïðèíàäëåæàùåãî P G( ), ïðèíàäëåæèò P G( ).
Ôîðìóëà F t( ) ñ åäèíñòâåííîé ñâîáîäíîé ïåðåìåííîé t íàçûâàåòñÿ k-îãðàíè-
÷åííîé ñïðàâà (k
Z), åñëè äëÿ ëþáîãî �
Z çíà÷åíèÿ ôîðìóëû F ( )� íà âñåõ
äâóñòîðîííèõ ñâåðõñëîâàõ, èìåþùèõ îäèíàêîâûå ( )� � k -ïðåôèêñû, ñîâïàäàþò.
Ôîðìóëû F t( ), 0-îãðàíè÷åííûå ñïðàâà, ðàññìàòðèâàþòñÿ êàê ñïîñîá çàäàíèÿ îá-
ðàòíûõ ñâåðõñëîâ. Áóäåì ñ÷èòàòü, ÷òî 0-îãðàíè÷åííàÿ ñïðàâà ôîðìóëà F t( ) èñ-
òèííà íà îáðàòíîì ñâåðõñëîâå g, åñëè F ( )0 èñòèííà íà ëþáîì äâóñòîðîííåì
ñâåðõñëîâå ñ 0-ïðåôèêñîì g. Ôîðìóëà F t( ), 0-îãðàíè÷åííàÿ ñïðàâà, çàäàåò
ìíîæåñòâî R F t( ( )) âñåõ òåõ îáðàòíûõ ñâåðõñëîâ, íà êîòîðûõ îíà èñòèííà.
Ôîðìóëà �tF t( ) íåïðîòèâîðå÷èâà òîãäà è òîëüêî òîãäà, êîãäà ñóùåñòâóåò
òàêîå Z-ñëîâî (ìîäåëü äëÿ �tF t( ), â êàæäîé ïîçèöèè êîòîðîãî èñòèííà F t( ), ò.å.
â ñëó÷àå 0-îãðàíè÷åííîñòè ôîðìóëû F t( ) ñïðàâà êàæäûé k-ïðåôèêñ (k
Z) ýòîãî
Z-ñëîâà ïðèíàäëåæèò R F t( ( )).
��-ðåãóëÿðíûå âûðàæåíèÿ. Äëÿ îïèñàíèÿ ìíîæåñòâ îáðàòíûõ ñâåðõñëîâ
áóäåì èñïîëüçîâàòü ��-ðåãóëÿðíûå âûðàæåíèÿ. Îïðåäåëèì íàä ìíîæåñòâàìè
ñëîâ îïåðàöèè êîíå÷íîé èòåðàöèè « *» è áåñêîíå÷íîé èòåðàöèè « ��» è « Z ».
Ïóñòü R
�* , îïåðàöèè èòåðàöèè íàä R îïðåäåëÿþòñÿ ñëåäóþùèì îáðàçîì:
R r r r nn
* |� �{ 1 2 0� , r Ri
}, çàìåòèì, ÷òî n � 0 ñîîòâåòñòâóåò ïóñòîìó ñëîâó �;
R r r r i r Ri
�
� ��
� �{ äëÿ âñåõ { }}� 2 1 0 0| \ ;
R r r r r r i r Ri
Z Z�
� �{ äëÿ âñåõ { }}� �2 1 0 1 2 | \ � .
Òàêèì îáðàçîì, ðåçóëüòàòîì êîíå÷íîé èòåðàöèè ÿâëÿåòñÿ áåñêîíå÷íîå ìíîæåñòâî
ñëîâ, à ðåçóëüòàòîì áåñêîíå÷íûõ èòåðàöèé — ìíîæåñòâà áåñêîíå÷íûõ ñëîâ.
Âûðàæåíèÿ, íàçûâàåìûå � �-ðåãóëÿðíûìè, ïðåäñòàâëÿþò ñîáîé êîíå÷íûå îáúå-
äèíåíèÿ âûðàæåíèé âèäà R U�� , ãäå R è U — ðåãóëÿðíûå âûðàæåíèÿ, ò.å. âûðàæå-
íèÿ, ïîñòðîåííûå èç ñèìâîëîâ àëôàâèòà � ñ ïîìîùüþ îïåðàöèé îáúåäèíåíèÿ, êîíêà-
òåíàöèè (ñèìâîë êîíêàòåíàöèè áóäåì ÷àñòî îïóñêàòü) è êîíå÷íîé èòåðàöèè. Î÷åâèä-
íî, ÷òî ��-ðåãóëÿðíûå âûðàæåíèÿ îïðåäåëåíû ñèììåòðè÷íî �-ðåãóëÿðíûì
âûðàæåíèÿì, èñïîëüçóþùèì îïåðàöèþ áåñêîíå÷íîé èòåðàöèè « �» [3]. Ïðè îïèñàíèè
ìíîæåñòâ Z-ñëîâ èñïîëüçóþòñÿ âûðàæåíèÿ âèäà R Z , ãäå R — ðåãóëÿðíîå âûðàæåíèå.
Ìíîæåñòâà îáðàòíûõ ñâåðõñëîâ, çàäàâàåìûå ��-ðåãóëÿðíûìè âûðàæåíèÿ-
ìè, íàçûâàþòñÿ ðåãóëÿðíûìè ìíîæåñòâàìè îáðàòíûõ ñâåðõñëîâ, èëè –�-ðåãó-
ëÿðíûìè ìíîæåñòâàìè. Ìíîæåñòâî âñåõ ��-ðåãóëÿðíûõ ìíîæåñòâ çàìêíóòî îò-
íîñèòåëüíî îïåðàöèé ïåðåñå÷åíèÿ «�» è äîïîëíåíèÿ «�» [4], ò.å. åñëè R è Q —
ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2019, òîì 55, ¹ 5 49
��-ðåãóëÿðíûå ìíîæåñòâà, òî ìíîæåñòâà �R è R Q� òàêæå ìîãóò áûòü çàäàíû
��-ðåãóëÿðíûìè âûðàæåíèÿìè. Ïîýòîìó äëÿ çàäàíèÿ ��-ðåãóëÿðíûõ ìíîæåñòâ
íàðÿäó ñ ��-ðåãóëÿðíûìè âûðàæåíèÿìè áóäóò èñïîëüçîâàòüñÿ âûðàæåíèÿ,
ñîäåðæàùèå îïåðàöèè «�» è, âîçìîæíî, «�».
Âûðàæåíèå, ïîëó÷åííîå èç ��-ðåãóëÿðíîãî âûðàæåíèÿ R â ðåçóëüòàòå óäà-
ëåíèÿ âñåõ ïîäâûðàæåíèé âèäà Q * (çàìåíîé èõ ïóñòûì ñëîâîì), îáîçíà÷èì �R.
Ìíîæåñòâà îáðàòíûõ ñâåðõñëîâ, îïðåäåëÿåìûå òàêèìè ��-ðåãóëÿðíûìè âûðàæå-
íèÿìè, èìåþò âèä �
��R èëè W R�� , ãäå R è W çàäàþò êîíå÷íûå ìíîæåñòâà ñëîâ
â àëôàâèòå � .
Çàìåòèì, ÷òî �R R
, áîëåå òîãî, åñëè R � �, òî è �R � �.
ÏÐÎÂÅÐÊÀ ÔÈÊÒÈÂÍÎÑÒÈ ÑÎÑÒÎßÍÈÉ ÀÂÒÎÌÀÒÀ A G�( )
Íàïîìíèì, ÷òî íîðìàëüíàÿ ôîðìà ôîðìóëû F t( ) â ñïåöèôèêàöèè G tF t� � ( )
èìååò âèä � �
�i
n
i iF t f t
1
1( ) ( ), ãäå f ti ( ) — äèçúþíêöèÿ àòîìàðíûõ ôîðìóë âèäà
�( )t , �
�. Ñîñòîÿíèÿ àâòîìàòà �A G( ), ñîîòâåòñòâóþùåãî íîðìàëüíîé ôîðìå
ôîðìóëû F t( ), îïðåäåëÿþòñÿ ôîðìóëàìè F t F tn1 ( ), , ( )� . Åñëè êàêàÿ-ëèáî èç
ýòèõ ôîðìóë òîæäåñòâåííî ëîæíà íà âñåõ ìîäåëÿõ äëÿ ôîðìóëû G, òî ñîîò-
âåòñòâóþùåå åé ñîñòîÿíèå íàçûâàåòñÿ ôèêòèâíûì è äîëæíî áûòü óäàëåíî èç
àâòîìàòà �A G( ). Ýòî ñâîéñòâî ôîðìóëû F ti ( ) â òåðìèíàõ ìíîæåñòâ îáðàòíûõ
ñâåðõñëîâ õàðàêòåðèçóåòñÿ âûðàæåíèåì R F t P Gi( ( )) ( )� � �.
Èç àëãîðèòìà ñèíòåçà �-àâòîìàòà [1] ñëåäóåò, ÷òî äëÿ êàæäîé ôîðìóëû F ti ( )
ñóùåñòâóþò òàêèå �
� è F tj ( ), ÷òî R F t R F ti j( ( )) ( ( ))�
� , ò.å. èç êàæäîãî ñî-
ñòîÿíèÿ àâòîìàòà �A G( ) èìååòñÿ ïåðåõîä â íåêîòîðîå åãî ñîñòîÿíèå. Â ïðîöåññå
ïîñòðîåíèÿ àâòîìàòà �A G( ) ñîñòîÿíèÿ, ïåðåõîäû â êîòîðûå îòñóòñòâóþò, ñëåäóåò
óäàëÿòü, ïîýòîìó ýòîò �-àâòîìàò áóäåì ñ÷èòàòü öèêëè÷åñêèì.
Óòâåðæäåíèå 1. Åñëè ñîñòîÿíèå q àâòîìàòà �A G( ) íå ôèêòèâíî, òî âñå äîñ-
òèæèìûå èç íåãî ñîñòîÿíèÿ òàêæå íå ôèêòèâíû.
Äîêàçàòåëüñòâî. Ïóñòü ñîñòîÿíèå qi àâòîìàòà �A G( ) íå ôèêòèâíî, ò.å.
R F t P Gi( ( )) ( )� � �, è îáðàòíîå ñâåðõñëîâî g ïðèíàäëåæèò R F t P Gi( ( )) ( )� . Òà-
êèì îáðàçîì, â êàæäîé ïîçèöèè îáðàòíîãî ñâåðõñëîâà g èñòèííà îäíà èç ôîðìóë
F t f tj j( ) ( )�1 , j n
{ }1 2, , ,� . Âñëåäñòâèå öèêëè÷íîñòè �-àâòîìàòà �A G( ) äëÿ ëþ-
áîãî ñîñòîÿíèÿ qk , äîñòèæèìîãî èç qi , ñóùåñòâóåò íà÷èíàþùàÿñÿ â qi è ñîäåð-
æàùàÿ qk êâàçèïåðèîäè÷åñêàÿ ïîñëåäîâàòåëüíîñòü ñîñòîÿíèé, êàæäîå ñîñòîÿíèå
êîòîðîé äîñòèæèìî èç qi . Ïóñòü ñâåðõñëîâî l â àëôàâèòå � ñîîòâåòñòâóåò ýòîé
ïîñëåäîâàòåëüíîñòè ñîñòîÿíèé. Ïîñêîëüêó íà îáðàòíîì ñâåðõñëîâå g èñòèííà
ôîðìóëà F ti ( ), â ñèëó óñëîâèÿ 2 òåîðåìû î ñïåöèôèêàöèè, êîòîðîìó óäîâëåòâî-
ðÿåò íîðìàëüíàÿ ôîðìà ôîðìóëû F t( ) [1], â êàæäîé ïîçèöèè Z -ñëîâà g l� èñòèí-
íà îäíà èç ôîðìóë F t f tj j( ) ( )�1 , j n
{ }1 2, , ,� . Òàêèì îáðàçîì, Z-ñëîâî g l� —
ìîäåëü äëÿ ñïåöèôèêàöèè G. Î÷åâèäíî, ÷òî ñîñòîÿíèå qk íå ôèêòèâíî, ïîñêîëü-
êó ñóùåñòâóåò ìîäåëü äëÿ G, èìåþùàÿ ïðåôèêñ, ïðèíàäëåæàùèé R F tk( ( )).
Ñëåäñòâèå 1. Åñëè ñîñòîÿíèå q àâòîìàòà �A G( ) ôèêòèâíî, òî âñå ñîñòîÿíèÿ,
èç êîòîðûõ îíî äîñòèæèìî, òàêæå ôèêòèâíû. Äîêàçûâàåòñÿ îò ïðîòèâíîãî.
Ââåäåì íåêîòîðûå ïîíÿòèÿ, õàðàêòåðèçóþùèå ñòðóêòóðó öèêëè÷åñêîãî �-àâ-
òîìàòà. Ìíîæåñòâî âñåõ ñîñòîÿíèé �-àâòîìàòà A ìîæíî ðàçáèòü íà ìàêñèìàëü-
íûå ñèëüíî ñâÿçíûå ïîäàâòîìàòû, ÷àñòè÷íî óïîðÿäî÷åííûå îòíîøåíèåì äîñòè-
æèìîñòè. Ìàêñèìàëüíûé ñèëüíî ñâÿçíûé ïîäàâòîìàò, íå äîñòèæèìûé íè èç êà-
êîãî äðóãîãî ìàêñèìàëüíîãî ñèëüíî ñâÿçíîãî ïîäàâòîìòà àâòîìàòà A, íàçûâàåòñÿ
íà÷àëüíûì (ÍÑÑÏ). Î÷åâèäíî, ÷òî êàæäîå ñîñòîÿíèå àâòîìàòà A äîñòèæèìî èç
íåêîòîðîãî íà÷àëüíîãî ñèëüíî ñâÿçíîãî åãî ïîäàâòîìàòà.
Èç óòâåðæäåíèÿ 1 ñëåäóåò, ÷òî åñëè â ÍÑÑÏ èìååòñÿ íåôèêòèâíîå ñîñòîÿ-
íèå, òî âñå åãî ñîñòîÿíèÿ íåôèêòèâíû, è íàîáîðîò, åñëè â ÍÑÑÏ èìååòñÿ ôèê-
òèâíîå ñîñòîÿíèå, òî âñå åãî ñîñòîÿíèÿ ôèêòèâíû. Òàêèì îáðàçîì, ëèáî âñå ñî-
50 ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2019, òîì 55, ¹ 5
ñòîÿíèÿ ÍÑÑÏ ôèêòèâíû, ëèáî âñå îíè íåôèêòèâíû. Ýòî ïîçâîëÿåò ïðè àíàëèçå
ôèêòèâíîñòè ñîñòîÿíèé îãðàíè÷èòüñÿ òîëüêî ñîñòîÿíèÿìè íà÷àëüíûõ ñèëüíî
ñâÿçíûõ ïîäàâòîìàòîâ. Åñëè â àâòîìàòå åñòü ôèêòèâíûå ñîñòîÿíèÿ, òî èìååòñÿ
ÍÑÑÏ, âñå ñîñòîÿíèÿ êîòîðîãî ôèêòèâíû. Íàçîâåì òàêîé ÍÑÑÏ ôèêòèâíûì. Âñå
ôèêòèâíûå ñîñòîÿíèÿ — ýòî ñîñòîÿíèÿ, êîòîðûå äîñòèæèìû òîëüêî èç ñîñòîÿíèé
òàêèõ ÍÑÑÏ. Óäàëèâ âñå ôèêòèâíûå ÍÑÑÏ è ñîñòîÿíèÿ, äîñòèæèìûå òîëüêî èç
íèõ, ïîëó÷èì �-àâòîìàò, íå ñîäåðæàùèé ôèêòèâíûõ ñîñòîÿíèé.  äàëüíåéøåì
áóäåì ðàññìàòðèâàòü òîëüêî ñèëüíî ñâÿçíûå àâòîìàòû è èõ ñïåöèôèêàöèè.
Êàê ïîêàçàíî â [5], äëÿ ëþáîé LP-ôîðìóëû G âèäà �tF t( ) ñóùåñòâóåò ñèììåò-
ðè÷íàÿ åé LF-ôîðìóëà
~
G , äëÿ êîòîðîé W G P G(
~
) ( )�
� , ò.å. W G(
~
) ïðåäñòàâëÿåò ñî-
áîé ìíîæåñòâî ñâåðõñëîâ, èíâåðñíûõ îáðàòíûì ñâåðõñëîâàì èç P G( ). Èçâåñ-
òíî [5], ÷òî ìíîæåñòâî W G(
~
) ìîæåò áûòü çàäàíî LTL-ôîðìóëîé âèäà G�. Îòñþäà ñëå-
äóåò, ÷òî ìíîæåñòâî W G(
~
) �-ðåãóëÿðíîå. Â [3, 6] ïîêàçàíî, ÷òî âñÿêîå �-ðåãóëÿðíîå
ìíîæåñòâî ñîäåðæèò êâàçèïåðèîäè÷åñêèå (ultimately periodic) ñâåðõñëîâà è ïîëíîñòüþ
îïðåäåëÿåòñÿ ìíîæåñòâîì ñîäåðæàùèõñÿ â íåì òàêèõ ñâåðõñëîâ, à çíà÷èò, P G( ) ñîäåð-
æèò êâàçèïåðèîäè÷åñêèå îáðàòíûå ñâåðõñëîâà. Ïîñêîëüêó äëÿ âñÿêîãî îáðàòíîãî ñâåðõ-
ñëîâà èç P G( ) ëþáîé åãî ïðåôèêñ ïðèíàäëåæèò P G( ), ýòî ìíîæåñòâî âñåãäà ñîäåðæèò
ïåðèîäè÷åñêèå îáðàòíûå ñâåðõñëîâà. Ñëåäîâàòåëüíî, åñëè ìíîæåñòâî R F t( ( )) íå ñî-
äåðæèò ïåðèîäè÷åñêèõ îáðàòíûõ ñâåðõñëîâ, òî ôîðìóëà G ïðîòèâîðå÷èâà. Òàêèì îáðà-
çîì, óñëîâèå íåïðîòèâîðå÷èâîñòè ôîðìóëû G tF t� � ( ) ìîæíî ñôîðìóëèðîâàòü òàê:
ôîðìóëà G íåïðîòèâîðå÷èâà òîãäà è òîëüêî òîãäà, êîãäà ñóùåñòâóåò ïåðèîäè÷åñêîå îá-
ðàòíîå ñâåðõñëîâî, êàæäûé ïðåôèêñ êîòîðîãî ïðèíàäëåæèò R F t( ( )).
Ïðè àíàëèçå ôèêòèâíîñòè ÍÑÑÏ áóäåì ðàññìàòðèâàòü òîëüêî ïåðèîäè÷åñ-
êèå îáðàòíûå ñâåðõñëîâà, ïðåäñòàâèìûå ñîñòîÿíèÿìè ýòîãî ïîäàâòîìàòà. Ïåðèî-
äè÷åñêèå îáðàòíûå ñâåðõñëîâà, ïðåäñòàâèìûå ñîñòîÿíèÿìè ÍÑÑÏ, îïðåäåëÿþòñÿ
öèêëàìè â ãðàôå ïåðåõîäîâ ýòîãî àâòîìàòà.
Öèêëîì (äëèíû k) íàçûâàåòñÿ òàêàÿ ïîñëåäîâàòåëüíîñòü ÷åðåäóþùèõñÿ ñî-
ñòîÿíèé è îòìåòîê ïåðåõîäîâ ( , , , , , , )q q qk k0 1 1 2 1� � �� � , ÷òî äëÿ âñåõ
0 1 � �i k � �( , )q qi i i� ��1 1, à � �( , )q qk k� �1 0 . Î÷åâèäíî, ÷òî ñëîâî
� � �1 2 � k ïåðåâîäèò ñîñòîÿíèå q0 â ñåáÿ. Òàêîìó öèêëó ñòàâÿòñÿ â ñîîòâåòñòâèå
Z-ñëîâî ( )� � �1 2 � k
Z è îáðàòíîå ñâåðõñëîâî ( )� � � �
1 2 � k
� , ïðåäñòàâèìîå ñî-
ñòîÿíèåì q0 . Öèêë íàçûâàåòñÿ îñíîâíûì, åñëè ñîîòâåòñòâóþùåå åìó ïåðèîäè-
÷åñêîå Z-ñëîâî ÿâëÿåòñÿ ìîäåëüþ äëÿ ñïåöèôèêàöèè ÍÑÑÏ.
Óòâåðæäåíèå 2. Åñëè ñïåöèôèêàöèÿ G íåïðîòèâîðå÷èâà, òî ëþáîé ïðåôèêñ
èç P G( ) ïðåäñòàâèì íåêîòîðûì ñîñòîÿíèåì ñïåöèôèöèðóåìîãî åþ àâòîìàòà A G( ).
Äîêàçàòåëüñòâî. Ïóñòü u — ìîäåëü äëÿ ôîðìóëû G, à g0 2 1 0� � �� � � � —
íåêîòîðûé åå ïðåôèêñ. Ýòîò ïðåôèêñ îäíîçíà÷íî îïðåäåëÿåò ñîñòîÿíèå àâ-
òîìàòà A G( ), ñêàæåì, ñîñòîÿíèå q0 [7]. Ïóñòü ïðåôèêñ g�1 òàêîé, ÷òî
g g� �1 0 0� , à q�1 — ñîñòîÿíèå, îïðåäåëÿåìîå ïðåôèêñîì g�1. Â ñîîòâåòñòâèè
ñ äåòåðìèíèðîâàííîé àâòîìàòíîé ñåìàíòèêîé ÿçûêà LP � �A q q( , )� �1 0 0 .
 ñèëó ïðîèçâîëüíîãî âûáîðà ïðåôèêñà g0 äëÿ ëþáîãî i � � � �1 2, , èìååì
� �A i i iq q( , )� ��1 1. Îòñþäà ñëåäóåò, ÷òî îáðàòíîå ñâåðõñëîâî � � � �� �2 1 0
ïðåäñòàâèìî ñîñòîÿíèåì q0 àâòîìàòà A G( ).
Ïîêàæåì, ÷òî ÍÑÑÏ, èìåþùèé îñíîâíîé öèêë, íå ôèêòèâåí. Ïóñòü ÍÑÑÏ
ñîäåðæèò îñíîâíîé öèêë ( , , , , , , )q q qk k0 1 1 2 1� � �� � . Òàê êàê Z-ñëîâî
( )� � �1 2 � k
Z ÿâëÿåòñÿ ìîäåëüþ äëÿ ñïåöèôèêàöèè ÍÑÑÏ, à çíà÷èò, è äëÿ ôîð-
ìóëû G, îáðàòíîå ñâåðõñëîâî ( )� � � �
1 2 � k
� ïðèíàäëåæèò P G( ). Ýòî îáðàòíîå
ñâåðõñëîâî ïðåäñòàâèìî ñîñòîÿíèåì q0 . Êàê ïîêàçàíî â [7], êàæäûé ïðåôèêñ
èç P G( ) ïðèíàäëåæèò îäíîìó (è òîëüêî îäíîìó) èç ìíîæåñòâ R F ti( ( )). Òàêèì
îáðàçîì, åñëè îáðàòíîå ñâåðõñëîâî g ïðèíàäëåæèò P G( ) è ïðåäñòàâèìî ñîñòî-
ÿíèåì qi , òî îíî ïðèíàäëåæèò R F ti( ( )), ñëåäîâàòåëüíî, R F t P G( ( )) ( )0 � � �, ÷òî
ÿâëÿåòñÿ óñëîâèåì íåôèêòèâíîñòè ñîñòîÿíèÿ q0 , à çíà÷èò, è âñåãî ÍÑÑÏ. Èòàê, ïðî-
âåðêà íåôèêòèâíîñòè ÍÑÑÏ ñâîäèòñÿ ê ïðîâåðêå íàëè÷èÿ â íåì îñíîâíîãî öèêëà.
ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2019, òîì 55, ¹ 5 51
Ïðîâåðêà òîãî, ôèêòèâåí ÍÑÑÏ èëè íåò, îñíîâàíà íà ïðåäñòàâëåíèè ôîðìóë
âèäà F t( ) ��-ðåãóëÿðíûìè ìíîæåñòâàìè R F t( ( )) çàäàâàåìûõ èìè îáðàòíûõ
ñâåðõñëîâ. Ïîýòîìó ïðèâåäåì íåîáõîäèìûå ñâåäåíèÿ î ��-ðåãóëÿðíûõ ìíî-
æåñòâàõ, çàäàâàåìûõ ôîðìóëàìè F t( ).
ÔÎÐÌÓËÛ F t( ) È ÇÀÄÀÂÀÅÌÛÅ ÈÌÈ ��-ÐÅÃÓËßÐÍÛÅ ÌÍÎÆÅÑÒÂÀ
Íîðìàëüíóþ ôîðìó ôîðìóëû F t F t f t
i
n
i i( ) ( ) ( )� � �
�1
1 áóäåì çàäàâàòü â âèäå
ìíîæåñòâà ïàð � � �R R F ti i i( ( )), � (i n�1 2, , ,� ), ãäå �i — ìíîæåñòâî ñèìâîëîâ
àëôàâèòà �, çàäàâàåìîå ôîðìóëîé f ti ( ), ò.å. �i it f t� �{ }� �| ( ) ( ) . Ýòî òå ñèìâî-
ëû, äëÿ êîòîðûõ îïðåäåëåí ïåðåõîä èç ñîñòîÿíèÿ qi , ñîîòâåòñòâóþùåãî ôîðìóëå F ti ( ).
Ïðèâåäåì íåêîòîðûå ïðàâèëà, ïîçâîëÿþùèå óñòàíàâëèâàòü ñîîòâåòñòâèå
ìåæäó ôîðìóëîé F t( ) è ��-ðåãóëÿðíûì âûðàæåíèåì R F t( ( )). Áóäåì ðàññìàòðè-
âàòü � �-ðåãóëÿðíûå âûðàæåíèÿ â àëôàâèòå � � { }a b c, , ,� .
Ôîðìóëå a t( ) (a
�) ñîîòâåòñòâóåò ��-ðåãóëÿðíîå âûðàæåíèå �
��a, çàäàþ-
ùåå ìíîæåñòâî âñåõ îáðàòíûõ ñâåðõñëîâ â àëôàâèòå � , çàêàí÷èâàþùèõñÿ ñèìâî-
ëîì a. Ôîðìóëå a t k( )� ñîîòâåòñòâóåò ��-ðåãóëÿðíîå âûðàæåíèå � �
��a k .
Åñëè ôîðìóëàì F t1 ( ) è F t2 ( ) ñîîòâåòñòâóþò ��-ðåãóëÿðíûå âûðàæåíèÿ R1 è R2 ,
òî ôîðìóëû F t F t1 2( )& ( ) è F t F t1 2( ) ( )� çàäàþò ìíîæåñòâà R R1 2� è R R1 2� .
Çàìåòèì, ÷òî êîíúþíêöèè a t b t( ) ( )�1 ñîîòâåòñòâóåò ��-ðåãóëÿðíîå âûðàæåíèå
� � �
� �
�
� �a b = �
��ab.
Äëÿ ÷àñòî âñòðå÷àþùèõñÿ â ñïåöèôèêàöèÿõ ôîðìóë c êâàíòîðàìè ïðèâåäåì
ñîîòâåòñòâóþùèå èì ��-ðåãóëÿðíûå âûðàæåíèÿ:
1) F t t t t a t( ) ( ) ( )� � 1 1 1 , R F t a( ( )) *�
�
� �
� ;
2) F t t t t a t t t t t b t( ) ( ) ( ) ( ) ( )� � � � �1 1 1 2 1 2 2 , R F t ab( ( )) *�
�
�
� ;
3) F t t t t a t( ) ( ) ( )� � �1 1 1 , R F t a( ( )) �
�� ;
4) F t t t t t t t a t( ) ( ) ( ) ( )� � � � 1 1 2 2 1 2 , R F t a( ( )) ( )*
�
�
�
� — ìíîæåñòâî
âñåõ îáðàòíûõ ñâåðõñëîâ, ñîäåðæàùèõ áåñêîíå÷íîå êîëè÷åñòâî ñèìâîëîâ a;
5) F t t t t t t t a t( ) ( ) ( ) ( )� � � �1 1 2 2 1 2 , R F t a( ( )) *
�
��
� ;
6) F t t t t a t t t t b t t t t t( ) ( ) ( ) (( ) ( )) (( )� � � � � � � 1 1 1 2 2 1 2 3 1 3 � c t( ))3 ,
R F t b ac( ( )) *�
�� ;
7) F t t t t a t b t b t a t b t( ) ( ) ( ( ) ( ) ( ) ( )) ( )� � � � � �1 1 1 1 1 11 1 = F t b t1 ( ) ( ), çäåñü
R F t( ( ))1 = ( ) ( )ab ba� �
�
� � , à R F t ab ba b( ( )) (( ) ( ) )� � �
� � �� � �
� = ( )ab �� ;
8) F t t t t a t b t( ) ( ) ( ( ) ( ))� � � � �1 1 1 11 , R F t b a b( ( )) *� �
� �� �
� ;
9) F t t t t b t t t t a t( ) ( ) ( ) ( ) ( )� � � �1 1 1 2 2 1 21 , R F t a b( ( )) * *
�
�
� � �
� .
Ðàññìîòðèì ïðèìåð ïðåäñòàâëåíèÿ íîðìàëüíîé ôîðìû ôîðìóëû F t( ) ÿçû-
êà LP â òåðìèíàõ � �-ðåãóëÿðíûõ âûðàæåíèé.
Ïðèìåð 1. Ïóñòü F t F t a t b t c t F t d t( ) ( )( ( ) ( ) ( )) ( ) ( )� � � � � �1 21 1 , ãäå
F t t t t a t t t t b t t t t t1 1 1 1 2 2 1 2 3 1 3( ) ( ) ( ) (( ) ( )) ((� � � � � � � ) ( ( ) ( )))� �a t b t3 3 ,
F t t t t c t t t t t d t2 1 1 1 2 1 2 2( ) ( ) ( ) ( ) ( )� � � � � .
Íåòðóäíî óáåäèòüñÿ, ÷òî ýòî íîðìàëüíàÿ ôîðìà [1]. Ïðèìåíèâ ñîîòâåòñòâèÿ 6) è 2),
ïîëó÷èì ñëåäóþùåå ïðåäñòàâëåíèå ñïåöèôèêàöèè:
R b a a b1 � �
�� ( )* , �1 � { }a b c, , ; R cd2 �
�
�
� * , �2 � { }d .
Ïðèâåäåì íåñêîëüêî ïðîñòûõ ðàâíîñèëüíîñòåé äëÿ ��-ðåãóëÿðíûõ âûðà-
æåíèé. Òàê, äëÿ R R1 2, *
� èìååì � �
� �
�
� �R1
* , ïîñêîëüêó �
R1
* ,
� � �
� � �
� �
� � �R R R R R R1 2 1 1 2 2
* * , ( ) ( )* * * *R R R R1 2 1 2� � , ( ) (* *R R R1 2 1
�
� �
�
52 ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2019, òîì 55, ¹ 5
�
�R
2
) � , R R R R1 2 1 2� � �* * *( )� � � . Çàìåòèì, ÷òî ïîñëåäíÿÿ ðàâíîñèëüíîñòü
íå èìååò ìåñòà äëÿ ïåðåñå÷åíèÿ.
ÀÍÀËÈÇ ÖÈÊËÎÂ Â ÍÑÑÏ
Ïðèâåäåì ðÿä ðåçóëüòàòîâ, èñïîëüçóåìûõ ïðè ïðîâåðêå ôèêòèâíîñòè ÍÑÑÏ.
Òåîðåìà 1. Öèêë â ãðàôå ÍÑÑÏ îñíîâíîé, åñëè è òîëüêî åñëè â êàêîé-ëèáî
ïîçèöèè ñîîòâåòñòâóþùåãî åìó Z-ñëîâà èñòèííà îäíà èç ôîðìóë F ti ( ), îïðåäåëÿ-
þùàÿ íåêîòîðîå ñîñòîÿíèå ýòîãî öèêëà.
Äîêàçàòåëüñòâî. Íåîáõîäèìîñòü î÷åâèäíà, ïîêàæåì äîñòàòî÷íîñòü.
Ðàññìîòðèì öèêë âèäà ( , , , , , , )q q qk k0 1 1 2 1� � �� � . Ïóñòü â ïîçèöèè Z -ñëî-
âà ( )� � �1 2 � k
Z , ñîîòâåòñòâóþùåé ñèìâîëó � i â íåì, èñòèííà ôîðìóëà F ti ( ),
îïðåäåëÿþùàÿ íåêîòîðîå ñîñòîÿíèå öèêëà. Òîãäà â ïîçèöèè �1 èñòèííà ôîðìó-
ëà F t ti i( ) ( )� �1 1� ïðè i k� èëè ôîðìóëà F t ti ( ) ( )�1 1� ïðè i k� . Çäåñü � i t( ) —
ôîðìóëà, èñòèííàÿ â ïîçèöèè t Z-ñëîâà, åñëè â íåé íàõîäèòñÿ ñèìâîë � i . Òàêèì
îáðàçîì, ñîãëàñíî óñëîâèþ 2 òåîðåìû î ñïåöèôèêàöèè â êàæäîé ïîçèöèè
�
ýòîãî Z-ñëîâà èñòèííà îäíà èç ôîðìóë F t f tj j( ) ( )�1 ( j k
�{ }0 1 1, , ,� ), ò.å. ôîð-
ìóëà F t( ). Èñòèííîñòü ôîðìóëû F t( ) â ïîçèöèÿõ, ìåíüøèõ �1, ñëåäóåò èç ïåðè-
îäè÷íîñòè Z-ñëîâà. Òàê, F ti ( ) èñòèííà â ëþáîé ïîçèöèè � kn ( , , , )n � 0 1 2 � è,
ñëåäîâàòåëüíî, ( )� � �1 2 � k
Z — ìîäåëü äëÿ ñïåöèôèêàöèè ÍÑÑÏ.
Çàìåòèì, ÷òî ìîæåò ñóùåñòâîâàòü ïåðèîäè÷åñêîå Z-ñëîâî, êàæäûé ïðåôèêñ
êîòîðîãî ïðèíàäëåæèò îäíîìó èç ìíîæåñòâ R F ti( ( )), íå ÿâëÿþùååñÿ ìîäåëüþ,
åñëè îíî íå ñîîòâåòñòâóåò íè îäíîìó öèêëó â ãðàôå ÍÑÑÏ.
Ïðèìåð 2. Ñïåöèôèêàöèÿ ôîðìóëû F t( ) â ðåãóëÿðíûõ âûðàæåíèÿõ èìååò
âèä R ab1 �
�
�
� * , �1 � { }b c, ; R cb2 �
�
�
� * , �2 � { }a b, . Íåòðóäíî óáåäèòüñÿ, ÷òî
R R1 2� � � è R b R1 1
, R c R1 2
, R a R2 1
, R b R2 2
. Ýòè âêëþ÷åíèÿ îïðåäå-
ëÿþò àâòîìàò, èçîáðàæåííûé íà ðèñ. 1.
Ðàññìîòðèì öèêë (2, a, 1, c), êîòîðîìó ñîîòâåòñòâóåò îáðàòíîå ñâåðõñëîâî
( )ac �� . Î÷åâèäíî, ÷òî åãî ïðåôèêñ ( )ac ��
ïðèíàäëåæèò R2 , èç ÷åãî ñëåäóåò, ÷òî öèêë
îñíîâíîé. Öèêëû ( 1, b) è (2, b) íå îñíîâ-
íûå, ïîñêîëüêó ïðåôèêñû îáðàòíîãî ñâåðõ-
ñëîâà b�� íå ïðèíàäëåæàò íè R1, íè R2 .
Òàêèì îáðàçîì, ïðîâåðêà òîãî, ÿâëÿåò-
ñÿ öèêë îñíîâíûì èëè íåò, ñâîäèòñÿ ê ïðî-
âåðêå ïðèíàäëåæíîñòè ïåðèîäè÷åñêîãî îáðàòíîãî ñâåðõñëîâà îäíîìó èç ìíîæåñòâ
R F ti( ( )), ãäå ôîðìóëà F ti ( ) ñîîòâåòñòâóåò íåêîòîðîìó ñîñòîÿíèþ öèêëà.
Ôîðìóëû âèäà F ti ( )�1 â íîðìàëüíîé ôîðìå ôîðìóëû F t( ) ÷àñòî ïðåä-
ñòàâëÿþò ñîáîé ïðîèçâåäåíèÿ áîëåå ïðîñòûõ ôîðìóë èëè èõ îòðèöàíèé, ÷òî
ñîîòâåòñòâóåò ïåðåñå÷åíèþ ��-ðåãóëÿðíûõ ìíîæåñòâ èëè èõ äîïîëíåíèé. Ïðè
ïðîâåðêå ïðèíàäëåæíîñòè ïåðèîäè÷åñêîãî îáðàòíîãî ñâåðõñëîâà òàêîìó ìíî-
æåñòâó ìîæíî íå âû÷èñëÿòü ñîîòâåòñòâóþùåãî åìó ��-ðåãóëÿðíîãî âûðàæåíèÿ,
à âûïîëíÿòü ýòó ïðîâåðêó äëÿ îòäåëüíûõ åãî êîìïîíåíòîâ. Î÷åâèäíî, ÷òî
g R R
�1 2 , åñëè g R
1, g R
2 , è g R
� , åñëè g R� .
Òåîðåìà 2. Åñëè ñïåöèôèêàöèÿ öèêëà ( , , , , , , )q q qk k0 1 1 2 1� � �� � óäîâëåò-
âîðÿåò ñîîòíîøåíèÿì � �R R0 1 1�
, � � , , � �R R R Rk k1 2 2 1 0� �
�� , ãäå R R F ti i� ( ( )),
i k� �0 1 1, , ,� , òî îí îñíîâíîé.
Äîêàçàòåëüñòâî. Ïîêàæåì, ÷òî ( )� � �1 2 � k
Z — ìîäåëü äëÿ ñïåöèôèêàöèè
öèêëà (â ñîîòâåòñòâóþùåì ÍÑÑÏ).
1. Ïóñòü �R R0 �
�
�
� . Îáðàòíîå ñâåðõñëîâî g ïðèíàäëåæèò �R0 , åñëè îíî èìå-
åò ñóôôèêñ, ïðèíàäëåæàùèé R. Ïóñòü ìàêñèìàëüíàÿ äëèíà ñëîâ èç R ðàâíà n.
Åñëè îáðàòíîå ñâåðõñëîâî g ïðèíàäëåæèò �R0 , òî äëÿ ëþáîãî p � 0
ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2019, òîì 55, ¹ 5 53
21
cb b
a
Ðèñ. 1
g Rk
p( ) �� � �1 2 0�
. Âûáåðåì p òàêèì, ÷òî kp n� . Òîãäà êàêîå-òî ñëîâî èç R áó-
äåò ñóôôèêñîì ñëîâà ( )� � �1 2� k
p . Ñëåäîâàòåëüíî, ïðåôèêñ Z-ñëîâà
( )� � �1 2 � k
Z ñ òàêèì ñóôôèêñîì ïðèíàäëåæèò �R0 , à çíà÷èò, è R0 . Òàêèì îáðà-
çîì, ñîãëàñíî òåîðåìå 1 Z-ñëîâî ( )� � �1 2 � k
Z ÿâëÿåòñÿ ìîäåëüþ äëÿ
ñïåöèôèêàöèè ÍÑÑÏ.
2. Ïóñòü � ( )R Q S0 1 1�
�� , ãäå Q1, S1 — êîíå÷íûå ìíîæåñòâà ñëîâ, è g R
�
0 .
Òîãäà äëÿ ëþáîãî p � 0 g Rk
p( ) �� � �1 2 0�
. Ïðè äîñòàòî÷íî áîëüøîì p ñëîâî
( )� � �1 2� k
p èìååò ñóôôèêñ r S1 1
. Óäàëèâ èç ( )� � �1 2� k
p ýòîò ñóôôèêñ,
ï î ëó÷èì ñëîâî r k
p
i� �( )� � � � �1 2 1 1
1� � ( p p i k1 � , ) òàêîå, ÷òî
g Qk
p
i( ) ( )� � � � � �
1 2 1 1 1
1� � �
�
. Ðàññìîòðèì ïåðèîä ( )� � � �i k i� �1 1� ,
î á î ç í à ÷ è â åãî ( )� � �� � �1 2� k . Òàêèì îáðàçîì, ñëîâî r èìååò âèä
� � � � �1 1 1 2
1� �i k
p
� � � �( ) . Êàê áûëî îòìå÷åíî, îáðàòíîå ñâåðõñëîâî
g i k
p� � � � �1 1 1 2
1� �� � � �( ) ïðèíàäëåæèò ìíîæåñòâó ( )Q1
�� è, ñëåäîâàòåëüíî,
ïðåäñòàâëÿåò ñîáîé áåñêîíå÷íóþ êîíêàòåíàöèþ ñëîâ èç Q1 (ôàêòîðîâ). Ðàññìîò-
ðèì ïîñëåäíèå k �1 ýòèõ ôàêòîðîâ � �1 1, ,� k� . Ïðè äîñòàòî÷íî áîëüøîì p ñëî-
âî � �1 1� k� áóäåò ñóôôèêñîì ñëîâà ( )� � �� � �1 2
1� k
p
. Ïîñêîëüêó êàæäûé ôàêòîð
íà÷èíàåòñÿ â íåêîòîðîé ïîçèöèè ñëîâà � � �� � �1 2 � k , ñðåäè íèõ íàéäóòñÿ äâà ôàê-
òîðà, íà÷èíàþùèõñÿ â îäíîé è òîé æå ïîçèöèè ýòîãî ñëîâà. Ïóñòü ýòî ôàêòîðû
� i è � j (i j k� �1), òîãäà îáðàòíîå ñâåðõñëîâî ( )� � � ��
i j j k� ��
�
�1 1
ïðèíàäëåæèò ( )Q1
�� è ñîâïàäàåò ñ ( )� � �
�� � � �
1 2 � k , à ( )� � �
�� � � �
1 2 1� k r ñîâïà-
äàåò ñ ( )� � � �
1 2 � k
� . Òàêèì îáðàçîì, Z-ñëîâî ( )� � �1 2 � k
Z èìååò ïðåôèêñ
( )� � �
�� � � �
1 2 1� k r , ïðèíàäëåæàùèé �R0 , è, ñëåäîâàòåëüíî, ñîãëàñíî òåîðåìå 1 ÿâ-
ëÿåòñÿ ìîäåëüþ äëÿ ñïåöèôèêàöèè ÍÑÑÏ.
Ïðèìåð 3. Ïóñòü
F t t t t c t t t t t c t b t a t( ) ( ) ( ) ( ) ( ( ) ( ))& ( (� � � � � � � �1 1 1 2 1 2 2 2 ) ( ) ( ))� � �b t c t
�� � � � � � �t t t a t t t t t b t b t c t1 1 1 2 1 2 2( ) ( ) ( ( ) ( ))& ( ( ) ( )) =
= F t a t b t c t F t b t c t1 21 1( )( ( ) ( ) ( )) ( )( ( ) ( ))� � � � � � .
Ôîðìóëà F t( ) ïðåäñòàâëåíà â íîðìàëüíîé ôîðìå, ÷òî â òåðìèíàõ ìíîæåñòâ
îáðàòíûõ ñâåðõñëîâ èìååò ñëåäóþùèé âèä: R c c b1 � �
�
�
� ( )* , �1 � { }a b c, , ;
R ab2 �
�
�
� * , �2 � { }b c, . Âûïîëíÿþòñÿ òàêèå âêëþ÷åíèÿ: R c b R1 1( )�
,
R a R1 2
, R b R2 2
, R c R2 1
. Ïîÿñíèì ñïðàâåäëèâîñòü âòîðîãî âêëþ÷åíèÿ:
R a c c b a a ab1 � �
� � �
� � �
� � �( )* * . Ýòè âêëþ÷åíèÿ îïðåäåëÿþò àâòîìàò,
èçîáðàæåííûé íà ðèñ. 2.
Ðàññìîòðèì öèêë (1, a, 2, c). Çäåñü
�R c1 �
�
�
� , �R a2 �
�
�
� . Òàêèì îáðàçîì, èìå-
åì � �R a R1 2
, � �R c R2 1
è, ñëåäîâàòåëüíî,
ñîãëàñíî òåîðåìå 2 ýòîò öèêë îñíîâíîé.
 àâòîìàòå �A G( ), ñîîòâåòñòâóþùåì
ñïåöèôèêàöèè G, äîñòàòî÷íî ÷àñòî âñòðå-
÷àþòñÿ ÍÑÑÏ, ñîñòîÿùèå èç îäíîãî ñîñòî-
ÿíèÿ. Ïðèâåäåì íåêîòîðûå ðåçóëüòàòû, óïðîùàþùèå ïðîâåðêó èõ ôèêòèâíîñòè.
ÏÐÎÂÅÐÊÀ ÔÈÊÒÈÂÍÎÑÒÈ ÍÑÑÏ, ÈÌÅÞÙÅÃÎ ÎÄÍÎ ÑÎÑÒÎßÍÈÅ
Ñïåöèôèêàöèÿ â ÿçûêå LP àâòîìàòà, ñîñòîÿùåãî èç îäíîãî ñîñòîÿíèÿ, èìååò
âèä � � � �tF t t tk1 11( )( ( ) ( ))� �� èëè â òåðìèíàõ ��-ðåãóëÿðíûõ âûðàæåíèé
54 ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2019, òîì 55, ¹ 5
21
ab, c b
c
Ðèñ. 2
� �R F t( ( )),1 1� , ãäå �1 1� { }� �, ,� k . Çäåñü � i
�1 òîãäà è òîëüêî òîãäà, êîãäà
R F t R F ti( ( )) ( ( ))1 1�
.
Óòâåðæäåíèå 3. Ïóñòü G R F t�� �( ( )),1 1� . Ïåðèîäè÷åñêîå Z-ñëîâî r Z , ãäå
r
�1
* , ÿâëÿåòñÿ ìîäåëüþ äëÿ G òîãäà è òîëüêî òîãäà, êîãäà íåêîòîðîé åãî ïîçè-
öèè ñîîòâåòñòâóåò ïðåôèêñ, ïðèíàäëåæàùèé R F t( ( ))1 .
Ýòî óòâåðæäåíèå íåïîñðåäñòâåííî ñëåäóåò èç òåîðåìû 1, ïîñêîëüêó êàæäîå
ïåðèîäè÷åñêîå Z-ñëîâî â àëôàâèòå �1 ñîîòâåòñòâóåò íåêîòîðîìó öèêëó â ÍÑÑÏ
èç îäíîãî ñîñòîÿíèÿ.
Óòâåðæäåíèå 4. Åñëè �R1 èìååò âèä �
��r, ãäå r — ñëîâî, òî ñïåöèôèêàöèÿ
� �R1 1, � ïðîòèâîðå÷èâà, åñëè �1 íå ñîäåðæèò âñåõ ñèìâîëîâ èç r. Î÷åâèäíî, ÷òî
êàæäûé ïðåôèêñ ìîäåëè çàêàí÷èâàåòñÿ ñèìâîëîì èç ��. Åñëè r ñîäåðæèò ñèìâîë,
íå ïðèíàäëåæàùèé �1, òî â ëþáîé ïåðèîäè÷åñêîé ìîäåëè äëÿ ñïåöèôèêàöèè
íàéäåòñÿ ïðåôèêñ, íå çàêàí÷èâàþùèéñÿ ñèìâîëîì èç �1. Íàïðèìåð, ñïåöèôèêà-
öèÿ R ab1 �
�
�
� * , �1 � { }b ïðîòèâîðå÷èâà.
Ïðèìåð 4. Ðàññìîòðèì ñïåöèôèêàöèþ èç
ïðèìåðà 1, ïðåäñòàâëåííóþ â ��-ðåãóëÿðíûõ
âûðàæåíèÿõ:
R b a a b1 � �
�� ( )* , �1 � { }a b c, , ;
R cd2 �
�
�
� * , �2 � { }d .
Äëÿ íåå âûïîëíÿþòñÿ ñëåäóþùèå âêëþ÷åíèÿ: R a b R1 1( )�
, R c R1 2
,
R d R2 2
. Ïîýòîìó åé ñîîòâåòñòâóåò àâòîìàò, èçîáðàæåííûé íà ðèñ. 3.
Ýòîò àâòîìàò èìååò åäèíñòâåííûé ÍÑÑÏ, ïðåäñòàâëåííûé ñîñòîÿíèåì 1. Îí
ôèêòèâíûé, ïîñêîëüêó R1 íå ñîäåðæèò íè îäíîãî ïåðèîäè÷åñêîãî îáðàòíîãî
ñâåðõñëîâà. Ïîñëå åãî óäàëåíèÿ ïîëó÷èì ÍÑÑÏ, ñîñòîÿùèé èç ñîñòîÿíèÿ 2, êîòî-
ðûé òàêæå ôèêòèâåí, ïîñêîëüêó �2 íå ñîäåðæèò ñèìâîëà c èç �R2 . Òàêèì îáðàçîì,
ðàññìàòðèâàåìàÿ ñïåöèôèêàöèÿ ïðîòèâîðå÷èâà.
Åñëè �R1 èìååò âèä �
��r, ãäå r — ñëîâî, ñîñòîÿùåå áîëåå ÷åì èç îäíîãî ñèì-
âîëà, òî â ñîîòâåòñòâóþùåì ÍÑÑÏ íå ñóùåñòâóåò îñíîâíîãî öèêëà äëèíû ìåíåå
| |r , åñëè r r k
� ( )1 (k �1). Íàïðèìåð, åñëè R a b1 �
�
� � �
� * * è �1 � { }a b, , òî
�R ab1 �
�
�
� è R a R1 1
, R b R1 1
, îäíàêî öèêëû (q a1, ) è (q b1, ) íå îñíîâíûå, ïî-
ñêîëüêó íè a �� , íè b�� íå ïðèíàäëåæàò R1.
Óòâåðæäåíèå 5. Åñëè R R1 �
�
�
� , à �R r1 �
�
�
� , ãäå r — ñëîâî â àëôàâèòå �1,
è äëÿ âñåõ �, âñòðå÷àþùèõñÿ â r, � �
� �
� ��R R, òî r Z — ìîäåëü äëÿ ñîîòâåòñòâó-
þùåé ñïåöèôèêàöèè.
Ðàññìîòðèì ïåðèîäè÷åñêîå Z-ñëîâî r Z . Î÷åâèäíî, ÷òî ôîðìóëà, ñîîòâåòñòâó-
þùàÿ ��-ðåãóëÿðíîìó âûðàæåíèþ �
��r, èñòèííà â íåêîòîðîé ïîçèöèè ýòîãî
Z-ñëîâà (à çíà÷èò, èñòèííà è �
��R). Òàêèì îáðàçîì, â ñîîòâåòñòâèè ñ òåîðåìîé 1
r Z ÿâëÿåòñÿ ìîäåëüþ äëÿ ñïåöèôèêàöèè ÍÑÑÏ.
Âîçìîæíî îáîáùåíèå, êîãäà �R R1 �
�
�
� , ãäå R — ìíîæåñòâî ñëîâ. Òîãäà äëÿ
êàæäîãî r R
, óäîâëåòâîðÿþùåãî óñëîâèÿì óòâåðæäåíèÿ 5, r Z — ìîäåëü äëÿ ñî-
îòâåòñòâóþùåé ñïåöèôèêàöèè.
Òåîðåìà 4. Ïóñòü íîðìàëüíàÿ ôîðìà ñïåöèôèêàöèè ÍÑÑÏ, ñîñòîÿùåãî èç
îäíîãî ñîñòîÿíèÿ, èìååò âèä � � �
�R R1 1� �
� , è �R r1 �
�
�
� , ãäå r k� � �1 � .
Ñïåöèôèêàöèÿ íåïðîòèâîðå÷èâà òîãäà è òîëüêî òîãäà, êîãäà äëÿ êàæäîãî
� � �i k
{ }1, ,� � i
�1 è R Ri1 1�
.
Äîêàçàòåëüñòâî íåïîñðåäñòâåííî âûòåêàåò èç óòâåðæäåíèé 4 è 5.
Çàìåòèì, ÷òî åñëè R1 �
�
�
� , òî �R r1 �
�
�
� , ãäå r — íåïóñòîå ñëîâî (ìíîæåñ-
òâî ñëîâ). Ïîýòîìó òåîðåìà 3 îïðåäåëÿåò íåîáõîäèìûå è äîñòàòî÷íûå óñëîâèÿ
íåïðîòèâîðå÷èâîñòè ñïåöèôèêàöèè âèäà � � �
�R R1 1� �
� , , ïðåäñòàâëåííîé
â íîðìàëüíîé ôîðìå.
ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2019, òîì 55, ¹ 5 55
21
c
da, b
Ðèñ. 3
Ïðè àíàëèçå ÍÑÑÏ, ñîñòîÿùåãî èç îäíîãî ñîñòîÿíèÿ, ðàññìàòðèâàëèñü ñïå-
öèôèêàöèè âèäà � � �
�R R1 1� �
� , . Ñëåäóþùàÿ òåîðåìà ïîçâîëÿåò ðàñïðîñòðà-
íèòü ïîëó÷åííûå ðåçóëüòàòû íà ñïåöèôèêàöèè âèäà � � �
�R R1 1
� , � .
Òåîðåìà 5. Ñïåöèôèêàöèè G tF t1 1� � ( ) è G tF t2 2� � ( ), ãäå R F t( ( ))1 =
� � �
��R1 1, R F t( ( ))2 = ( )R1 1
��
� , à � �1
, ýêâèâàëåíòíû, ò.å. èìåþò îäíî è òî
æå ìíîæåñòâî ìîäåëåé.
Äîêàçàòåëüñòâî. 1. Ïåðèîäè÷åñêîå Z-ñëîâî r Z , ãäå r
�1
* , ÿâëÿåòñÿ ìî-
äåëüþ äëÿ G1 òîãäà è òîëüêî òîãäà, êîãäà êàæäûé åãî ïðåôèêñ ïðèíàäëåæèò
� �
��R1 1. Òàêîé ïðåôèêñ èìååò âèä g � �, ãäå �
�1, è êàæäûé ïðåôèêñ îáðàòíî-
ãî ñâåðõñëîâà g ïðèíàäëåæèò �
��R1, ò.å. çàêàí÷èâàåòñÿ ñëîâîì èç R1. Îòñþäà
ñëåäóåò, ÷òî g ìîæåò áûòü ïðåäñòàâëåíî êàê áåñêîíå÷íàÿ êîíêàòåíàöèÿ ñëîâ èç R1,
ò.å. g R
�( )1
� . Ñîãëàñíî óòâåðæäåíèþ 3 Z-ñëîâî r Z — ìîäåëü äëÿ G2 , ïîñêîëü-
êó èìååò ïðåôèêñ, ïðèíàäëåæàùèé ( )R1
�� . Òàêèì îáðàçîì, êàæäàÿ ïåðèîäè÷åñ-
êàÿ ìîäåëü äëÿ ñïåöèôèêàöèè G1 ÿâëÿåòñÿ ìîäåëüþ äëÿ ñïåöèôèêàöèè G2 .
2. Ïåðèîäè÷åñêîå Z-ñëîâî r Z , ãäå r
�1
* , — ìîäåëü äëÿ G2 òîãäà è òîëüêî òîã-
äà, êîãäà îíî èìååò ïðåôèêñ, ïðèíàäëåæàùèé ìíîæåñòâó ( )R1
�� è, ñëåäîâàòåëüíî,
çàêàí÷èâàþùèéñÿ ñëîâîì èç R1. Òàêèì îáðàçîì, Z-ñëîâî r Z èìååò ïðåôèêñ, ïðèíàä-
ëåæàùèé ìíîæåñòâó �
��R1 è ñîãëàñíî óòâåðæäåíèþ 3 ÿâëÿåòñÿ ìîäåëüþ äëÿ G1.
Èç ñîâïàäåíèÿ ìíîæåñòâ ïåðèîäè÷åñêèõ ìîäåëåé äëÿ ñïåöèôèêàöèé G1 è G2
ñëåäóåò, ÷òî ñîâïàäàþò è ìíîæåñòâà ïåðèîäè÷åñêèõ îáðàòíûõ ñâåðõñëîâ, èìåþ-
ùèõñÿ â ìíîæåñòâàõ P G( )1 è P G( )2 . Áóäó÷è ��-ðåãóëÿðíûì, ìíîæåñòâî P G( )
îäíîçíà÷íî îïðåäåëÿåòñÿ èìåþùèìèñÿ â íåì ïåðèîäè÷åñêèìè îáðàòíûìè ñâåðõ-
ñëîâàìè [6], ïîýòîìó ìíîæåñòâà P G( )1 è P G( )2 ñîâïàäàþò, à çíà÷èò, ñîâïàäàþò è
ìíîæåñòâà ìîäåëåé äëÿ ñïåöèôèêàöèé G1 è G2 .
ÇÀÊËÞ×ÅÍÈÅ
Íàñòîÿùàÿ ñòàòüÿ çàâåðøàåò îïèñàíèå ïðîöåññà ñèíòåçà äåòåðìèíèðîâàííîãî
�-àâòîìàòà, ñïåöèôèöèðîâàííîãî ôîðìóëîé ÿçûêà LP. Íà ïåðâîì ýòàïå ñèíòåçà,
îïèñàííîì â [1], ñòðîèòñÿ àâòîìàò �A G( ), ñîîòâåòñòâóþùèé íîðìàëüíîé ôîðìå
ôîðìóëû F t( ) â ñïåöèôèêàöèè G tF t� � ( ). Ýòîò àâòîìàò ìîæåò ñîäåðæàòü
ôèêòèâíûå ñîñòîÿíèÿ, ò.å. ñîñòîÿíèÿ, íå ïðèíàäëåæàùèå àâòîìàòó, ñïåöèôèöèðóå-
ìîìó ôîðìóëîé G. Íà âòîðîì ýòàïå, êîòîðîìó ïîñâÿùåíà äàííàÿ ñòàòüÿ, îñóùåñò-
âëÿåòñÿ íàõîæäåíèå â àâòîìàòå �A G( ) ôèêòèâíûõ ñîñòîÿíèé è èõ óäàëåíèå. Ïî-
êàçàíî, ÷òî ñîîòâåòñòâóþùàÿ çàäà÷à ñâîäèòñÿ ê ïðîâåðêå ôèêòèâíîñòè íà÷àëü-
íûõ ñèëüíî ñâÿçíûõ ïîäàâòîìàòîâ àâòîìàòà �A G( ), ÷òî, â ñâîþ î÷åðåäü, ñâîäèò-
ñÿ ê îïðåäåëåíèþ íàëè÷èÿ â ÍÑÑÏ îñíîâíîãî öèêëà. Öèêë íàçûâàåòñÿ îñíîâ-
íûì, åñëè ñîîòâåòñòâóþùåå åìó ïåðèîäè÷åñêîå îáðàòíîå ñâåðõñëîâî èìååò
ïðåôèêñ, ïðèíàäëåæàùèé íåêîòîðîìó ìíîæåñòâó R F ti( ( )), ãäå ôîðìóëà F ti ( )
ñîîòâåòñòâóåò îäíîìó èç ñîñòîÿíèé ýòîãî öèêëà. Â ñòàòüå ïðåäïîëàãàåòñÿ, ÷òî
äëÿ ïðåäñòàâëåíèÿ ìíîæåñòâ R F ti( ( )) èñïîëüçóþòñÿ ��-ðåãóëÿðíûå âûðàæåíèÿ.
Òàêèì îáðàçîì, çàäà÷à ïðîâåðêè, ÿâëÿåòñÿ ëè ðàññìàòðèâàåìûé öèêë äëèíû k
îñíîâíûì, ñîñòîèò â ïðîâåðêå ïðèíàäëåæíîñòè ïåðèîäè÷åñêîãî îáðàòíîãî
ñâåðõñëîâà íåêîòîðîìó ��-ðåãóëÿðíîìó ìíîæåñòâó. Ýòà çàäà÷à äîñòàòî÷íî ïðî-
ñòàÿ è ñâÿçàíà ñ ïîñòðîåíèåì ìíîæåñòâà âñåõ ñëîâ äëèíû k, ïðèíàäëåæàùèõ
ðåãóëÿðíîìó ìíîæåñòâó. Ââèäó îãðàíè÷åííîñòè îáúåìà ñòàòüè îíà íå ðàññìàò-
ðèâàëàñü. Êðîìå òîãî, ïîëó÷åííûå ðåçóëüòàòû â ñëó÷àå íàëè÷èÿ ëåãêî ïðîâåðÿå-
ìûõ ñâîéñòâ ñïåöèôèêàöèè ïîçâîëÿþò îáõîäèòüñÿ áåç ïðîâåðêè ïðèíàäëåæíîñ-
òè ïåðèîäè÷åñêîãî îáðàòíîãî ñâåðõñëîâà ��-ðåãóëÿðíîìó ìíîæåñòâó.
Îñíîâíàÿ ñëîæíîñòü ïðè ðåàëèçàöèè ïðåäëîæåííîãî ïîäõîäà ê íàõîæäåíèþ ôèê-
òèâíûõ ñîñòîÿíèé ñîñòîèò â ïåðåõîäå îò ôîðìóëû F t( ) ê ìíîæåñòâó R F t( ( )) çàäàâàå-
ìûõ åþ îáðàòíûõ ñâåðõñëîâ. Ïîêà íåèçâåñòåí äîñòàòî÷íî ïðîñòîé ñïîñîá ðåøåíèÿ ýòîé
çàäà÷è.  ñòàòüå ïðèâåäåíû íåêîòîðûå ïðàâèëà ïîñòðîåíèÿ ìíîæåñòâà R F t( ( )) äëÿ îò-
íîñèòåëüíî ïðîñòûõ ôîðìóë F t( ). Ïåðå÷åíü òàêèõ ïðàâèë ìîæíî ñóùåñòâåííî ðàñ-
56 ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2019, òîì 55, ¹ 5
øèðèòü, ÷òî ïîçâîëèò ðåøàòü ðàññìàòðèâàåìóþ çàäà÷ó äëÿ øèðîêîãî êëàññà ñïåöèôè-
êàöèé, ó÷èòûâàÿ, ÷òî áàçîâûå ôîðìóëû, èç êîòîðûõ ñòðîÿòñÿ ïîäôîðìóëû âèäà
F ti ( )�1 â íîðìàëüíîé ôîðìå ôîðìóëû F t( ), êàê ïðàâèëî, íåñëîæíûå.
Ïðîáëåìà íàõîæäåíèÿ ôèêòèâíûõ ñîñòîÿíèé ðàññìàòðèâàëàñü äëÿ àâòîìàòà �A G( ),
ñèíòåçèðîâàííîãî ïî ñïåöèôèêàöèè â ÿçûêå LP ñ äåòåðìèíèðîâàííîé ñåìàíòèêîé.
Àíàëîãè÷íàÿ çàäà÷à âîçíèêàåò äëÿ íåäåòåðìèíèðîâàííîãî àâòîìàòà �A G( ) , ñèíòåçè-
ðîâàííîãî ïî ñïåöèôèêàöèè â ÿçûêå LF. Ðåçóëüòàòû, ïðèâåäåííûå â íàñòîÿùåé
ñòàòüå, ëåãêî àäàïòèðóþòñÿ è äëÿ òàêîãî ñëó÷àÿ.
ÑÏÈÑÎÊ ËÈÒÅÐÀÒÓÐÛ
1. ×åáîòàðåâ À.Í. Ñèíòåç �-àâòîìàòîâ, ñïåöèôèöèðîâàííûõ â ëîãè÷åñêèõ ÿçûêàõ LP è LF. Êèáåðíåòèêà
è ñèñòåìíûé àíàëèç. 2018. Ò. 54, ¹ 4. Ñ. 16–31.
2. ×åáîòàðåâ À.Í. Ñèíòåç ïðîöåäóðíîãî ïðåäñòàâëåíèÿ àâòîìàòà, ñïåöèôèöèðîâàííîãî â ëîãè÷åñêîì
ÿçûêå L*. II. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç. 1997. ¹ 6. Ñ. 115–127.
3. Perrin D., Pin J.- E. Infinite words. Automata, semigroups, logic and games. Pure and applied mathematics
series. Amsterdam: Elsevier, 2004. Vol. 141. 550 p.
4. Bresolin D., Montanari A., Puppis G. A theory of ultimately periodic languages and automata with an
application to time granularity. Acta Informatica. 2009. Vol. 46, N 5. P. 331–360.
5. ×åáîòàðåâ À.Í. Íåêîòîðûå ïîäìíîæåñòâà ìîíàäè÷åñêîé ëîãèêè ïåðâîãî ïîðÿäêà (MFO), èñïîëüçóåìûå
äëÿ ñïåöèôèêàöèè è ñèíòåçà �-àâòîìàòîâ. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç. 2017. Ò. 53, ¹ 4. Ñ. 22–36.
6. Calbrix H., Nivat M., Podelsky A. Ultimately periodic words of rational �-languages. Lecture Notes in
Computer Science. 1994. Vol. 802. P. 554–566.
7. ×åáîòàðåâ À.Í. Ïðîáëåìû ñèíòåçà �-àâòîìàòîâ, ñïåöèôèöèðîâàííûõ â ÿçûêàõ LP è LF ëîãèêè ïåðâî-
ãî ïîðÿäêà. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç. 2017. Ò. 53, ¹ 5. Ñ. 22–33.
Íàä³éøëà äî ðåäàêö³¿ 11.12.2018
À.Ì. ×åáîòàðüîâ
ÂÈÇÍÀ×ÅÍÍß Ô²ÊÒÈÂÍÈÕ ÑÒÀͲ  �-ÀÂÒÎÌÀÒ²,
ÙÎ ÑÈÍÒÅÇÎÂÀÍÈÉ ÇÀ ÑÏÅÖÈÔ²ÊÀÖ²ªÞ Ó Ìβ LP
Àíîòàö³ÿ. Ñèíòåç äåòåðì³íîâàíîãî �-àâòîìàòà, ñïåöèô³êîâàíîãî ìîâîþ LP,
ïîëÿãຠó ïîñë³äîâíîìó âèêîíàíí³ äâîõ ïðîöåäóð. Ïåðøà áóäóº àâòîìàò,
ÿêèé ì³ñòèòü ó ñîá³ ï³äàâòîìàò, ùî çá³ãàºòüñÿ ç³ ñïåöèô³êîâàíèì àâòîìàòîì,
à äðóãà âèäàëÿº ñòàíè, ÿê³ íå íàëåæàòü öüîìó ï³äàâòîìàòó. Òàê³ ñòàíè íàçè-
âàþòüñÿ ô³êòèâíèìè. Ðîçãëÿíóòî ñïîñ³á âèçíà÷åííÿ ô³êòèâíèõ ñòàí³â. Îòðè-
ìàí³ ðåçóëüòàòè äîçâîëÿþòü â³äïîâ³äíèé ïðîöåñ çâåñòè äî çíàõîäæåííÿ òàê
çâàíèõ îñíîâíèõ öèêë³â â àâòîìàò³ ³, âðåøò³-ðåøò, äî ïåðåâ³ðêè íàëåæíîñò³
ïåð³îäè÷íîãî çâîðîòíîãî íàäñëîâà äåÿê³é ��-ðåãóëÿðí³é ìíîæèí³.
Êëþ÷îâ³ ñëîâà: �-àâòîìàò, ô³êòèâíèé ñòàí, ïî÷àòêîâèé ñèëüíî çâ’ÿçíèé
ï³äàâòîìàò, íîðìàëüíà ôîðìà, ��-ðåãóëÿðíà ìíîæèíà, îñíîâíèé öèêë.
A.N. Chebotarev
DETECTING FICTITIOUS STATES IN A �-AUTOMATON SYNTHESIZED
FROM THE SPECIFICATION IN THE LANGUAGE LP
Abstract. Synthesis of a deterministic �-automaton specified in the language LP
consists in the execution of two consecutive procedures. The first one constructs
the automaton that has a subautomaton, which is identical to the specified
automaton, and the other deletes the states that do not belong to this
subautomaton. Such states are called fictitious. The method for detecting
fictitious states is considered. The obtained results allow reducing detection of
fictitious states to finding so-called basic cycles and eventually to checking the
membership of a periodic ��-word in some ��-regular set.
Keywords: �-automaton, fictitious state, initial strongly connected subautomaton,
normal form, ��-regular set, basic cycle.
×åáîòàðåâ Àíàòîëèé Íèêîëàåâè÷,
äîêòîð òåõí. íàóê, âåäóùèé íàó÷íûé ñîòðóäíèê Èíñòèòóòà êèáåðíåòèêè èì. Â.Ì. Ãëóøêîâà ÍÀÍ
Óêðàèíû, Êèåâ, e-mail: ancheb@gmail.com.
ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2019, òîì 55, ¹ 5 57
|