Конечные автоматы в информационных технологиях
Наведено короткий огляд застосуваня теорiї скiнченних автоматiв у деяких сучасних галузях комп’ютерних наук i технологiй. Зокрема, розглядаються сфери застосування скiнченних автоматiв в комп’ютернiй алгебрi, мережах Петрi, бiологiї, верифiкацiї. A short review of applications of finite state automa...
Gespeichert in:
| Veröffentlicht in: | Кибернетика и системный анализ |
|---|---|
| Datum: | 2011 |
| 1. Verfasser: | |
| Format: | Artikel |
| Sprache: | Russian |
| Veröffentlicht: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2011
|
| Schlagworte: | |
| Online Zugang: | https://nasplib.isofts.kiev.ua/handle/123456789/84230 |
| 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: | Конечные автоматы в информационных технологиях / С.Л. Крывый // Кибернетика и системный анализ. — 2011. — Т. 47, № 5. — С. 3-20. — Бібліогр.: 36 назв. — рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
nasplib_isofts_kiev_ua-123456789-84230 |
|---|---|
| record_format |
dspace |
| spelling |
Крывый, С.Л. 2015-07-04T12:51:07Z 2015-07-04T12:51:07Z 2011 Конечные автоматы в информационных технологиях / С.Л. Крывый // Кибернетика и системный анализ. — 2011. — Т. 47, № 5. — С. 3-20. — Бібліогр.: 36 назв. — рос. 0023-1274 https://nasplib.isofts.kiev.ua/handle/123456789/84230 51.681.3 Наведено короткий огляд застосуваня теорiї скiнченних автоматiв у деяких сучасних галузях комп’ютерних наук i технологiй. Зокрема, розглядаються сфери застосування скiнченних автоматiв в комп’ютернiй алгебрi, мережах Петрi, бiологiї, верифiкацiї. A short review of applications of finite state automata in some modern areas of computer science and technologies is presented. In particular, fields of application of finite state automata in computer algebra, Petri nets, biology, and verification are considered. ru Інститут кібернетики ім. В.М. Глушкова НАН України Кибернетика и системный анализ Кибернетика Конечные автоматы в информационных технологиях Скiнченнi автомати в iнформацiйних технологiях Finite state automata in informational technologies 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 |
2011 |
| language |
Russian |
| container_title |
Кибернетика и системный анализ |
| publisher |
Інститут кібернетики ім. В.М. Глушкова НАН України |
| format |
Article |
| title_alt |
Скiнченнi автомати в iнформацiйних технологiях Finite state automata in informational technologies |
| description |
Наведено короткий огляд застосуваня теорiї скiнченних автоматiв у деяких сучасних галузях комп’ютерних наук i технологiй. Зокрема, розглядаються сфери застосування скiнченних автоматiв в комп’ютернiй алгебрi, мережах Петрi, бiологiї, верифiкацiї.
A short review of applications of finite state automata in some modern areas of computer science and technologies is presented. In particular, fields of application of finite state automata in computer algebra, Petri nets, biology, and verification are considered.
|
| issn |
0023-1274 |
| url |
https://nasplib.isofts.kiev.ua/handle/123456789/84230 |
| citation_txt |
Конечные автоматы в информационных технологиях / С.Л. Крывый // Кибернетика и системный анализ. — 2011. — Т. 47, № 5. — С. 3-20. — Бібліогр.: 36 назв. — рос. |
| work_keys_str_mv |
AT kryvyisl konečnyeavtomatyvinformacionnyhtehnologiâh AT kryvyisl skinčenniavtomativinformaciinihtehnologiâh AT kryvyisl finitestateautomataininformationaltechnologies |
| first_indexed |
2025-11-26T15:10:22Z |
| last_indexed |
2025-11-26T15:10:22Z |
| _version_ |
1850625832795504640 |
| fulltext |
Ñ.Ë. ÊÐÛÂÛÉ
ÓÄÊ 51.681.3 ÊÎÍÅ×ÍÛÅ ÀÂÒÎÌÀÒÛ
 ÈÍÔÎÐÌÀÖÈÎÍÍÛÕ ÒÅÕÍÎËÎÃÈßÕ
Êëþ÷åâûå ñëîâà: êîíå÷íûé àâòîìàò, àâòîìàò Áþõè, àâòîìàò Ìþëëåðà,
âåðèôèêàöèÿ.
ÂÂÅÄÅÍÈÅ
Òåîðèÿ àâòîìàòîâ, êàê îäèí èç ðàçäåëîâ ñîâðåìåííîé íàóêè î âû÷èñëåíèÿõ, âîç-
íèêëà áîëåå 65 ëåò íàçàä. Ê ñåðåäèíå ïðîøëîãî ñòîëåòèÿ â òåîðèè (êîíå÷íûõ)
àâòîìàòîâ áûëè ïîëó÷åíû îñíîâíûå ðåçóëüòàòû: ðàçðåøèìîñòü ïðîáëåì ýêâèâà-
ëåíòíîñòè, ñèíòåçà, àíàëèçà, ìèíèìèçàöèè, äåòåðìèíèçàöèè [1–5]. Óñòàíîâëåí
òàêæå êëàññ ÿçûêîâ, êîòîðûå äîïóñêàþòñÿ êîíå÷íûìè àâòîìàòàìè (ÊÀ) [2, 6].
ßçûêè ýòîãî êëàññà ïîëó÷èëè íàçâàíèå ðåãóëÿðíûõ ÿçûêîâ. Äëÿ íèõ óñòàíîâëåíà
ðàçðåøèìîñòü ïðîáëåì ïóñòîòû, áåñêîíå÷íîñòè, âêëþ÷åíèÿ, çàìêíóòîñòè îòíîñè-
òåëüíî òåîðåòèêî-ìíîæåñòâåííûõ îïåðàöèé è äðóãèõ ïðîáëåì [1, 7].
 íàñòîÿùåå âðåìÿ òåîðèÿ êîíå÷íûõ àâòîìàòîâ àêòèâíî èñïîëüçóåòñÿ â ñè-
ñòåìàõ îáðàáîòêè è ïîèñêà òåêñòîâîé èíôîðìàöèè [8], âåðèôèêàöèè [4, 9], ïðî-
åêòèðîâàíèè àïïàðàòóðû [10], áèîëîãèè, ãåíåòèêå [8, 11, 12] è äð. Ïîïóëÿðíîñòü
òåîðèè àâòîìàòîâ îáúÿñíÿåòñÿ òåì, ÷òî îíà èìååò õîðîøóþ àëãîðèòìè÷åñêóþ
îñíîâó â ñâÿçè ñ ðàçðåøèìîñòüþ ïåðå÷èñëåííûõ âûøå ïðîáëåì äëÿ àâòîìàòîâ è
ÿçûêîâ. Áëàãîäàðÿ ýòèì ñâîéñòâàì êîíå÷íûõ àâòîìàòîâ ïîÿâèëèñü ìíîãèå îáîá-
ùåíèÿ ýòîãî ïîíÿòèÿ: àâòîìàòû íàä áåñêîíå÷íûìè ñëîâàìè [13, 14], àâòîìàòû
íàä äåðåâüÿìè [15–17], âåðîÿòíîñòíûå è ìíîãîëåíòî÷íûå àâòîìàòû [18, 19],
âðåìåííûå àâòîìàòû [9, 20], êëåòî÷íûå àâòîìàòû [21], ãèáðèäíûå àâòîìàòû [22],
ìàãàçèííûå àâòîìàòû [4, 6] è äð.
 äàííîé ñòàòüå îïèñûâàþòñÿ íåêîòîðûå îáëàñòè ïðèìåíåíèÿ òåîðèè àâòîìà-
òîâ. Ýòè îáëàñòè ðàçëè÷íû ïî ñâîåé ïðèðîäå, ïîýòîìó èçëîæåíèå ìîæåò ïîêàçàòü-
ñÿ íåñêîëüêî ðàçíîðîäíûì, îäíàêî èìåííî ýòî, ïî ìíåíèþ àâòîðà, è îòðàæàåò ðàç-
íîîáðàçèå îáëàñòåé ïðèëîæåíèÿ òåîðèè àâòîìàòîâ. Çäåñü ðàññìàòðèâàåòñÿ ïðèìå-
íåíèå êîíå÷íûõ àâòîìàòîâ íàä ñëîâàìè êîíå÷íîé äëèíû â îáëàñòè êîìïüþòåðíîé
àëãåáðû, äèîôàíòîâûõ îãðàíè÷åíèé, âåðèôèêàöèè ñâîéñòâ ñåòåé Ïåòðè, áèîëîãèè
è â ãåíåòèêå. Êðîìå òîãî, ðàññìàòðèâàåòñÿ ïðèìåíåíèå êîíå÷íûõ àâòîìàòîâ íàä
ñëîâàìè áåñêîíå÷íîé äëèíû â îáëàñòè âåðèôèêàöèè ñâîéñòâ ðåàêòèâíûõ ñèñòåì,
êîòîðûå ñïåöèôèöèðóþòñÿ ñ ïîìîùüþ ôîðìóë òåìïîðàëüíîé ëîãèêè, à òàêæå ïðè-
ëîæåíèÿ âðåìåííûõ àâòîìàòîâ ê àíàëèçó ñâîéñòâ âðåìåííûõ ñåòåé Ïåòðè.
ÊÎÍÅ×ÍÛÅ ÀÂÒÎÌÀÒÛ ÍÀÄ ÑËÎÂÀÌÈ ÊÎÍÅ×ÍÎÉ ÄËÈÍÛ
Ïóñòü X x x xn� { }1 2, , ,� — êîíå÷íûé àëôàâèò. Ìíîæåñòâî âñåõ ñëîâ êîíå÷-
íîé äëèíû â àëôàâèòå X áóäåì îáîçíà÷àòü X * . Ïðîèçâîëüíîå ïîäìíîæåñòâî
ñëîâ L X� * íàçûâàåòñÿ ÿçûêîì â àëôàâèòå X .
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 5 3
© Ñ.Ë. Êðûâûé, 2011
Êîíå÷íûì èíèöèàëüíûì äåòåðìèíèðîâàííûì X -àâòîìàòîì íàçûâàåòñÿ ïÿ-
òåðêà � � ( , , , , )A X f a F0 , ãäå A — êîíå÷íîå ìíîæåñòâî ñîñòîÿíèé, X — êîíå÷-
íûé àëôàâèò, f A X A: � � — ôóíêöèÿ ïåðåõîäîâ, a A0 � — íà÷àëüíîå ñîñòîÿ-
íèå, F A� — ìíîæåñòâî çàêëþ÷èòåëüíûõ ñîñòîÿíèé. Àëôàâèò X íàçûâàåòñÿ
âõîäíûì àëôàâèòîì àâòîìàòà � . Ñ÷èòàåòñÿ, ÷òî åñëè f a x b( , ) � , òî àâòîìàò ïîä
äåéñòâèåì âõîäíîãî ñèìâîëà x X� ïåðåõîäèò èç ñîñòîÿíèÿ a â ñîñòîÿíèå b ,
à åñëè f a p a( , ) � � , ãäå p X� * , òî ñëîâî p ïåðåâîäèò àâòîìàò � èç ñîñòîÿíèÿ a
â ñîñòîÿíèå a� . Ñëîâî p äîïóñêàåòñÿ àâòîìàòîì � , åñëè f a p F( , )0 � . ßçûê L
äîïóñêàåòñÿ àâòîìàòîì � , åñëè âñå ñëîâà ýòîãî ÿçûêà è òîëüêî îíè äîïóñêàþòñÿ
ýòèì àâòîìàòîì. ßçûêè, äîïóñêàåìûå êîíå÷íûìè X -àâòîìàòàìè, íàçûâàþòñÿ ðå-
ãóëÿðíûìè.
1. ÊÀ â òåîðèè ñâîáîäíûõ ïîëóãðóïï è ãðóïï. Åñëè P p p pm� { , , , }1 2 � —
êîíå÷íîå ìíîæåñòâî ñëîâ èç X * , òî ñëîâà p p pm1 2, , ,� ïîðîæäàþò ïîëóãðóïïó
L X� * îòíîñèòåëüíî îïåðàöèè êîíêàòåíàöèè. Ýòî çíà÷èò, ÷òî p L� òîãäà è
òîëüêî òîãäà, êîãäà ñëîâî p ïîñòðîåíî èç ñëîâ p p pm1 2, , ,� ñ ïîìîùüþ îïåðà-
öèè êîíêàòåíàöèè. Ïîñêîëüêó ìíîæåñòâî ñëîâ L ÿâëÿåòñÿ ðåãóëÿðíûì ÿçûêîì
( { })L p p pm� � � �1 2 � , òî äëÿ íåãî ñóùåñòâóåò êîíå÷íûé X -àâòîìàò, êîòîðûé
äîïóñêàåò ñëîâà ýòîãî ÿçûêà è òîëüêî èõ. Òàêîé äåòåðìèíèðîâàííûé àâòîìàò
ëåãêî ïîñòðîèòü áåç ïðèìåíåíèÿ îáùåãî àëãîðèòìà ñèíòåçà êîíå÷íûõ àâòîìàòîâ.
Òîãäà èç òåîðèè êîíå÷íûõ àâòîìàòîâ âûòåêàåò ñëåäóþùåå óòâåðæäåíèå.
Òåîðåìà 1. Ïåðåñå÷åíèå êîíå÷íîãî ÷èñëà êîíå÷íî-ïîðîæäåííûõ ñâîáîäíûõ
ïîëóãðóïï L L Ln1 2, , ,� â àëôàâèòå X ÿâëÿåòñÿ êîíå÷íî-ïîðîæäåííîé ïîëóãðóï-
ïîé. Ñóùåñòâóåò àëãîðèòì ïîñòðîåíèÿ ìíîæåñòâà îáðàçóþùèõ ïîëóãðóïïû
L L L Ln� 1 2 � ïî ñèñòåìàì îáðàçóþùèõ ïîëóãðóïï L L Ln1 2, , ,� .
Íà ýòîì ñâîéñòâå êîíå÷íî-ïîðîæäåííûõ ïîëóãðóïï áàçèðóþòñÿ ñïîñîáû
èäåíòèôèêàöèè ñëîâ è ïðåäñòàâëåíèÿ ñëîâàðåé åñòåñòâåííûõ ÿçûêîâ [8].
Àíàëîãè÷íûå ðåçóëüòàòû èìåþò ìåñòî è äëÿ ñâîáîäíûõ êîíå÷íî-ïîðîæäåí-
íûõ ãðóïï [23]. Ïðè ýòîì âíà÷àëå ïî ñèñòåìå îáðàçóþùèõ ñòðîèòñÿ íèëüñåíîâ-
ñêèé áàçèñ [24], à çàòåì íà îñíîâàíèè ýòîãî áàçèñà ñòðîèòñÿ êîíå÷íûé äåòåðìè-
íèðîâàííûé X -àâòîìàò, äîïóñêàþùèé ñëîâà ïîäãðóïïû, ïîðîæäåííîé òàêèì
áàçèñîì. Èìååò ìåñòî ñëåäóþùàÿ òåîðåìà.
Òåîðåìà 2. Ïåðåñå÷åíèå êîíå÷íîãî ÷èñëà êîíå÷íî-ïîðîæäåííûõ ñâîáîäíûõ
ãðóïï L L Ln1 2, , ,� â àëôàâèòå X ÿâëÿåòñÿ êîíå÷íî-ïîðîæäåííîé ãðóïïîé. Ñóùå-
ñòâóåò àëãîðèòì ïîñòðîåíèÿ ìíîæåñòâà îáðàçóþùèõ ãðóïïû L L L Ln� 1 2 � ïî
íèëüñåíîâñêèì áàçèñàì ãðóïï L L Ln1 2, , ,� .
2. ÊÀ è ëèíåéíûå äèîôàíòîâûå óðàâíåíèÿ. Îäíèì èç íàèáîëåå ýôôåêòèâ-
íûõ àëãîðèòìîâ ðåøåíèÿ ëèíåéíîãî îäíîðîäíîãî äèîôàíòîâîãî óðàâíå-
íèÿ (ËÎÄÓ)
a x a x a xq q1 1 2 2 0
�� (1)
ÿâëÿåòñÿ àëãîðèòì Ôîðòåíáàõåðà [25]. Ýòîò àëãîðèòì ñòðîèò áàçèñ ìíîæåñòâà
âñåõ ðåøåíèé ËÎÄÓ, êîòîðûé ñîñòîèò èç ìèíèìàëüíûõ ðåøåíèé îòíîñèòåëüíî
ïîðÿäêà x x x x y y y y x yq q i i� � � � �( , , , ) ( , , , )1 2 1 2� � äëÿ âñåõ i q�1 2, , ,� .
Ñóòü àëãîðèòìà Ôîðòåíáàõåðà ñîñòîèò â òîì, ÷òîáû èñêàòü ìèíèìàëüíûå áà-
çèñíûå ðåøåíèÿ ËÎÄÓ (1), íà÷èíàÿ ñ êàíîíè÷åñêèõ âåêòîðîâ N q , ò.å. ñ âåê-
òîðîâ e e1 21 0 0 0 1 0� �( , , , ), ( , , , )� � , ..., eq � ( , , , )0 0 1� . Ïðè ýòîì åñëè íåêîòî-
ðûé òåêóùèé âåêòîð x x xq� ( , , )1 � åùå íå ÿâëÿåòñÿ ðåøåíèåì (1), òî:
— ïðè a x a xq q1 1 0
� óâåëè÷èòü íà åäèíèöó íåêîòîðîå x j òàêîå, ÷òî
a j � 0;
4 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 5
— ïðè a x a xq q1 1 0
�� óâåëè÷èòü íà åäèíèöó íåêîòîðîå x j òàêîå, ÷òî
a j
0 . (Çàìåòèì, ÷òî åñëè âñå ai � 0 èëè âñå ai
0, òî óðàâíåíèå (1) èìååò ëèøü
òðèâèàëüíîå ðåøåíèå x0 0 0� ( , , )� .)
Ñêàçàííîå ìîæíî âûðàçèòü ôîðìàëüíî òàêèì óñëîâèåì (óñëîâèå Ôîðòåíáà-
õåðà): óâåëè÷èâàòü íà åäèíèöó òàêîå x j , äëÿ êîòîðîãî a x a e j( ) ( )�
0 , ãäå
x x xq� ( , , )1 � , a e aj j( ) � , à e j — âåêòîð êàíîíè÷åñêîãî áàçèñà.
Ïðèìåð 1. Íàéòè áàçèñ ìíîæåñòâà ðåøåíèé ËÎÄÓ �
� �x x x x1 2 3 42 3 0 .
Cõåìà âñåãî ïðîöåññà ðåøåíèÿ ïîêàçàíà íà ðèñ. 1. Íà âåêòîðàõ êàíîíè÷åñêî-
ãî áàçèñà óðàâíåíèå èìååò çíà÷åíèÿ � �1 1 2 3, , , (îòðàæàåò âåðõíèé ðÿä ñõåìû).
 ðåçóëüòàòå ïîëó÷àåì òàêèå áàçèñíûå âåêòîðû:
v1 � (0, 0, 3, 2) , v2 � (0, 1, 1, 1) , v3 � (0, 3, 0, 1) ,
v4 � (1, 0, 2, 1) , v5 � (2, 0, 1, 0), v6 � (1, 1, 0, 0) .
Ìåòîä Ôîðòåíáàõåðà ìîæíî ïåðåôîðìóëèðîâàòü è îáîñíîâàòü ñ ïîìîùüþ
÷àñòè÷íûõ êîíå÷íûõ X -àâòîìàòîâ. Ñóùåñòâîâàíèå è âîçìîæíîñòü ïîñòðîåíèÿ
ñîîòâåòñòâóþùåãî ÊÀ âûòåêàåò èç óñëîâèÿ Ôîðòåíáàõåðà: ñóììà ÷èñåë a x( ) è
a ei( ) , óäîâëåòâîðÿþùèõ ýòîìó óñëîâèþ, âñåãäà ñòðîãî ìåíüøå ïî àáñîëþòíîé
âåëè÷èíå àáñîëþòíûõ âåëè÷èí ñëàãàåìûõ. Ýòî çíà÷èò, ÷òî àëãîðèòì Ôîðòåíáà-
õåðà ïîðîæäàåò ïðîöåññ, êîòîðûé ÷åðåç êîíå÷íîå ÷èñëî øàãîâ äîëæåí
çàìêíóòüñÿ. Ôîðìàëüíîå èçëîæåíèå ýòîãî ïîäõîäà èìååò ñëåäóþùèé âèä.
Ïóñòü a x a x a x a xq q( ) �
�1 1 2 2 0� ÿâëÿåòñÿ ËÎÄÓ. Âõîäíûì àëôàâèòîì
èñêîìîãî àâòîìàòà åñòü ìíîæåñòâî X e e eq� { , , , }1 2 � âåêòîðîâ êàíîíè÷åñêîãî
áàçèñà. Ìíîæåñòâî ñîñòîÿíèé Q àâòîìàòà âíà÷àëå âêëþ÷àåò åäèíñòâåííîå ñîñòî-
ÿíèå 0, à îñòàëüíûå ýëåìåíòû ýòîãî ìíîæåñòâà ïîðîæäàþòñÿ â ïðîöåññå ïîñòðîå-
íèÿ X -àâòîìàòà � � ( , , , { },{ })Q X f 0 0 ñëåäóþùèì îáðàçîì:
f m e
a m
m a e m a ei
i
i i( , )
, ,
( ), ( ) ,
*,
�
�
�
åñëè
åñëè
åñëè íå î
0
0
ïðåäåëåíî,
�
�
�
�
�
ãäå m Z� — ìíîæåñòâî öåëûõ ÷èñåë, e X i qi � �, , , ,1 2 � , à ñèìâîë * îçíà÷àåò
íåîïðåäåëåííîñòü.
Ïîñëå çàìûêàíèÿ ïðîöåññà ãåíåðàöèè ñîñòîÿíèé àâòîìàòà � ñòðîèòñÿ áàçèñ
ìíîæåñòâà ðåøåíèé óðàâíåíèÿ a x( ) � 0 . Äëÿ ýòîãî íåîáõîäèìî íàéòè âñå ñëîâà p
â àëôàâèòå X , ñîîòâåòñòâóþùèå âñåì ïðîñòûì öèêëè÷åñêèì ïóòÿì èç ñîñòîÿ-
íèÿ 0 â ñîñòîÿíèå 0 , ïîñòðîèòü âåêòîðû-ðåøåíèÿ, ñîîòâåòñòâóþùèå ýòèì ñëî-
âàì, è óäàëèòü ïîâòîðÿþùèåñÿ è íåìèíèìàëüíûå âåêòîðû (ñì. ðèñ. 1).
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 5 5
Ðèñ. 1. Ñõåìà ïðîöåññà ðåøåíèÿ ËÎÄÓ
Èç ñâîéñòâ êîíå÷íûõ àâòîìàòîâ è äîïóñêàåìûõ èìè ÿçûêîâ ñëåäóþò òàêèå
óòâåðæäåíèÿ.
Òåîðåìà 3. Ìíîæåñòâî âñåõ ðåøåíèé óðàâíåíèÿ a x( ) � 0 ÿâëÿåòñÿ ðåãóëÿð-
íûì ìíîæåñòâîì. Áàçèñ ìíîæåñòâà ðåøåíèé ýòîãî óðàâíåíèÿ ñîñòîèò èç âñåõ
ñëîâ â àëôàâèòå X , ñîîòâåòñòâóþùèõ âñåì ðàçëè÷íûì ïðîñòûì öèêëè÷åñêèì ïó-
òÿì èç íà÷àëüíîãî ñîñòîÿíèÿ 0 â ñîñòîÿíèå 0 àâòîìàòà � , ïðåäñòàâëÿþùåãî ìíî-
æåñòâî ðåøåíèé äàííîãî óðàâíåíèÿ [26].
Ñëåäñòâèå 1. Àëãîðèòì ïîñòðîåíèÿ àâòîìàòà � çàâåðøàåò ñâîþ ðàáîòó ïî-
ñëå êîíå÷íîãî ÷èñëà øàãîâ. ×èñëî ñîñòîÿíèé àâòîìàòà � , ïîðîæäàåìûõ â ïðî-
öåññå åãî ïîñòðîåíèÿ ìåòîäîì Ôîðòåíáàõåðà, îãðàíè÷åíî âåëè÷èíîé | |ai
i
q
�
�
1
1 .
Ïðèìåð 2 (ïðîäîëæåíèå ïðèìåðà 1). Ðàññìîòðèì ËÎÄÓ a x x x( ) � �
1 2
� �2 3 03 4x x èç ïðèìåðà 1. Àâòîìàò, ïðåäñòàâëÿþùèé âñå ðåøåíèÿ äàííîãî
óðàâíåíèÿ, ïîðîæäàåòñÿ ñëåäóþùèì îáðàçîì. Íà÷àëüíîå çíà÷åíèå ìíîæåñòâà
Q � 0 . Ñîñòîÿíèå 0 ÿâëÿåòñÿ íà÷àëüíûì è çàêëþ÷èòåëüíûì ñîñòîÿíèåì àâòîìàòà.
Ãåíåðèðóåì íîâûå ñîñòîÿíèÿ:
f e f e f e f e( , ) , ( , ) , ( , ) , ( , ) .0 1 0 1 0 2 0 31 2 3 4� � � � � �
Ñëåäîâàòåëüíî, ìíîæåñòâî Q � � �{ , , , , }0 1 2 1 3 . Âíîâü ïîëó÷åííûå ñîñòîÿíèÿ, â
ñâîþ î÷åðåäü, ïîðîæäàþò òàêèå ñîñòîÿíèÿ:
f e f e f e f e( , ) , ( , ) , ( , ) , ( , ) ,1 0 1 0 1 1 2 11 2 3 1� � � � � �
f e f e f e f e( , ) , ( , ) , ( , ) , ( , ) .1 2 2 1 3 2 3 14 4 2 3� � � � � � � � � �
Íîâûì åñòü ñîñòîÿíèå �2, êîòîðîå ïîðîæäàåò ñîñòîÿíèÿ f e( , ) ,� � �2 12
f e( , )� �2 03 . Ïîñêîëüêó ýòè ñîñòîÿíèÿ ïðèíàäëåæàò ìíîæåñòâó Q , òî ýòî
çíà÷èò, ÷òî ïðîöåññ ïîðîæäåíèÿ ñîñòîÿíèé çàìêíóëñÿ. Ñëåäîâàòåëüíî, ïîëó÷à-
åì àâòîìàò, òàáëèöà ïåðåõîäîâ êîòîðîãî èìååò âèä
f 0 �1 �2 1 2 �3
e1 �1 * * 0 1 *
e2 1 0 �1 * * �2
e3 2 1 0 * * �1
e4 �3 * * �2 �1 *
Àâòîìàòíûé ïîäõîä îáîáùàåòñÿ è íà ñëó÷àé íåîäíîðîäíûõ ËÄÓ, è íà ñëó-
÷àé ñèñòåì ËÄÓ [25, 26].
3. ÊÀ è ñåòè Ïåòðè. Ïðèìåíåíèå ÊÀ ê àíàëèçó ñâîéñòâ ñåòåé Ïåòðè (ÑÏ)
ïîÿñíèì íà ïðèìåðå. Ïóñòü èìååòñÿ ÑÏ, êîòîðàÿ ìîäåëèðóåò ðàáîòó íàñîñà,
ïåðåêà÷èâàþùåãî æèäêîñòü èç îäíîé åìêîñòè p1 â äðóãóþ åìêîñòü p3
(ðèñ. 2). Ìåñòî p2 ñîîòâåòñòâóåò ðàáî÷åìó ñîñòîÿíèþ íàñîñà, à p4 — íåðàáî÷å-
ìó ñîñòîÿíèþ íàñîñà.
Íàèáîëåå èçâåñòíûì è ïðàê-
òè÷íûì ìåòîäîì àíàëèçà ñâîéñòâ
ÑÏ ÿâëÿåòñÿ óðàâíåíèå ñîñòîÿíèÿ,
ïðåäñòàâëÿåìîå ñèñòåìîé ëèíåé-
íûõ îäíîðîäíûõ äèîôàíòîâûõ
óðàâíåíèé (ÑËÎÄÓ), ðåøåíèÿ êî-
òîðîé íàõîäÿòñÿ âî ìíîæåñòâå íà-
òóðàëüíûõ ÷èñåë N . Ýòà ñèñòåìà
èìååò âèä A x� � 0 , ãäå A — ìàòðè-
öà èíöèäåíòíîñòè ÑÏ. Ñòðîêè ìàò-
ðèöû ñîîòâåòñòâóþò ìåñòàì ÑÏ,
6 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 5
Ðèñ. 2. Ñåòü Ïåòðè
à ñòîëáöû — ïåðåõîäàì. Åñëè â i-ì ñòîëáöå ýòîé ìàòðèöû ýëåìåíòû èìåþò ïîëî-
æèòåëüíûå çíàêè è ïðèíàäëåæàò ðàçíûì ñòðîêàì, òî ýòî çíà÷èò, ÷òî ïðè ñðàáà-
òûâàíèè i-ãî ïåðåõîäà â ýòè ìåñòà áóäåò ïîëîæåíî ñîîòâåòñòâóþùåå êîëè÷åñòâî
ôèøåê. Åñëè ýëåìåíòû èìåþò îòðèöàòåëüíûå çíà÷åíèÿ, òî îïðåäåëåííîå êîëè-
÷åñòâî ôèøåê çàáèðàåòñÿ èç ñîîòâåòñòâóþùåãî ìåñòà ïðè ñðàáàòûâàíèè i-ãî ïå-
ðåõîäà. Êîëè÷åñòâî ôèøåê, êîòîðîå èìååòñÿ â ìåñòå pi , îáîçíà÷èì M pi( ) .
 äàííîì ïðèìåðå íà÷àëüíîé ðàçìåòêîé ÑÏ ÿâëÿåòñÿ M 0 2 1 0 0� ( , , , ) , à åå ìàòðè-
öà èíöèäåíòíîñòè èìååò âèä
A �
�
�
�
�
�
�
�
�
�
��
�
�
�
�
�
��
1 1 0 0
0 0 1 1
1 1 0 0
0 0 1 1
.
Äåéñòâèòåëüíî, ïåðåõîä t1 ïðè ñðàáàòûâàíèè çàáèðàåò ôèøêó èç ìåñò p1 è p2
è ïîìåùàåò ïî îäíîé ôèøêå â ìåñòà p2 (âîçâðàùàåò ôèøêó â òî æå ìåñòî) è p3 .
Ïîýòîìó â ïåðâîì ñòîëáöå ïåðâûé ýëåìåíò ìàòðèöû îòðèöàòåëüíûé (�1), à òðå-
òèé ýëåìåíò ïîëîæèòåëüíûé (
1). Îñòàëüíûå ýëåìåíòû ðàâíû íóëþ (âòîðîé ýëå-
ìåíò ðàâåí íóëþ, ïîñêîëüêó ôèøêà çàáèðàåòñÿ èç ìåñòà p2 è òóäà âîçâðàùàåòñÿ).
Ðåøåíèÿ ÑËÎÄÓ A x� � 0 íàçûâàþòñÿ T-èíâàðèàíòàìè, à ðåøåíèÿ ÑËÎÄÓ
A yT � � 0 — S-èíâàðèàíòàìè.
T-èíâàðèàíòû ÑÏ ñîñòàâëÿþò ìèíèìàëüíîå ïîðîæäàþùåå ìíîæåñòâî ðåøå-
íèé ÑËÎÄÓ A x� � 0 . Â äàííîì ïðèìåðå òàêèìè ðåøåíèÿìè åñòü âåêòîðû
x x1 21 1 0 0 0 0 1 1� �( , , , ), ( , , , ),
ñîîòâåòñòâóþùèå äâóì ïîñëåäîâàòåëüíîñòÿì ñðàáàòûâàíèé ïåðåõîäîâ: t t1 2 è
t t3 4 . Ýòè èíâàðèàíòû ñâèäåòåëüñòâóþò î òîì, ÷òî ÑÏ íå èìååò ìåðòâûõ ïåðå-
õîäîâ, êîòîðûå íèêîãäà íå ñðàáàòûâàþò â ïðîöåññå ôóíêöèîíèðîâàíèÿ ÑÏ.
S-èíâàðèàíòû ÑÏ ñîñòàâëÿþò ìèíèìàëüíîå ïîðîæäàþùåå ìíîæåñòâî ðåøå-
íèé ÑËÎÄÓ A yT � � 0 .  äàííîì ñëó÷àå òàêèìè ðåøåíèÿìè åñòü âåêòîðû
y y1 21 0 1 0 0 1 0 1� �( , , , ), ( , , , ),
÷òî ñâèäåòåëüñòâóåò îá îãðàíè÷åííîñòè ìåñò p p p p1 2 3 4, , , è ñîîòâåòñòâåííî
îãðàíè÷åííîñòè ÑÏ.
Åñëè â ïðîöåññå àíàëèçà ñâîéñòâ ÑÏ íåîáõîäèìî íàéòè ïîñëåäîâàòåëü-
íîñòü ñðàáàòûâàíèé åå ïåðåõîäîâ, êîòîðàÿ ïðèâîäèò ê îïðåäåëåííîìó ìåñòó
èëè îïèñûâàåò íåêîòîðîå ñîáûòèå â ÑÏ, òî ïî èíâàðèàíòàì ÑÏ ýòî ñäåëàòü
ïðàêòè÷åñêè íåâîçìîæíî. Îòìåòèì, ÷òî èíâàðèàíòû óêàçûâàþò òîëüêî íà ïå-
ðåõîä, êîòîðûé ñðàáîòàë, íî íå óêàçûâàþò ïîñëåäîâàòåëüíîñòè èõ ñðàáàòûâà-
íèÿ. Äëÿ ýòîé öåëè ñëóæèò òðàíçèöèîííàÿ ñèñòåìà, êîòîðàÿ ÿâëÿåòñÿ ãðàôîì
äîñòèæèìûõ ðàçìåòîê ÑÏ. Åñëè ÑÏ îãðàíè÷åíà, òî ãðàô äîñòèæèìûõ ðàçìå-
òîê ýòîé ÑÏ áóäåò êîíå÷íûì àâòîìàòîì. Ãðàô G ïåðåõîäîâ òàêîãî àâòîìàòà
ïîêàçàí íà ðèñ. 3.
Ïî ýòîìó àâòîìàòó ñ ïîìîùüþ àëãîðèòìà àíàëèçà êîíå÷íîãî X -àâòîìàòà
ìîæíî íàéòè ìíîæåñòâî ïîñëåäîâàòåëüíîñòåé ñðàáàòûâàíèÿ ïåðåõîäîâ, à òàêæå
àíàëèçèðîâàòü ìíîãèå ñòàòè÷åñêèå, äèíàìè÷åñêèå è ëîãè÷åñêèå ñâîéñòâà ÑÏ.
Îñíîâíûìè èç íèõ ÿâëÿþòñÿ ñâîéñòâà âçàèìíîãî èñêëþ÷åíèÿ (mutex), ñïðàâåäëè-
âîñòè ( fairness) è æèâó÷åñòè (liveness).
Ñîãëàñíî ñâîéñòâó mutex äëÿ äàííîé ÑÏ â ìåñòàõ p2 è p4 íå ìîãóò ôèøêè
íàõîäèòüñÿ îäíîâðåìåííî (ò.å. íàñîñ íå ìîæåò íàõîäèòüñÿ îäíîâðåìåííî â ðàáî-
÷åì è íåðàáî÷åì ñîñòîÿíèè). Ýòî ñâîéñòâî ñëåäóåò èç òîãî, ÷òî â àâòîìàòå âñå
äîñòèæèìûå ðàçìåòêè óäîâëåòâîðÿþò ðàâåíñòâó M p M p( ) ( )2 4 1
� .
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 5 7
Íà îñíîâàíèè ñâîéñòâà fairness äëÿ äàííîé ÑÏ â ìåñòå p4 â êàêîé-òî ìîìåíò
áóäåò íàõîäèòüñÿ ôèøêà. Ñîäåðæàòåëüíî ýòî ñâîéñòâî îçíà÷àåò, ÷òî íàñîñ íå áó-
äåò ðàáîòàòü ïîñòîÿííî, åñëè íàëè÷èå èëè îòñóòñòâèå ôèøåê â ìåñòàõ p2 è p4
èíòåðïðåòèðîâàòü êàê âêëþ÷åíèå èëè îòêëþ÷åíèå ðàáîòû íàñîñà, ïåðåêà÷èâàþ-
ùåãî æèäêîñòü èç ïåðâîé åìêîñòè âî âòîðóþ (èç ãðàôà G âèäíî, ÷òî ôîðìóëà
M p( )4 1� âûïîëíÿåòñÿ â âåðøèíàõ v v3 4, è v5).
Ñâîéñòâî liveness äëÿ äàííîé ÑÏ ñîñòîèò â òîì, ÷òî â íåé ïðè ëþáîé ðàçìåòêå
âñåãäà âîçìîæåí õîòÿ áû îäèí ïåðåõîä. Ýòî îçíà÷àåò, ÷òî â ÑÏ íåò ðàçìåòêè, ïðè
êîòîðîé íåâîçìîæåí íè îäèí ïåðåõîä. Ñîäåðæàòåëüíî ñâîéñòâî îçíà÷àåò, ÷òî ðàáîòà
ñèñòåìû ìîæåò ïðîäîëæàòüñÿ ïîòåíöèàëüíî áåñêîíå÷íî ïðè óñëîâèè, ÷òî âñå êîí-
òðîëèðóþùèå ïðèáîðû áóäóò ðàáîòàòü ïðàâèëüíî. Ýòî ñâîéñòâî âûïîëíÿåòñÿ äëÿ
äàííîé ÑÏ, ïîñêîëüêó èç êàæäîãî ñîñòîÿíèÿ â àâòîìàòå G èìåþòñÿ ïåðåõîäû.
4. ÊÀ â áèîëîãèè. Êîíå÷íûå àâòîìàòû â íàñòîÿùåå âðåìÿ óñïåøíî ïðèìåíÿþò-
ñÿ â áèîëîãèè. Ñîçäàþòñÿ íîâûå êëåòêè è ðàñïîçíàþòñÿ ñâîéñòâà ñóùåñòâóþùèõ æè-
âûõ êëåòîê, â ÷àñòíîñòè ðàñïîçíàþòñÿ ñâîéñòâà ÄÍÊ. Ýòè ïðèìåíåíèÿ ñâÿçàíû ñî
ñïåöèàëüíûìè ÿçûêàìè, êîòîðûå äîïóñêàþòñÿ êîíå÷íûìè àâòîìàòàìè [12].
Êîíñòðóèðîâàíèå òàêèõ ÿçûêîâ ñâÿçàíî ñ ïîëó÷åíèåì íîâûõ ñëîâ èç èìåþ-
ùèõñÿ. Íåôîðìàëüíî ýòî âûïîëíÿåòñÿ ñëåäóþùèì îáðàçîì. Äàíà óïîðÿäî÷åííàÿ
ïàðà ñëîâ â àëôàâèòå a b c d, , , , íàïðèìåð
u ddddccaabbddd� è v dddccaabbdddd� .
Ïî ýòîé ïàðå ñëîâ ìîæíî ïîñòðîèòü íîâîå ñëîâî ïóòåì ïðèìåíåíèÿ îïåðà-
öèè ñå÷åíèÿ êàæäîãî èç íèõ, íàïðèìåð ìåæäó äâóìÿ âõîæäåíèÿìè ñèìâîëà a
â ïîäïîñëåäîâàòåëüíîñòè s ccaabb� , êîòîðàÿ âõîäèò êàê â u, òàê è â v. Ïîñ-
ëå îïåðàöèè ñå÷åíèÿ ïðèìåíÿåòñÿ îïåðàöèÿ ñêëåèâàíèÿ ëåâîé ÷àñòè ïåðâî-
ãî ñëîâà è ïðàâîé ÷àñòè âòîðîãî ñëîâà. Ïåðâàÿ îïåðàöèÿ, áóäó÷è ïðèìåíÿå-
ìîé ê ñëîâàì u è v, ãåíåðèðóåò ÷àñòè ddddcca abbddd, è dddcca abbdddd, .
Ïðèìåíÿÿ îïåðàöèþ ñêëåèâàíèÿ ê ïîëó÷åííûì ÷àñòÿì, íàõîäèì ñëîâî
x ddddccaabbdddd� . Çàìåòèì, ÷òî, âûïîëíÿÿ ýòè îïåðàöèè íà óïîðÿäî÷åííîé
ïàðå v u, , ïîëó÷àåì ñëîâî y dddccaabbddd� .  ýòîì ñëó÷àå ãîâîðÿò, ÷òî ñëî-
âà x è y ïîëó÷åíû â ðåçóëüòàòå ïðèìåíåíèÿ îïåðàöèè ñðàùèâàíèÿ ïàð ñëîâ
u v, è v u, ñîîòâåòñòâåííî.
8 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 5
Ðèñ. 3. Ãðàô (àâòîìàò) G äîñòèæèìûõ ðàçìåòîê ÑÏ
Ñðàùèâàíèå ñëîâ ïðîèñõîäèò íå ïðîèçâîëüíûì ñïîñîáîì, à â ñîîòâåòñòâèè
ñ îïðåäåëåííûìè ïðàâèëàìè, êîòîðûå çàäàþòñÿ èçíà÷àëüíî.
4.1. Ïðàâèëà ñðàùèâàíèÿ, ñõåìû, ñèñòåìû è ÿçûêè. Ðàññìîòðèì ôîð-
ìàëüíûå îïðåäåëåíèÿ ââåäåííûõ âûøå ïîíÿòèé. Ïóñòü X x x xn� { , , , }1 2 � — êî-
íå÷íûé àëôàâèò, X * — ìíîæåñòâî âñåõ ñëîâ êîíå÷íîé äëèíû â àëôàâèòå X .
Ïðàâèëîì ñðàùèâàíèÿ íàçûâàåòñÿ ÷åòâåðêà r u u v v X� � � �( , , , ) ( )* 4 . Äåé-
ñòâèå ïðàâèëà r íà ñëîâàõ ÿçûêà îïðåäåëÿåò ÿçûê r L xuvy X L( ) { |*� � ñîäåðæèò
ñëîâà xuu q� è pv vy� äëÿ íåêîòîðûõ x p q y X, , , *� }. Äëÿ ìíîæåñòâà ïðàâèë ñðà-
ùèâàíèÿ R ïîëó÷àåì ÿçûê R L r L
r R
( ) ( )�
�
� . Ïðàâèëî r îòíîñèòñÿ ê ÿçûêó L , åñëè
ÿçûê r L( ) ñîäåðæèòñÿ â L . Ìíîæåñòâî ïðàâèë R îòíîñèòñÿ ê ÿçûêó L , åñëè R L( )
ñîäåðæèòñÿ â L . Ðàäèóñîì k ïðàâèëà ñðàùèâàíèÿ r u u v v� � �( , , , ) íàçûâàåòñÿ ìàê-
ñèìóì äëèí ñëîâ u u v v, , ,� � .
Îïðåäåëåíèå 1. Ñõåìîé ñðàùèâàíèÿ íàçûâàåòñÿ ïàðà � � ( , )X R , ãäå X —
êîíå÷íûé àëôàâèò, R — êîíå÷íîå ìíîæåñòâî ïðàâèë ñðàùèâàíèÿ. Äëÿ êàæäîãî
ÿçûêà L X� * è íàòóðàëüíîãî ÷èñëà n îïðåäåëÿåòñÿ � n L( ) :
� 0 ( )L L� ; � � �k k kL L R L
� �1 ( ) ( ) ( ( )) .
Òðàíçèòèâíîå çàìûêàíèå ïîñëåäîâàòåëüíîñòè � � �0 1 2( ), ( ), ( )L L L , ...
..., ( ),� k L � îïðåäåëÿåò ÿçûê � �* ( ) ( )L Ln
n
�
�0
� .
Ñèñòåìîé ñðàùèâàíèÿ íàçûâàåòñÿ ïàðà ( , )� I , ãäå � — ñõåìà ñðàùèâàíèÿ,
I — êîíå÷íûé íà÷àëüíûé ÿçûê, ñîäåðæàùèéñÿ â X * . ßçûêîì, ïîðîæäåííûì
ñèñòåìîé ( , )� I , íàçûâàåòñÿ ÿçûê L I I( , ) ( )*� �� .
ßçûê L íàçûâàåòñÿ ÿçûêîì-ñðàùèâàíèåì, åñëè L L I� ( , )� äëÿ íåêîòîðîé ñèñ-
òåìû ñðàùèâàíèÿ ( , )� I .
Ïðèìåð 3. Ïóñòü X a b c d� { , , , } , r u u v v� � �( , , , ) , ãäå ñëîâà u u v v X, , , *� � �
ïðàâèëà r òàêèå, ÷òî u v cca� � � è u v abb� � � . Ïóñòü R r� { } , òîãäà ñõåìà ñðàùè-
âàíèÿ èìååò âèä
� � �( , ) ({ , , , }, { , , , })X R a b c d cca abb cca abb .
Ïóñòü I ddddccaabbddd dddccaabbdddd� { , } . Ïðèìåíèì ïðàâèëî r ê óïî-
ðÿäî÷åííîé ïàðå ñëîâ ( , )ddddccaabbddd dddccaabbdddd . Ýòî ïðàâèëî ïî-
ðîæäàåò ñëîâî dddccaabbdddd, à ñ ïðèìåíåíèåì ïðàâèëà r ê ïàðå
( , )dddccaabbdddd ddddccaabbddd ïîëó÷àåì ñëîâî dddccaabbddd.
Êîãäà r äåéñòâóåò íà ìíîæåñòâå I I� , íàïðèìåð íà ïàðå ( ,ddddccaabbddd
dddccaabbdddd), òî ðåçóëüòàòîì áóäåò ñëîâî ddddccaabbddd, êîòîðîå ÿâëÿåòñÿ
êîîðäèíàòîé îäíîé èç ïàð. Îòñþäà ïîëó÷àåì
� 0 ( ) { , })I I ddddccaabbddd dddccaabbdddd� �
è
� � �1 0 0( ) ( ) ( ( ))I I R I� � �
� �I ddddccaabbdddd dddccaabbddd ddddccaabbddd dddc{ , , , caabbdddd} �
� { , , ,ddddccaabbdddd dddccaabbddd ddddccaabbddd dddccaabbdddd} .
Çàìåòèì, ÷òî R îòíîñèòñÿ ê ÿçûêó �1 ( )I è, çíà÷èò, � �2 1( ) ( )I I� . Òîãäà
� � �1 2 3( ) ( ) ( )I I I� � è � �* ( ) ( )I I� 1 .
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 5 9
Îòñþäà ñëåäóåò, ÷òî L I( , )� — êîíå÷íûé ÿçûê.
Ïðèìåð 4. Ïóñòü X a b c d� { , , , } , r b bbbcc b bbbcc� ( , , , ) , R r� { } , I �
� { }a bbbbcca bbbbcca6 6 6 .
Ïðàâèëî r , ïðèìåíÿåìîå â ïàðå
( , )a bbbbcca bbbbcca a bbbbcca bbbbcca6 6 6 6 6 6
ê ñàìîìó ïðàâîìó âõîæäåíèþ ñëîâà bbbcc ïðàâîé êîîðäèíàòû, ïîðîæäàåò ñëî-
âî a bbbbcca bbbbcca bbbbcca6 6 6 6 äëèíû 42.
Ïðàâèëî r ìîæíî ïðèìåíÿòü è ê ëåâîìó âõîæäåíèþ ñëîâà bbbbcc â ïåðâîé
êîîðäèíàòå, è ê ïðàâîìó âõîæäåíèþ ýòîãî ñëîâà âî âòîðîé êîîðäèíàòå. Ýòî ïî-
ðîæäàåò ñëîâî a bbbbcca6 6 äëèíû 18. Ñëåäîâàòåëüíî,
�1 6 6 6 6 6 6 6( ) { , ,I a bbbbcca a bbbbcca bbbbcca a bbbbcca bbb� bcca bbbbbcca6 6 }.
Ïðîäîëæàÿ âû÷èñëåíèÿ ïîäîáíûì îáðàçîì, ïîëó÷àåì áåñêîíå÷íûé ÿçûê
L I a bbbbcca bbbbcca( , ) { }� � 6 6 6 .
Ñèìâîëû ñëîâ âèäà a bbbbcca bbbbcca6 6 6 â ãåíåòèêå èíòåðïðåòèðóþòñÿ êàê
ìîäåëü ìîëåêóëû ÄÍÊ. Ïðàâèëî r ïðåäñòàâëÿåò îïåðàöèè ñå÷åíèÿ è ñêëåèâàíèÿ
íà íåêîòîðîé ñóáñòàíöèè â ñîåäèíåíèè åå ñ äðóãîé ñóáñòàíöèåé. Â ýòîì ïîíèìà-
íèè ÿçûê L I a bbbbbcca bbbbcca( , ) { }� � 6 6 6 , ïîëó÷åííûé â ïðèìåðå 4, ÿâëÿåòñÿ
ìîäåëüþ ìíîæåñòâà ÄÍÊ ìîëåêóë, êîòîðûå ïîòåíöèàëüíî ìîãóò ïîÿâëÿòüñÿ ïðè
ïðîâåðêå íà ñîäåðæàíèå íåêîòîðîãî âåùåñòâà ÄÍÊ ìîëåêóëû âèäà
a bbbbcca bbbbbcca6 6 6 èëè ìîëåêóëû äðóãîãî âåùåñòâà.
ßçûêè ñðàùèâàíèÿ áûëè ââåäåíû â 1987 ã. â ðàáîòå [27], à ïîçæå â ðàáî-
òàõ [28, 29] áûëî ïîêàçàíî, ÷òî ÿçûêè ñðàùèâàíèÿ ÿâëÿþòñÿ ðåãóëÿðíûìè ÿçûêà-
ìè, ïîñêîëüêó èìååò ìåñòî ñëåäóþùàÿ òåîðåìà.
Òåîðåìà 4. Êàæäûé ÿçûê ñðàùèâàíèÿ ÿâëÿåòñÿ ðåãóëÿðíûì ÿçûêîì [28, 29].
 ðàáîòå [30] ïîêàçàíî, ÷òî íå âñå ðåãóëÿðíûå ÿçûêè ÿâëÿþòñÿ ÿçûêàìè ñðà-
ùèâàíèÿ. Â [27] áûëî äîêàçàíî, ÷òî ÿçûê L ÿâëÿåòñÿ ÿçûêîì ñðàùèâàíèÿ, åñëè ñó-
ùåñòâóåò íàòóðàëüíîå ÷èñëî n òàêîå, ÷òî ñëîâî uxq ïðèíàäëåæèò L , êàê òîëüêî x
èìååò äëèíó n è îáà ñëîâà uxv è pxq ïðèíàäëåæàò ÿçûêó L .
Âîçíèêàåò âîïðîñ: åñëè äàí ðåãóëÿðíûé ÿçûê L , òî ñóùåñòâóåò ëè ñèñòåìà
ñðàùèâàíèÿ, êîòîðàÿ ïîðîæäàåò ÿçûê L?
4.2. Ñèíòàêñè÷åñêèå ìîíîèäû, ñîîòâåòñòâóþùèå ÿçûêàì ñðàùèâàíèÿ.
Äëÿ îòâåòà íà ñôîðìóëèðîâàííûé âûøå âîïðîñ íåîáõîäèìî ïîêàçàòü, êàê ðåøà-
åòñÿ ñëåäóþùàÿ çàäà÷à: áóäåò ëè äàííîå ïðàâèëî ñðàùèâàíèÿ îòíîñèòüñÿ ê ðåãó-
ëÿðíîìó ÿçûêó L X� * [12].
Ïóñòü � � ( , , , , )A X f a F0 — ìèíèìàëüíûé äåòåðìèíèðîâàííûé àâòîìàò,
äîïóñêàþùèé ÿçûê L . Äëÿ êàæäîãî ñîñòîÿíèÿ a A� è êàæäîãî ñëîâà p X� *
îïðåäåëèì ñîñòîÿíèå b f a p� ( , ) , â êîòîðîå ïåðåõîäèò àâòîìàò � èç ñîñòîÿíèÿ a
ïîä äåéñòâèåì ñëîâà p. Çàìåòèì, ÷òî ïðàâèëî r u u v v� � �( , , , ) îòíîñèòñÿ ê ÿçû-
êó L òîãäà è òîëüêî òîãäà, êîãäà äëÿ ëþáîé ïàðû ñîñòîÿíèé a a A, �� , äëÿ êîòîðîé
ìíîæåñòâà { | ( , ) }*x X f a uu x F� � � è { | ( , ) }*y X f a v vy F� � � � íåïóñòû, ìíîæåñ-
òâî { | ( , ) }*z X f a v vz F� � � � âêëþ÷àåòñÿ â ìíîæåñòâî { | ( , ) }*z X f a uvz F� � . Ýòè
óñëîâèÿ ëåãêî ïðîâåðèòü, ïîñêîëüêó ïðîáëåìû ïóñòîòû ÿçûêà è âêëþ÷åíèÿ äëÿ ðå-
ãóëÿðíûõ ÿçûêîâ ðàçðåøèìû.
Ïîêàæåì òåïåðü, êàêèì îáðàçîì ñïåöèôèöèðîâàòü âñå ïðàâèëà, êîòîðûå îò-
íîñÿòñÿ ê ðåãóëÿðíîìó ÿçûêó L , èñïîëüçóÿ ôàêò êîíå÷íîñòè ÷èñëà ïðàâèë. Ýòà
ñïåöèôèêàöèÿ îïèðàåòñÿ íà îòíîøåíèå R ñèíòàêñè÷åñêîé êîíãðóýíòíîñòè, êîòî-
ðîå îïðåäåëÿåòñÿ íà X * è çàäàåòñÿ ñëåäóþùèì îáðàçîì: p Rp� �
10 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 5
� � � � !! � " � � ! � " # $( x y X xp y xpy L xp y xpy L . Ôàêòîð-ìíîæåñòâî X R* / íà-
çûâàåòñÿ ñèíòàêñè÷åñêèì ìîíîèäîì.  ñèëó ðåãóëÿðíîñòè L ÷èñëî êëàññîâ ýêâè-
âàëåíòíîñòè n L( ) ïî ýòîìó îòíîøåíèþ áóäåò êîíå÷íûì. Òîãäà ñóùåñòâóåò â òî÷-
íîñòè m n L� ( ( ))4 óïîðÿäî÷åííûõ ÷åòâåðîê êëàññîâ êîíãðóýíòíîñòè. Ïóñòü
( , , , )W U V Z — óïîðÿäî÷åííàÿ ÷åòâåðêà êëàññîâ êîíãðóýíòíîñòè, r w x y z� ( , , , ) è
r w x y z� � � � � �( , , , ) — äâà ïðàâèëà ñðàùèâàíèÿ èç ìíîæåñòâà W U V Z� � � . Äîêà-
æåì, ÷òî r îòíîñèòñÿ ê ÿçûêó L òîãäà è òîëüêî òîãäà, êîãäà r� îòíîñèòñÿ ê ÿçûêó
L .  ñèëó ñèììåòðèè ïðàâèë r è r� â ýòîì óòâåðæäåíèè äîñòàòî÷íî ïîêàçàòü, ÷òî
åñëè r îòíîñèòñÿ ê ÿçûêó L , òî r� òàêæå îòíîñèòñÿ ê ÿçûêó L .
Ïóñòü r îòíîñèòñÿ ê ÿçûêó L è ñëîâà uw x v� � , sy z t L� � � , ïîêàæåì, ÷òî
uw z t L� � � . Èç òîãî, ÷òî w Rw� , ïîëó÷àåì uwx v L� � è èç òîãî, ÷òî x Rx� , ïîëó÷àåì
uwxv L� . Èç òîãî, ÷òî y Ry� è z Rz� , ñëåäóåò, ÷òî syzt L� . Ïîñêîëüêó r îòíîñèòñÿ ê
L è uwxv syzt L, � , òî uwzt L� , à èç òîãî, ÷òî w Rw� è z Rz� , ñëåäóåò uw z t L� � � , ÷òî
è òðåáîâàëîñü ïîêàçàòü.
Ñëåäîâàòåëüíî, äëÿ îïðåäåëåíèÿ âñåõ ïðàâèë, êîòîðûå îòíîñÿòñÿ ê ÿçûêó L ,
íåîáõîäèìî ïîñòðîèòü ( ( ))n L 4 ÷åòâåðîê ñèíòàêñè÷åñêèõ êëàññîâ íà X * ñ ïî-
ìîùüþ L . Çàòåì èç êàæäîé òàêîé ÷åòâåðêè ( , , , )W U V Z ñëåäóåò âûáðàòü ïî îäíî-
ìó ñëîâó-ïðåäñòàâèòåëþ êàæäîãî êëàññà äëÿ ïîëó÷åíèÿ îäíîãî ïðàâèëà
( , , , )w x y z , ÷òîáû îïðåäåëèòü, áóäåò ëè îíî îòíîñèòüñÿ ê ÿçûêó L . Åñëè îíî îò-
íîñèòñÿ ê L , òî è êàæäîå ïðàâèëî èç W U V Z� � � îòíîñèòñÿ ê L . Â ïðîòèâíîì
ñëó÷àå íè îäíî ïðàâèëî èç W U V Z� � � íå îòíîñèòñÿ ê ÿçûêó L . Òàêèì îáðàçîì,
èìååò ìåñòî ñëåäóþùàÿ òåîðåìà.
Òåîðåìà 5. Ïóñòü L — ðåãóëÿðíûé ÿçûê. Ìíîæåñòâî ïðàâèë, êîòîðûå îòíî-
ñÿòñÿ ê ÿçûêó L , èìååò âèä
{ }W U V Zi i i i
i
m
� � �
�1
� ,
ãäå m n L� �( ( ))4 0 — íàòóðàëüíîå ÷èñëî è êàæäîå èç ìíîæåñòâ W U V Zi i i i, , ,
( )1 � �i m ÿâëÿåòñÿ ýëåìåíòîì ñèíòàêñè÷åñêîãî ìîíîèäà ÿçûêà L .
Ïîñêîëüêó êàæäûé ñèíòàêñè÷åñêèé êëàññ ðåãóëÿðíîãî ÿçûêà ñàì ÿâëÿåòñÿ
ðåãóëÿðíûì ÿçûêîì, òî ïåðå÷èñëèì âñå ñëîâà äëèíû, íå áîëüøåé ðàäèóñà k ïðà-
âèë ñðàùèâàíèÿ â ýòîì êëàññå. Åñëè ïðåäñòàâëåíèå, äàííîå â òåîðåìå 5, ïîñòðîå-
íî, òî ìíîæåñòâî âñåõ ïðàâèë ðàäèóñà, íå áîëüøåãî k , ñîõðàíÿþùèõ ÿçûê L ,
ìîæíî ïåðå÷èñëèòü áåç äîïîëíèòåëüíûõ ïðîâåðîê. Äëÿ êàæäîãî ìíîæåñòâà
W U V Z i mi i i i� � � � �( )1 â ýòîì ïðåäñòàâëåíèè ïåðå÷èñëèì âñå ïðàâèëà
( , , , )w x y z èç W U V Zi i i i� � � ðàäèóñà, íå áîëüøåãî k. Äëÿ òîãî ÷òîáû âûïîë-
íèòü òàêîå ïåðå÷èñëåíèå áåç èñïîëüçîâàíèÿ ñèíòàêñè÷åñêîãî ìîíîèäà, íåîáõîäè-
ìî ïåðåáðàòü êàæäîå èç ïðàâèë ðàäèóñà, íå áîëüøåãî k , â ìíîæåñòâå ( ( ))n L 4
è ïðîâåðèòü êàæäîå èç íèõ íà ïðåäìåò ñîõðàíåíèÿ ÿçûêà L [31].
ÊÎÍÅ×ÍÛÅ ÀÂÒÎÌÀÒÛ ÍÀÄ ÑËÎÂÀÌÈ ÁÅÑÊÎÍÅ×ÍÎÉ ÄËÈÍÛ
Îáîáùåíèåì êîíå÷íûõ X -àâòîìàòîâ ÿâëÿþòñÿ ÊÀ íàä áåñêîíå÷íûìè ñëîâàìè.
 îñíîâå òàêîãî îáîáùåíèÿ ëåæèò ìîäåëü X -àâòîìàòà, àíàëîãè÷íàÿ ðàññìîò-
ðåííîé âûøå, îäíàêî íà âõîä äàííîãî àâòîìàòà ïîäàþòñÿ ñëîâà íå êîíå÷íîé,
à áåñêîíå÷íîé äëèíû.  ñâÿçè ñ ýòèì óñëîâèÿ ðàñïîçíàâàíèÿ ÿçûêà, âîñïðèíè-
ìàåìîãî òàêèì àâòîìàòîì, èçìåíÿþòñÿ. Ïðè ýòîì èçìåíÿþòñÿ è ñâîéñòâà òà-
êèõ àâòîìàòîâ. Èìååòñÿ äâà òèïà àâòîìàòîâ ýòîãî ðîäà: àâòîìàòû Áþõè è îá-
îáùåííûå àâòîìàòû Áþõè, íàçûâàåìûå àâòîìàòàìè Ìþëëåðà [14].
1. Îñíîâíûå ñâîéñòâà. Ïóñòü X x x xn� { , , , }1 2 � — êîíå÷íûé àëôàâèò.
Ìíîæåñòâî âñåõ ñëîâ áåñêîíå÷íîé äëèíû â ýòîì àëôàâèòå îáîçíà÷èì X � , à ïðî-
èçâîëüíîå ïîäìíîæåñòâî L ìíîæåñòâà X � áóäåì íàçûâàòü �-ÿçûêîì.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 5 11
Îïðåäåëåíèå 2. Íåäåòåðìèíèðîâàííûì àâòîìàòîì Áþõè � íàä ñëîâàìè
áåñêîíå÷íîé äëèíû â àëôàâèòå X íàçûâàåòñÿ ïÿòåðêà ( , , , , )A X f A F0 , ãäå A —
êîíå÷íîå ìíîæåñòâî ñîñòîÿíèé àâòîìàòà, A A0 % — ìíîæåñòâî íà÷àëüíûõ ñî-
ñòîÿíèé, f A X A% � � — îòíîøåíèå ïåðåõîäîâ, F A� — ìíîæåñòâî çàêëþ÷è-
òåëüíûõ ñîñòîÿíèé.
Íåäåòåðìèíèðîâàííûì àâòîìàòîì Ìþëëåðà � íàä ñëîâàìè áåñêîíå÷íîé
äëèíû â àëôàâèòå X íàçûâàåòñÿ ïÿòåðêà ( , , , , )A X f A0 � , ãäå A f A, , 0 îáîçíà÷å-
íû âûøå, à ìíîæåñòâî çàêëþ÷èòåëüíûõ ñîñòîÿíèé � � B A( ) , ãäå B A( ) — áóëå-
àí ìíîæåñòâà A .
×åòâåðêà ( , , , )A X f A0 íàçûâàåòñÿ òàáëèöåé ïåðåõîäîâ àâòîìàòà.
Àâòîìàòû Áþõè è Ìþëëåðà ÷àñòî íàçûâàþò �-àâòîìàòàìè, åñëè íåò íåîáõî-
äèìîñòè èõ ðàçëè÷àòü. Òàáëèöà ïåðåõîäîâ ( , , , )A X f A0 íàçûâàåòñÿ äåòåðìèíè-
ðîâàííîé, åñëè | |A0 1� , è äëÿ ëþáûõ x X� è a A� ñóùåñòâóåò íå áîëåå îäíîãî
a A�� òàêîãî, ÷òî ( , , )a x a f� � . Íàçûâàåòñÿ �-àâòîìàò äåòåðìèíèðîâàííûì, åñëè
äåòåðìèíèðîâàíà åãî òàáëèöà ïåðåõîäîâ; �-àâòîìàò ñòàðòóåò â îäíîì èç íà÷àëü-
íûõ ñîñòîÿíèé; åñëè ( , , )s x s f� � , òî àâòîìàò ìîæåò èçìåíèòü ñâîå ñîñòîÿíèå s íà
s� ïîä äåéñòâèåì âõîäíîãî ñèìâîëà x X� .
Äëÿ ñëîâà � � x x x1 2 3� â àëôàâèòå X âûðàæåíèå
r s s s
x x x
� � � �0 1 2
1 2 3
...
íàçûâàåòñÿ òðàññîé àâòîìàòà � íàä � , êîòîðàÿ íà÷èíàåòñÿ â ñîñòîÿíèè
s A0 0� è ( , , )s x s fi i i� �1 äëÿ âñåõ i � 1 . Äëÿ òðàññû r ìíîæåñòâî inf(r) ñîñòîèò
èç ñîñòîÿíèé s A� òàêèõ, ÷òî s si� äëÿ áåñêîíå÷íîãî ÷èñëà ðàç i � 0.
Òðàññà r àâòîìàòà � íàä ñëîâîì � �� X íàçûâàåòñÿ âîñïðèíèìàþùåé òðàñ-
ñîé òîãäà è òîëüêî òîãäà, êîãäà inf inf( ) ( ( )r F r & ' �� ). Äðóãèìè ñëîâàìè,
òðàññà r ÿâëÿåòñÿ âîñïðèíèìàþùåé òîãäà è òîëüêî òîãäà, êîãäà íåêîòîðîå ñîñòîÿ-
íèå èç ìíîæåñòâà F (ìíîæåñòâî èç � ) ïîâòîðÿåòñÿ áåñêîíå÷íî ÷àñòî íà òðàññå r.
ßçûê L X� � íàçûâàåòñÿ äîïóñêàåìûì àâòîìàòîì � , åñëè îí ñîñòîèò èç ñëîâ
� �� X òàêèõ, ÷òî àâòîìàò � èìååò òðàññó r , êîòîðàÿ âîñïðèíèìàåò �.  ýòîì
ñëó÷àå ÿçûê L áóäåì îáîçíà÷àòü L( )� .
Îïðåäåëåíèå 3. �-ÿçûê íàçûâàåòñÿ ðåãóëÿðíûì �-ÿçûêîì òîãäà è òîëüêî
òîãäà, êîãäà îí äîïóñêàåòñÿ íåêîòîðûì àâòîìàòîì Áþõè.
Òåîðåìà 6. Ïðèâåäåì îñíîâíûå ñâîéñòâà íåäåòåðìèíèðîâàííûõ àâòîìàòîâ
Áþõè [13, 14]:
à) �-ÿçûê L X� � äîïóñêàåòñÿ íåêîòîðûì àâòîìàòîì Áþõè òîãäà è òîëüêî
òîãäà, êîãäà ýòîò ÿçûê ÿâëÿåòñÿ îáúåäèíåíèåì êîíå÷íîãî ÷èñëà ìíîæåñòâ âèäà
U V� � , ãäå U V X, *� ÿâëÿþòñÿ ðåãóëÿðíûìè ÿçûêàìè ñëîâ êîíå÷íîé äëèíû; áî-
ëåå òîãî, ñïðàâåäëèâî âêëþ÷åíèå V V V� � ;
á) åñëè V X� * ÿâëÿåòñÿ ðåãóëÿðíûì ÿçûêîì, òî ÿçûê V � äîïóñêàåòñÿ íåêî-
òîðûì àâòîìàòîì Áþõè;
â) åñëè V X� *— ðåãóëÿðíûé ÿçûê è L X� � ÿâëÿåòñÿ ÿçûêîì, êîòîðûé äî-
ïóñêàåòñÿ àâòîìàòîì Áþõè, òî ÿçûê V L� ÿâëÿåòñÿ ÿçûêîì, êîòîðûé òàêæå äîïó-
ñêàåòñÿ íåêîòîðûì àâòîìàòîì Áþõè;
ã) êëàññ ÿçûêîâ, äîïóñêàåìûõ íåäåòåðìèíèðîâàííûìè àâòîìàòàìè Áþõè,
çàìêíóò îòíîñèòåëüíî îïåðàöèé îáúåäèíåíèÿ, ïåðåñå÷åíèÿ è äîïîëíåíèÿ;
ä) �-ðåãóëÿðíûé ÿçûê íåïóñò òîãäà è òîëüêî òîãäà, êîãäà îí âêëþ÷àåò áåñêî-
íå÷íîå �-ñëîâî ïåðèîäè÷åñêîãî õàðàêòåðà pqqq � � � ;
å) ïðîáëåìà ïóñòîòû ÿçûêà äëÿ àâòîìàòîâ Áþõè ÿâëÿåòñÿ àëãîðèòìè÷åñêè
ðàçðåøèìîé.
Íà ýòèõ ñâîéñòâàõ àâòîìàòîâ ïîñòðîåíî áîëüøèíñòâî àëãîðèòìîâ ïðîâåðêè âû-
ïîëíèìîñòè ôîðìóë íà ìîäåëÿõ (àëãîðèòìû model checking) â ìîäàëüíûõ ëîãèêàõ.
12 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 5
Îòìåòèì, ÷òî êëàññû ÿçûêîâ, âîñïðèíèìàåìûõ íåäåòåðìèíèðîâàííûìè àâ-
òîìàòàìè Áþõè, à òàêæå äåòåðìèíèðîâàííûìè è íåäåòåðìèíèðîâàííûìè àâòîìà-
òàìè Ìþëëåðà, ñîâïàäàþò. Êëàññ äåòåðìèíèðîâàííûõ àâòîìàòîâ Áþõè íå çà-
ìêíóò îòíîñèòåëüíî îïåðàöèè äîïîëíåíèÿ ÿçûêîâ, ïîýòîìó îí ÿâëÿåòñÿ
ñîáñòâåííûì ïîäêëàññîì êëàññà íåäåòåðìèíèðîâàííûõ àâòîìàòîâ Áþõè.
2. ÊÀ, ëèíåéíàÿ ëîãèêà è âåðèôèêàöèÿ. ÊÀ íàä áåñêîíå÷íûìè ñëîâàìè
èñïîëüçóþòñÿ â ïðîöåäóðàõ ìîäåëèðîâàíèÿ è âåðèôèêàöèè ñâîéñòâ ðåàêòèâíûõ
ñèñòåì. Â ïðîöåññå òàêîé âåðèôèêàöèè èñïîëüçóþòñÿ ìîäåëü Êðèïêå, êîòîðàÿ
ìîäåëèðóåò âåðèôèöèðóåìóþ ñèñòåìó, è ëîãè÷åñêàÿ ôîðìóëà, îïèñûâàþùàÿ
îæèäàåìîå ïîâåäåíèå âåðèôèöèðóåìîé ñèñòåìû, âûïîëíèìîñòü êîòîðîé ïðî-
âåðÿåòñÿ íà ýòîé ìîäåëè (model checking). Ëîãè÷åñêàÿ ôîðìóëà íàçûâàåòñÿ ñïå-
öèôèêàöèåé ñèñòåìû, è äëÿ åå çàïèñè ÷àñòî èñïîëüçóåòñÿ ÿçûê ëèíåéíîé òåì-
ïîðàëüíîé ëîãèêè (ËÒË). Òàêàÿ âåðèôèêàöèÿ âîçìîæíà áëàãîäàðÿ òðàíñëèðóå-
ìîñòè â �-àâòîìàòû êàê ìîäåëè Êðèïêå, òàê è ëîãè÷åñêîé ôîðìóëû.
Ñóùåñòâóåò íåñêîëüêî àëãîðèòìîâ òðàíñëÿöèè ËÒË-ôîðìóë â �-àâòîìàòû.
Áîëüøèíñòâî òàêèõ àëãîðèòìîâ áàçèðóåòñÿ íà ìåòîäå ñåìàíòè÷åñêîãî òàáëî [32].
Íàèáîëåå ïîïóëÿðíûì ÿâëÿåòñÿ àëãîðèòì, ïðåäëîæåííûé â ìîíîãðàôèè [33].
Ýòîò àëãîðèòì ïî ËÒË-ôîðìóëå � ñòðîèò ñîîòâåòñòâóþùèé àâòîìàò Áþõè ��
ñ ÷èñëîì ñîñòîÿíèé, êîòîðîå íå ïðåâûøàåò âåëè÷èíû 2O (| |)� , ãäå | |� — äëèíà
ôîðìóëû �. Ïîñòðîåííûé àâòîìàò äîïóñêàåò ÿçûê L X� � �{ | | }� � �� , ãäå
X B AP� ( ) — áóëåàí ìíîæåñòâà AP àòîìàðíûõ ôîðìóë ôîðìóëû � .
×òîáû ïðèìåíèòü ýòîò àëãîðèòì, íåîáõîäèìî ËÒË-ôîðìóëó ïðèâåñòè ê òàê
íàçûâàåìîé íåãàòèâíîé íîðìàëüíîé ôîðìå, â êîòîðîé îòðèöàíèÿ ïðèìåíÿþòñÿ
òîëüêî ê ïðîïîçèöèîíàëüíûì ïåðåìåííûì.
Àëãîðèòì òðàíñëÿöèè ËÒË-ôîðìóë â �-àâòîìàòû â ðàìêàõ îãðàíè÷åííîãî îáú-
åìà ñòàòüè èçëîæèòü çàòðóäíèòåëüíî, ïîýòîìó çäåñü áóäóò ïðèâåäåíû òîëüêî íåêî-
òîðûå ïîäãîòîâèòåëüíûå ÷àñòè ýòîãî àëãîðèòìà. (Áîëåå ïîäðîáíî ýòîò âîïðîñ èçëî-
æåí â [33].) Ðàññìîòðèì ñíà÷àëà ñïîñîá òðàíñëÿöèè ìîäåëåé Êðèïêå â �-àâòîìàòû.
Òðàíñëÿöèÿ ìîäåëåé Êðèïêå. Ìîäåëüþ Êðèïêå íàä àëôàâèòîì àòîìàðíûõ
ôîðìóë AP íàçûâàåòñÿ ÷åòâåðêà M S R S f� ( , , , )0 , ãäå S — êîíå÷íîå ìíîæåñò-
âî, ýëåìåíòû êîòîðîãî íàçûâàþòñÿ òî÷êàìè; R S S� � — áèíàðíîå îòíîøåíèå
ïåðåõîäîâ ìåæäó òî÷êàìè; S S0 � — ìíîæåñòâî íà÷àëüíûõ òî÷åê;
f S B AP: ( )� — ôóíêöèÿ, ñîïîñòàâëÿþùàÿ äàííîé òî÷êå s S� ìíîæåñòâî àòî-
ìàðíûõ ôîðìóë, èñòèííûõ â ýòîé òî÷êå.
Äëÿ ìîäåëåé Êðèïêå ïðîáëåì ñ òðàíñëÿöèåé â �-àâòîìàòû íå âîçíèêàåò, ïî-
ñêîëüêó îíà íåïîñðåäñòâåííî ñîîòíîñèòñÿ ñ �-àâòîìàòîì (Áþõè èëè Ìþëëåðà), âñå
ñîñòîÿíèÿ êîòîðîãî çàêëþ÷èòåëüíûå, à ìíîæåñòâî âîçìîæíûõ ïîâåäåíèé ñèñòåìû
çàäàåòñÿ �-ÿçûêîì L( )� , äîïóñêàåìûì ñîîòâåòñòâóþùèì àâòîìàòîì � .
Ôîðìàëüíîå îïðåäåëåíèå òðàíñëÿöèè ìîäåëè Êðèïêå â �-àâòîìàò ñëåäóþùåå.
Ïóñòü M S R S f� ( , , , )0 — ìîäåëü Êðèïêå íàä ìíîæåñòâîì àòîìàðíûõ ôîð-
ìóë AP. Ïî ýòîé ìîäåëè ñòðîèì àâòîìàò Áþõè � � ( , ,A X Q, { }, )a F0 , ãäå
A S a� �{ }0 — ìíîæåñòâî ñîñòîÿíèé; a0 — åäèíñòâåííîå íà÷àëüíîå ñîñòîÿíèå;
X B AP� ( ) , ãäå B AP( ) — áóëåàí ìíîæåñòâà AP ; F A� — ìíîæåñòâî çàêëþ÷è-
òåëüíûõ ñîñòîÿíèé; Q — îòíîøåíèå ïåðåõîäîâ, êîòîðîå îïðåäåëÿåòñÿ òàêèì îá-
ðàçîì: � � � " �a a A x X, òðîéêà ( , , )a x a Q� � òîãäà è òîëüêî òîãäà, êîãäà
f a x a a R a a a S( ) (( , ) ( ))� " � � � � " ��0 0 .
Ïðèìåð 5. Ïóñòü äàíà ìîäåëü Êðèïêå
(ðèñ. 4), â êîòîðîé s s S1 2 0, � , S s s s� { , , }1 2 3 .
Òîãäà òàêîé ìîäåëè ñîîòâåòñòâóåò àâòîìàò
Áþõè, ïðåäñòàâëåííûé íà ðèñ. 5.
Ñïåöèôèêàöèþ � òàêæå ìîæíî ïðåäñòàâèòü
â âèäå àâòîìàòà �� íàä òåì æå àëôàâèòîì
X B AP� ( ) .  ýòîì ñëó÷àå �-ÿçûê L( )�� îïðåäå-
ëÿåò ìíîæåñòâî äîïóñòèìûõ ïîâåäåíèé ñèñòåìû.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 5 13
Ðèñ. 4. Ìîäåëü Êðèïêå
Òðàíñëÿöèÿ ËÒË-ôîðìóë â �-àâòîìàòû.
Àëãîðèòì òðàíñëÿöèè òðåáóåò îïðåäåëåíèÿ ìíî-
æåñòâà ïîäôîðìóë äëÿ äàííîé ËÒË-ôîðìóëû � .
Ýòî ìíîæåñòâî, îáîçíà÷àåìîå sub( )� , îïðåäåëÿ-
åòñÿ ñëåäóþùèì îáðàçîì:
— áóëåâû êîíñòàíòû 0, 1 è ñàìà ôîðìóëà �
ïðèíàäëåæàò sub( )� ;
— åñëè � � �1 2� �sub( ) ,
òî { , } ( )� � �1 2 � sub ;
— åñëè � � �1 2" �sub( ) ,
òî �� � �1 2, } ( )� sub ;
— åñëè �� �1 �sub( ) ,
òî { } ( )� �1 � sub ;
— åñëè � � �1 2U �sub ( ) ,
òî �� � �1 2, } ( )� sub ;
— åñëè � � �1 2R �sub ( ) ,
òî �� � �1 2, } ( )� sub ,
ãäå � , ,U R — îïåðàòîðû ËÒË, íàçûâàåìûå next-time , untill è release ñîîòâåò-
ñòâåííî. Î÷åâèäíî, ÷òî | ( )| (| | )sub O� �� , à ÷èñëî ïîäìíîæåñòâ ìíîæåñòâà
sub( )� èìååò âèä | ( ( ))| (| |)B sub O� �� 2 , ãäå | |� — äëèíà ôîðìóëû � .
Îñíîâíàÿ èäåÿ àëãîðèòìà òðàíñëÿöèè îñíîâûâàåòñÿ íà òàêèõ ñâîéñòâàõ ñå-
ìàíòèêè ËÒË äëÿ w S� :
— äëÿ äîêàçàòåëüñòâà òîãî, ÷òî w |� �� �1 2 , íåîáõîäèìî äîêàçàòü âûïîëíè-
ìîñòü w |� �1 èëè w |� �2 ;
— äëÿ äîêàçàòåëüñòâà òîãî, ÷òî w |� � �1 2U , íåîáõîäèìî äîêàçàòü âûïîëíè-
ìîñòü w |� �1 èëè (w |� �2 è w | ))��!� �1 2U ;
— äëÿ äîêàçàòåëüñòâà òîãî, ÷òî w |� � �1 2R , íåîáõîäèìî äîêàçàòü âûïîëíè-
ìîñòü w |� �1 è w |� �2 èëè (w |� �2 è w | ))��!� �1 2R .
Àëãîðèòì òðàíñëÿöèè â ïðîöåññå ðàáîòû ñòðîèò ãðàô ïåðåõîäîâ àâòîìàòà,
äîïóñêàþùèé âñå èíòåðïðåòàöèè, ïðè êîòîðûõ âûïîëíÿåòñÿ äàííàÿ ôîðìóëà.
ÂÐÅÌÅÍÍÛÅ ÊÎÍÅ×ÍÛÅ ÀÂÒÎÌÀÒÛ ÍÀÄ ÑËÎÂÀÌÈ ÁÅÑÊÎÍÅ×ÍÎÉ ÄËÈÍÛ
 êà÷åñòâå ìîäåëè âðåìåííîãî àâòîìàòà (ÂÀ) âûáèðàþòñÿ àâòîìàòû Áþõè è
Ìþëëåðà, íà ñîñòîÿíèÿ è ïåðåõîäû êîòîðûõ íàêëàäûâàþòñÿ âðåìåííûå îãðà-
íè÷åíèÿ. Ñâîéñòâà ÂÀ, èñïîëüçóåìûå â ñèñòåìàõ âåðèôèêàöèè, â îñíîâíîì òå
æå, ÷òî è äëÿ àâòîìàòîâ Áþõè è Ìþëëåðà.
1. Îñíîâíûå ñâîéñòâà âðåìåííûõ ÊÀ. Ïðèâåäåì ñíà÷àëà íåôîðìàëüíîå
îïðåäåëåíèå ÂÀ. Âðåìåííîé àâòîìàò ïðåäñòàâëÿåò ñîáîé êîíå÷íûé �-àâòîìàò,
ñíàáæåííûé ÷àñàìè, çíà÷åíèÿ êîòîðûõ ïðèíàäëåæàò ìíîæåñòâó ðàöèîíàëüíûõ
íåîòðèöàòåëüíûõ ÷èñåë Q
. Ñ÷èòàåòñÿ, ÷òî ïåðåõîäû ÂÀ èç îäíîãî ñîñòîÿíèÿ
â äðóãîå ïðîèñõîäÿò ìãíîâåííî, íî òå÷åíèå âðåìåíè íå îñòàíàâëèâàåòñÿ, ïîêà àâ-
òîìàò íàõîäèòñÿ â íåêîòîðîì ñîñòîÿíèè. Ïðè âûïîëíåíèè ïåðåõîäà çíà÷åíèÿ íå-
êîòîðûõ ÷àñîâ ìîãóò ñáðàñûâàòüñÿ â íóëü.  êàæäûé ìîìåíò âðåìåíè çíà÷åíèÿ
÷àñîâ ôèêñèðóþò âðåìÿ, êîòîðîå ïðîøëî ñ ìîìåíòà ïîñëåäíåãî ñáðàñûâàíèÿ ÷à-
ñîâ. Ñ÷èòàåòñÿ, ÷òî òåìï âðåìåíè îäèíàêîâûé äëÿ âñåõ ÷àñîâ, ïðè÷åì êîíå÷íîå
÷èñëî ïåðåõîäîâ ìîæåò áûòü âûïîëíåíî íà êîíå÷íîì îòðåçêå âðåìåíè.
Ñ êàæäûì ïåðåõîäîì ñâÿçàíî íåêîòîðîå âðåìåííîå îãðàíè÷åíèå. Ïåðåõîä
ìîæåò ïðîèçîéòè òîëüêî òîãäà, êîãäà òåêóùèå çíà÷åíèÿ ÷àñîâ óäîâëåòâîðÿþò
âðåìåííîìó îãðàíè÷åíèþ äàííîãî ïåðåõîäà. Âðåìåííûå îãðàíè÷åíèÿ òàêæå ñâÿ-
çàíû ñ êàæäûì ñîñòîÿíèåì àâòîìàòà, ýòè îãðàíè÷åíèÿ íàçûâàþòñÿ èíâàðèàíòàìè
ñîñòîÿíèé. Âðåìÿ â ñîñòîÿíèè òå÷åò äî òåõ ïîð, ïîêà èíâàðèàíò ýòîãî ñîñòîÿíèÿ
èñòèííûé.
14 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 5
Ðèñ. 5. Àâòîìàò Áþõè äëÿ ìîäåëè
Êðèïêå
Ïðèìåð 6. Ðàññìîòðèì âðåìåííîé àâòîìàò, ïðåäñòàâëåííûé íà ðèñ. 6. Íà-
÷àëüíûì ñîñòîÿíèåì â ýòîì àâòîìàòå ÿâëÿåòñÿ s0 . Àâòîìàò ìîæåò íàõîäèòüñÿ
â ýòîì ñîñòîÿíèè äî òåõ ïîð, ïîêà çíà÷åíèå ÷àñîâ y íå ïðåâûñèò ïÿòè. Êàê òîëüêî
çíà÷åíèå ÷àñîâ y ñòàíåò á�ëüøèì èëè ðàâíûì òðåì, àâòîìàò ìîæåò âûïîëíèòü
ïåðåõîä ïîä äåéñòâèåì ñèìâîëà a â ñîñòîÿíèå s1 è ñáðîñèòü çíà÷åíèå ÷àñîâ x
â íóëü.
Àâòîìàò ìîæåò îñòàâàòüñÿ â ñîñòîÿíèè s1 äî òåõ ïîð, ïîêà y íå ñòàíåò áîëü-
øå äåñÿòè è x íå ñòàíåò áîëüøå âîñüìè. Êîãäà çíà÷åíèå ÷àñîâ y äîñòèãíåò çíà÷å-
íèÿ ÷åòûðåõ, à çíà÷åíèå ÷àñîâ x áóäåò íå áîëüøå øåñòè, àâòîìàò ïîëó÷àåò âîç-
ìîæíîñòü ïåðåéòè ïîä äåéñòâèåì ñèìâîëà b â ñîñòîÿíèå s0 è ñáðîñèòü çíà÷åíèå
÷àñîâ y â íóëü.
Îñòàåòñÿ îáúÿñíèòü ïîâåäåíèå ÂÀ â ñîñòîÿíèè. Ïðåäïîëàãàåòñÿ, ÷òî òå÷åíèå
âðåìåíè áåñêîíå÷íî, ò.å. â êàæäîì ñîñòîÿíèè âðåìåííûå îãðàíè÷åíèÿ ñâåðõó,
êîòîðûå íàêëàäûâàþòñÿ íà çíà÷åíèÿ ÷àñîâ, èëè ðàâíû áåñêîíå÷íîñòè, èëè ìåíü-
øå ìàêñèìàëüíîãî ïðåäåëà, êîòîðûé îïðåäåëÿåòñÿ èíâàðèàíòîì ñîñòîÿíèÿ è
óñëîâèÿìè ïåðåõîäîâ, âîçìîæíûõ äëÿ ÂÀ. Èíûìè ñëîâàìè, â êàæäîì ñîñòîÿíèè
ÂÀ ìîæåò îñòàâàòüñÿ áåñêîíå÷íî äîëãî èëè èíâàðèàíò ñîñòîÿíèÿ çàñòàâèò
ïîêèíóòü ýòî ñîñòîÿíèå è â ýòîò ìîìåíò â ÂÀ âîçìîæåí õîòÿ áû îäèí ïåðåõîä.
Âðåìåííûå îãðàíè÷åíèÿ îïðåäåëÿþòñÿ èíäóêòèâíî ñëåäóþùèì îáðàçîì.
Îïðåäåëåíèå 4. Äëÿ ìíîæåñòâà ïåðåìåííûõ-÷àñîâ C ìíîæåñòâî âðåìåííûõ
îãðàíè÷åíèé E âêëþ÷àåò îãðàíè÷åíèÿ âèäà � � � �� � � ( "true x c c x| | | | 1 2 , ãäå
x C� , à c Q�
— ðàöèîíàëüíîå íåîòðèöàòåëüíîå ÷èñëî.
Îïðåäåëåíèå 5. Êîíå÷íûì íåäåòåðìèíèðîâàííûì âðåìåííûì àâòîìàòîì
Áþõè (ÂÀÁ) íàä àëôàâèòîì X íàçûâàåòñÿ óïîðÿäî÷åííàÿ øåñòåðêà
� � ( , , , , , )A X A C E F0 , ãäå A — êîíå÷íîå ìíîæåñòâî ñîñòîÿíèé; A A0 � —
ìíîæåñòâî íà÷àëüíûõ ñîñòîÿíèé; C — ìíîæåñòâî ÷àñîâ; E A X A� � � �
� �B C C( ) ( )) — ìíîæåñòâî âðåìåííûõ îãðàíè÷åíèé (B C( ) — áóëåàí ìíîæåñòâà
C , à )( )C — ìíîæåñòâî ôîðìóë íàä C); F A� — ìíîæåñòâî çàêëþ÷èòåëüíûõ
ñîñòîÿíèé.
Åñëè â ýòîì îïðåäåëåíèè âìåñòî ìíîæåñòâà F A� ðàññìàòðèâàòü ñåìåéñòâî
ìíîæåñòâ � � B A( ) , ãäå B A( ) — áóëåàí ìíîæåñòâà A , òî òàêîé àâòîìàò íàçûâà-
åòñÿ êîíå÷íûì âðåìåííûì àâòîìàòîì Ìþëëåðà (ÂÀÌ).
Åñëè ïåðåõîä ( , , , , )a a E� � �� � , òî ïðîèñõîäèò ïåðåõîä èç ñîñòîÿíèÿ a â ñî-
ñòîÿíèå a� ïîä äåéñòâèåì ñèìâîëà � � X , ïðè êîòîðîì ÷àñû èç ìíîæåñòâà � � C
ñáðàñûâàþòñÿ â íóëü, à ��)( )C — âðåìåííûå îãðàíè÷åíèÿ ýòîãî ïåðåõîäà.
ÂÀ íà÷èíàåò ñâîþ ðàáîòó â îäíîì èç íà÷àëüíûõ ñîñòîÿíèé, êîãäà âñå ÷àñû
èìåþò íóëåâûå çíà÷åíèÿ.  ìîìåíò âðåìåíè � i àâòîìàò îñóùåñòâëÿåò ïåðåõîä èç
ñîñòîÿíèÿ a â ñîñòîÿíèå a�, ÷èòàÿ âõîäíîé ñèìâîë � � X è èñïîëüçóÿ íåêîòîðûé ïå-
ðåõîä ( , , , , )a a E� � �� � , åñëè òåêóùèå çíà÷åíèÿ ÷àñîâ óäîâëåòâîðÿþò âðåìåííûì
îãðàíè÷åíèÿì ��)( )C . Âñå çíà÷åíèÿ ÷àñîâ èç ìíîæåñòâà � ñáðàñûâàþòñÿ â íóëü.
Ñëåäîâàòåëüíî, êàæäîìó âõîäíîìó ñëîâó p X� � ñîîòâåòñòâóåò ïîñëåäîâàòåëü-
íîñòü � , ýëåìåíòàìè êîòîðîé ÿâëÿþòñÿ çíà÷åíèÿ ÷àñîâ, ñîîòâåòñòâóþùèå ìîìåíòàì
âðåìåíè ÷òåíèÿ ñèìâîëîâ ñëîâà p . Ïàðó ( , )p � íàçûâàþò âðåìåííûì ñëîâîì ÂÀ.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 5 15
Ðèñ. 6. Âðåìåííîé àâòîìàò
Òðàññîé r ÂÀ íàä âðåìåííûì ñëîâîì ( , )p � íàçûâàåòñÿ áåñêîíå÷íàÿ ïîñëå-
äîâàòåëüíîñòü âèäà
r s v s v s v: ( , ) ( , ) ( , )0 0
1
1
1 1
2
2
2 2
3
3
�
�
�
�
�
�
� ,
ãäå s A Xi i� �, � , à v C Ri � �[ ] äëÿ i � 1 óäîâëåòâîðÿþò óñëîâèÿì:
— s A0 0� è v x0 0( ) � äëÿ âñåõ x C� ;
— äëÿ âñåõ i � 1 â ìíîæåñòâå E ñóùåñòâóåò ïåðåõîä ( , , , , )s si i i i i�1 � � � òàêîé,
÷òî ( )vi i i� �
�1 1� � óäîâëåòâîðÿåò �i , a vi èìååò âèä [ ]( )� � �i i i iv�
�� �0 1 1 .
Ìíîæåñòâî inf (r) ñîñòîèò èç òàêèõ ñîñòîÿíèé s , ÷òî s s Fi� � (F Fi� �� )
ïîÿâëÿåòñÿ áåñêîíå÷íîå ÷èñëî ðàç i � 0 .
Âûïîëíåíèå run r s v� ( , ) ÂÀÁ � íàä âðåìåííûì ñëîâîì ( , )� � äîïóñêàåòñÿ
ÂÀ � òîãäà è òîëüêî òîãäà, êîãäà inf(r) & 'F (inf(r)�� ). ßçûê L( )� âðåìåí-
íûõ ñëîâ, êîòîðûå äîïóñêàþòñÿ ÂÀ � , îïðåäåëÿåòñÿ êàê ìíîæåñòâî âñåõ âðå-
ìåííûõ ñëîâ ( , )� � òàêèõ, ÷òî âûïîëíåíèå r íàä ( , )� � äîïóñêàåòñÿ àâòîìàòîì �.
Âðåìåííîé ÿçûê L íàçûâàåòñÿ âðåìåííûì ðåãóëÿðíûì ÿçûêîì òîãäà è òîëüêî
òîãäà, êîãäà ñóùåñòâóåò òàêîé ÂÀ � , ÷òî L L� ( )� . Äëÿ ÂÀÁ è ÂÀÌ èìåþò
ìåñòî óòâåðæäåíèÿ, àíàëîãè÷íûå óòâåðæäåíèþ äëÿ îáû÷íûõ àâòîìàòîâ Áþõè
è Ìþëëåðà [9].
Òåîðåìà 7. Êëàññ âðåìåííûõ ÿçûêîâ, äîïóñêàåìûõ äåòåðìèíèðîâàííûìè
ÂÀÁ, çàìêíóò îòíîñèòåëüíî (êîíå÷íûõ) ïåðåñå÷åíèé è îáúåäèíåíèé è íå çà-
ìêíóò îòíîñèòåëüíî äîïîëíåíèÿ.
Òåîðåìà 8. Êëàññ âðåìåííûõ ÿçûêîâ, êîòîðûå äîïóñêàþòñÿ äåòåðìèíèðî-
âàííûìè ÂÀÌ, ñîâïàäàåò ñ êëàññîì ÿçûêîâ, äîïóñêàåìûõ íåäåòåðìèíèðîâàííû-
ìè ÂÀÁ è ÂÀÌ, è ýòîò êëàññ çàìêíóò îòíîñèòåëüíî îïåðàöèé îáúåäèíåíèÿ, ïåðå-
ñå÷åíèÿ è äîïîëíåíèÿ.
Îòìåòèì, ÷òî ïðàâèëà ôóíêöèîíèðîâàíèÿ ÂÀ ìîãóò èìåòü ðàçëè÷íóþ ñå-
ìàíòèêó, íåêîòîðûå èç íèõ îïèñàíû â [9, 34].
2. ÊÀ è âðåìåííûå ñåòè Ïåòðè. Âðåìåííàÿ ÑÏ — ýòî îáû÷íàÿ ñåòü Ïåòðè,
ñðàáàòûâàíèå ïåðåõîäîâ êîòîðîé äîëæíî óäîâëåòâîðÿòü îïðåäåëåííûì âðåìåí-
íûì îãðàíè÷åíèÿì. Ôîðìàëüíîå îïðåäåëåíèå äàíî â [34].
Îïðåäåëåíèå 6. Âðåìåííîé ÑÏ (ÂÑÏ) íàçûâàåòñÿ óïîðÿäî÷åííàÿ øåñòåðêà
� � ( , , , , , )P T F M Et Lt0 , ãäå ( , , , )P T F M 0 — ñåòü Ïåòðè è Et T N: � ,
Lt T N: { }� � * — ôóíêöèè, îïðåäåëÿþùèå âðåìåííûå èíòåðâàëû âîçìîæíîãî
ñðàáàòûâàíèÿ ïåðåõîäîâ ÑÏ, ïðè÷åì � � �t T Et t Lt t( ( ) ( )) .
Ïóñòü en M( ) — ìíîæåñòâî ïåðåõîäîâ, êîòîðûå ìîãóò ñðàáîòàòü ïðè ðàç-
ìåòêå M . Ýòî ìíîæåñòâî ìîæåò îòëè÷àòüñÿ îò âñåãî ìíîæåñòâà ïåðåõîäîâ T , íî ïðè
èññëåäîâàíèè ïîâåäåíèÿ ÂÑÏ äîñòàòî÷íî èìåòü òîëüêî ýòî ìíîæåñòâî.
Ïðèìåð 7. Ðàññìîòðèì ÂÑÏ, èçîáðàæåííóþ íà ðèñ. 7, ãäå äëÿ i � 1, 3, 5, 6
èìååì Et ti( ) �1 , Lt ti( ) � 2 , Et t( )2 0� , Lt t( )2 3� , Et t Lt t( ) ( )4 4 1� � ,
M 0 � (1, 1, 0, 0, 0, 0, 0, 0) , en M t t( ) ,0 1 2� .
16 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 5
Ðèñ. 7. Âðåìåííàÿ ÑÏ
Âðåìÿ, àññîöèèðîâàííîå ñ ïåðåõîäàìè, èçìåíÿåòñÿ òàêèì îáðàçîì. Íàçîâåì
êîíêðåòíûì ñîñòîÿíèåì ÂÑÏ � ïàðó
�T TM clock� ( , ) ,
ãäå M — ðàçìåòêà ÂÑÏ � , à clock T QT : �
— ôóíêöèÿ, ñîïîñòàâëÿþùàÿ
êàæäîìó âîçìîæíîìó ïåðåõîäó t T� ïðè ðàçìåòêå M (t en M� ( )) âðåìÿ.
Äëÿ ��
Q è t T� âûðàæåíèå clock T
� îçíà÷àåò âðåìÿ clock tT( )
� . Äàëåå
áóäåì ñ÷èòàòü, ÷òî ( , ) ( , )M clock M clockT T
�
� � .
Ïðîñòðàíñòâîì êîíêðåòíûõ ñîñòîÿíèé ÂÑÏ � íàçûâàåòñÿ òðàíçèöèîííàÿ
ñèñòåìà
C CPc
T T T
Tc
( ) ( , ( ) , )� � �� 0 .
Çäåñü CP T — ìíîæåñòâî êîíêðåòíûõ ñîñòîÿíèé ÂÑÏ � ; ( )�T 0 �
� ( , )M clock T
0 0
, ãäå � � �t T clock T( )
0
0 ïðè íà÷àëüíîé ðàçìåòêå M 0 ; �Tc
—
îòíîøåíèå ïåðåõîäîâ, ãäå:
— äëÿ ��
Q ( , )M clock T
Tc�
�
( , ) ( )( ) ( )M clock clock t Lt tT T
�
�� �
� � ! t en M (íàñëåäíèê âðåìåíè);
— äëÿ t T� ( , ) ( , ) ( ), ( )M clock M clock t en M Et tT
t
T
T
c� � � �1 1
clock tT ( ) �
� Lt t( ) , M M
t
� 1 è � � �u T clock uT( ( ) )
1
0 , åñëè u newly� -en M t( , ) , èíà÷å
clock clock uT T
1
� ( ) (íàñëåäíèê äåéñòâèÿ) (newly-en M t( , ) — ñîâîêóïíîñòü ïåðå-
õîäîâ, ñðàáàòûâàíèÿ êîòîðûõ âîçìîæíû ïîñëå âûïîëíåíèÿ ïåðåõîäà t ïðè ðàç-
ìåòêå M ).
Âðåìÿ, àññîöèèðîâàííîå ñ ìåñòàìè, èçìåíÿåòñÿ àíàëîãè÷íûì îáðàçîì. Ïóñòü
ïàðà � P PM clock� ( , ) îçíà÷àåò êîíêðåòíîå ñîñòîÿíèå ÂÑÏ � , ãäå M — ðàçìåò-
êà ÂÑÏ � , clock P QP : �
— ôóíêöèÿ, ñîïîñòàâëÿþùàÿ êàæäîìó ìåñòó p P�
ïðè ðàçìåòêå M âðåìÿ. Äëÿ ��
Q è p P� âûðàæåíèå clock P
� îçíà÷àåò âðåìÿ
clock pP ( )
� . Äàëåå áóäåì ñ÷èòàòü, ÷òî ( , ) ( , )M clock M clockP P
�
� � .
Ïðîñòðàíñòâîì êîíêðåòíûõ ñîñòîÿíèé ÂÑÏ � íàçûâàåòñÿ òðàíçèöèîííàÿ
ñèñòåìà
C CPc
P P P
Pc
( ) ( , ( ) , )� � �� 0 .
Çäåñü CP P — ìíîæåñòâî êîíêðåòíûõ ñîñòîÿíèé ÂÑÏ � ; ( )� P 0 � ( ,M 0
clock P
0
) , ãäå � � �p P clock P( )
0
0 ïðè íà÷àëüíîé ðàçìåòêå M 0 ; �Pc
— îòíîøå-
íèå ïåðåõîäîâ, ãäå:
— äëÿ ��
Q ( , ) ( , )M clock M clockP
P
P
c�
�
�
� äëÿ êàæäîãî t en M� ( ) ñó-
ùåñòâóåò ìåñòî p t�• òàêîå, ÷òî ( )( ) ( )clock p Lt tP
�� (íàñëåäíèê âðåìåíè);
— äëÿ t T� ( , ) ( , ) ( )M clock M clock t en MP
t
P
P
c� � �1 1
, äëÿ êàæäîãî p t�•
èìååò ìåñòî Et t clock pP( ) ( )� , ñóùåñòâóåò p t�• òàêîå, ÷òî clock p Lt tP ( ) ( )� ,
M M
t
� 1 è � � �p P clock pP( ( ) )
1
0 , åñëè p t�• , èíà÷å clock p clock pP P
1
( ) ( )� (íà-
ñëåäíèê äåéñòâèÿ).
Òðàíñëÿöèÿ ÂÑÏ â ÂÀ ïðîèñõîäèò ñîïîñòàâëåíèåì ìíîæåñòâàì êîíêðåòíûõ
ñîñòîÿíèé âðåìåííûõ îãðàíè÷åíèé.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 5 17
Ïóñòü � � ( , , , , , )P T F M Et Lt0 — âðåìåííàÿ ñåòü Ïåòðè. Ïðåäïîëàãàåòñÿ,
÷òî ÂÑÏ îãðàíè÷åííàÿ è îðäèíàðíàÿ. Òàêîé ÂÑÏ ñîïîñòàâëÿåòñÿ ÂÀ
A A L A C E F� � � � � �� ( , , , , , )0 .  ýòîì àâòîìàòå ìíîæåñòâîì ñîñòîÿíèé âû-
ñòóïàåò ìíîæåñòâî âñåõ äîñòèæèìûõ ðàçìåòîê, ñèìâîëàìè âõîäíîãî àëôàâèòà
ÿâëÿþòñÿ ñèìâîëû ìíîæåñòâà ïåðåõîäîâ T , A M0 0� . Ìíîæåñòâî çíà÷åíèé ÷àñîâ
èìååò âèä C x t Tt� � �{ | } , ò.å. ÷àñû îïðåäåëåíû äëÿ êàæäîãî ïåðåõîäà ÂÑÏ � .
Èíâàðèàíòû ñîñòîÿíèé M A� � íàõîäÿòñÿ ñëåäóþùèì îáðàçîì:
F M
x Lt t t T t en
t T t en M Lt t
t
� ( )
( ), { |
{ | ( ) ( ) }�
� � ��
� � "
*
åñëè ( ) ( ) },M Lt t"
* & '�
�
�
�� true,
Ìíîæåñòâî ïåðåõîäîâ îïðåäåëÿåòñÿ òàê:
E e t en M M AM t� �� � " �{ | ( ) }, .
Äëÿ çàäàííîãî ïåðåõîäà e EM t, �
�
, ñîîòâåòñòâóþùåãî ñðàáàòûâàþùåìó ïåðå-
õîäó t en M� ( ) ïðè ðàçìåòêå M , óñëîâèå ïåðåõîäà íàõîäèòñÿ èç âûðàæåíèÿ
quard e x Et tM t t� ( ) ( ( )), � � ,
à ìíîæåñòâî çíà÷åíèé ÷àñîâ óñòàíàâëèâàåòñÿ ðàâåíñòâîì
reset M t x C x newlyu u� �( , ) { |� � � -en M t( , )} .
Ïåðåõîäû àâòîìàòà A� èìåþò âèä
e M MM t
t cc X
,
, ,
:� + �+++ 1 ,
ãäå cc quard eM t� � ( ), è X reset M t� � ( , ) .
Ïðîïîçèöèîíàëüíûå ïåðåìåííûå PVP îïðåäåëÿþòñÿ â çàâèñèìîñòè îò ìåñòà
ÂÑÏ, à ôóíêöèÿ çíà÷åíèé V A B PVP� ��
: ( )� èìååò âèä
V M V p
p P M p
� ��
( ) ( ) .
{ | ( ) }
�
� �0
�
Ïðè ýòîì äâå ìîäåëè ÂÑÏ è ñîîòâåòñòâóþùåãî åé ÂÀ äîëæíû áûòü áèñèìó-
ëÿöèîííî ýêâèâàëåíòíû.
Ïðèìåð 8. Âðåìåííîé àâòîìàò äëÿ ÂÑÏ ïðåäñòàâëåí íà ðèñ. 8.
Âåðèôèêàöèÿ ñâîéñòâ ÂÑÏ âûïîëíÿåòñÿ ïóòåì ïðîâåðêè ñîîòâåòñòâóþùèõ
ñâîéñòâ ÂÀ. Åñëè õàðàêòåðèçîâàòü ÂÑÏ è ÂÀ, òî îòìåòèì ñëåäóþùåå. ÂÑÏ
îïðåäåëÿþò êëàññ ÂÀ, ñëàáî áèñèìóëÿöèîííî ýêâèâàëåíòíûõ ÂÑÏ. Îáðàòíîå íå
18 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 5
åñëè èíà÷å.
Ðèñ. 8. ÂÀ äëÿ ÂÑÏ èç ðèñ. 7
èìååò ìåñòà, ÷òî ñëåäóåò èç ðåçóëüòàòîâ ðàáîòû [20], ãäå ïîêàçàíî íàëè÷èå ÂÀ,
äëÿ êîòîðûõ íå ñóùåñòâóåò ÂÑÏ, ñëàáî áèñèìóëÿöèîííî ýêâèâàëåíòíûõ ñ íèìè.
Îñíîâíàÿ ïðîáëåìà øèðîêîãî ïðèìåíåíèÿ ýòîãî è ïîäîáíûõ åìó ìåòîäîâ ñîñòîèò
â êîìáèíàòîðíîì âçðûâå ÷èñëà ñîñòîÿíèé ÂÑÏ è ñîîòâåòñòâóþùåãî åé ÂÀ.
Êàê äëÿ ÂÀ, òàê è äëÿ ÂÑÏ ñóùåñòâóåò íåñêîëüêî ñåìàíòèê, îïèñûâàþùèõ
èõ ïîâåäåíèå. Íåêîòîðûå èç ýòèõ ñåìàíòèê äàíû â ìîíîãðàôèè [34].
ÇÀÊËÞ×ÅÍÈÅ
 íàñòîÿùåì îáçîðå ðàññìîòðåíû îñíîâíûå ïðèìåíåíèÿ òåîðèè àâòîìàòîâ
â ðàçëè÷íûõ îáëàñòÿõ ñîâðåìåííîé íàóêè î âû÷èñëåíèÿõ. Ýòî äàëåêî íå ïîë-
íûé ïåðå÷åíü îáëàñòåé, â êîòîðûõ óñïåøíî èñïîëüçóþòñÿ àâòîìàòû. Òàê, íå
ðàññìàòðèâàëèñü çàäà÷è èäåíòèôèêàöèè ñëîâ [8], ïðèâåäåíèÿ îáùèõ ïîäâûðà-
æåíèé â àëãåáðàè÷åñêèõ âûðàæåíèÿõ [35], à òàêæå íå ðàññìàòðèâàëèñü ïðèëî-
æåíèÿ òåîðèè àâòîìàòîâ â îáëàñòè óíèôèêàöèè, ñîçäàíèè àïïàðàòóðû âû÷èñ-
ëèòåëüíûõ ñèñòåì [10, 11], êðèïòîãðàôèè, ëèíãâèñòèêå è äðóãèõ îáëàñòÿõ.
 íàñòîÿùåå âðåìÿ ñôåðà ïðèìåíåíèÿ êîíå÷íûõ àâòîìàòîâ ðàñøèðÿåòñÿ, è ýòà
òåíäåíöèÿ, ïî-âèäèìîìó, áóäåò ñîõðàíÿòüñÿ â áóäóùåì [36].
ÑÏÈÑÎÊ ËÈÒÅÐÀÒÓÐÛ
1. Ã ë ó ø ê î â Â . Ì . Àáñòðàêòíàÿ òåîðèÿ àâòîìàòîâ // Óñïåõè ìàò. íàóê. — 1961. — ¹ 5. —
Ñ. 3–62
2. Ã ë ó ø ê î â Â . Ì . , Ë å ò è ÷ å â ñ ê è é À . À . , Ã î ä ë å â ñ ê è é À . Á . Ìåòîäû ñèíòåçà
äèñêðåòíûõ ìîäåëåé. — Êèåâ: Âèùà øê., 1983. — 262 ñ.
3. Ê î á ð è í ñ ê è é Í . Å . , Ò ð à õ ò å í á ð î ò Á . À . Ââåäåíèå â òåîðèþ êîíå÷íûõ àâòîìàòîâ. — Ì.:
Ôèçìàòãèç, 1962. — 286 ñ.
4. H o p c r o f t J . E . , M o n t w a n i J . , U l l m a n J . D . Introduction to autonmata theory and computa-
tion (Second addition). — Stanford: Addison Wesley, 2001. — 521 p.
5. à è ë ë À . Ââåäåíèå â òåîðèþ êîíå÷íûõ àâòîìàòîâ. — Ì.: Íàóêà, 1966. — 272 ñ.
6. à è í ç á ó ð ã Ñ . Ìàòåìàòè÷åñêàÿ òåîðèÿ êîíòåêñòíî-ñâîáîäíûõ ÿçûêîâ. — Ì.: Ìèð, 1970. —
326 ñ.
7. Ð à á è í Ì . Î . , Ñ ê î ò ò Ä . Êîíå÷íûå àâòîìàòû è çàäà÷è èõ ðàçðåøåíèÿ // Êèáåðíåòè÷åñêèé
ñáîðíèê (Ñòàðàÿ ñåðèÿ). — Ì.: Èçä-âî èíîñòð. ëèò., 1962. — Ñ. 58–98.
8. S m i t h B . Computing patterns in strings. — UK: Pearson Education Limited, 2003. — 423 p.
9. A l u r R . , D i l l D . L . A theory of timed automata // TCS. — 1994. — N 126. — P. 183–235.
10. Ã ë ó ø ê î â Â . Ì . Ñèíòåç öèôðîâûõ àâòîìàòîâ. — Ì.: Ôèçìàòãèç, 1962. — 562 ñ.
11. B e y g a L . , G a j e w s k i T . , M i a d o w i c z Z . , S i w a k P . , S t o k l o s a J . , B e r g a n d y J . ,
M i k o l a j c z a k B . Algebraic and structural automata theory. — Amsterdam: Elsevier Science Pub-
lishers B.V., 1991. — 402 p.
12. A n d e r s o n J . Automata theory with modern applications. — Cambridge: Cambridge University
Press, 2006. — 255 p.
13. Ò ð à õ ò å í á ð î ò Á . À . , Á à ð ç ä è í ü ß . Ì . Êîíå÷íûå àâòîìàòû (ïîâåäåíèå è ñèíòåç). — Ì.:
Íàóêà, 1970. — 400 ñ.
14. T h o m a s W . Automata on infinite objects. Handbook on theoretical computer science. — Amster-
dam: Elsevier Science Publishers B.V., 1990. — P. 133–191.
15. G e' c s e g F . , S t e i n b y M . Tree automata. — Hungary: Akademiai Kiado, 1984. — 262 p.
16. G e' c s e g F . , S t e i n b y M . Tree languages. Handbook of formal languages. — Amsterdam:
Elsevier Science Publishers B.V., 1996. — 3. — P. 1–68.
17. C o m o n H . , D a u c h e t M . , G i l l e r o n R . , J a c q u e m a n d F . , L u g i e s D . , T i s o n S . ,
T o m m a s i M . Tree automata: techniques and applications. TATA, 1999. — 193 p.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 5 19
18. Ô ð å é â à ë ä Ð .  . Ðàñïîçíàâàíèå ÿçûêîâ íà êîíå÷íûõ âåðîÿòíîñòíûõ ìíîãîëåíòî÷íûõ è
ìíîãîãîëîâî÷íûõ àâòîìàòàõ // Ïðîáëåìû ïåðåäà÷è èíôîðìàöèè. — 1979. — 15, ¹ 3. —
Ñ. 99–106.
19. Á ó õ à ð à å â Ð . Ã . Îñíîâû òåîðèè âåðîÿòíîñòíûõ àâòîìàòîâ. — Ì.: Íàóêà, 1985. — 394 ñ.
20. B e r a r d B . , C a s s e z F . , H a d d a d D . , L i m e D . , R o u x O . H . Comparison of the expres-
siveness of time automata and time Petri nets // Proc. of the 3rd Int. Workshop on Formal Analysis
and Modeling of Timed Systems (FORMATS’05). — Springer-Verlag. — LNCS. — 2005. — 3829.
— P. 211–225.
21. Ò î ô ô î ë è Ò . , Ì à ð ã î ë ó ñ Í . Ìàøèíû êëåòî÷íûõ àâòîìàòîâ. — Ì.: Ìèð, 1991. — 272 ñ.
22. H e n z i n g e r T . A , K o p k e P . W . , P u r i A . , V a r i a y a P . What’s decidable about hybrid au-
tomata // J. of Computer and System Science. — 1998. — 57. — P. 94–124.
23. Ê ð è â î é Ñ . Ë . Îá àëãîðèòìå ïîñòðîåíèÿ áàçèñà ïåðåñå÷åíèÿ êîíå÷íî ïîðîæäåííûõ
ñâîáîäíûõ ãðóïï // Êèáåðíåòèêà. — 1982. — ¹ 4. — C. 5–11.
24. Ë å ò è ÷ å â ñ ê è é À . À . , Ã î ä ë å â ñ ê è é À . Á . , Ê ð è â î é Ñ . Ë . Îá ýôôåêòèâíîñòè àëãîðèòìà
ïîñòðîåíèÿ áàçèñà ïîäãðóïïû ñâîáîäíîé ãðóïïû // Êèáåðíåòèêà. — 1981. — ¹ 3. —
C. 107–116.
25. C l a u s e n M . , F o r t e n b a c h e r A . Efficient solution of linear diophantine equations // J. Sym-
bolic Computation. — 1989. — 8, N 1. — P. 201–216.
26. R o m e u f J . F . A polinomial algorithm for solvin systems of two linear Diophantine equations //
TCS. — 1990. — 74, N 3. — P. 329–340.
27. H e a d T . Formal language theory and DNA: an analysis of the generative capacity of specific re-
combinant behaviors // Bull. Math. Biology. — 1987. — N 49. — P. 737–759.
28. C u l i k K . , H a r j u T . The regularity of splicing systems and DNA // Proc. ICALP — 89. — 1989.
— N 372. — P. 222–233.
29. C u l i k K . , H a r j u T . Splicing semigroup of dominoes and DNA // Discrete Applied Mathem. —
1991. — N 31. — P. 261–277.
30. G a t t e r d a m R . W . Splicing systems and regularity // Intern. J. Computer Math. — 1989. —
N 31. — P. 63–67.
31. G o o d e E . Constants and splicing systems. — Binghamton: Dissertation binghamton university,
1999. — 36 p.
32. B e n - A r i M . Mathematical logic for computer science (Second addition). — Springer-Verlag,
London-Limited, 2001. — 326 p.
33. C l a r k e E . M . , G r u m b e r g J r . O . , P e l e d D . Model Checking. The MIT Press: Cambridge,
Massachusetts; London, England, 2001. — 356 p.
34. P e n c z e k W . , P o' l r o l a A . Advanced in verification on time Petri nets and timed automata.
Berlin Heidelberg: Springer-Verlag, 2006. — 258 p.
35. Ã î ä ë å â ñ ê è é À . Á . , Ê ð è â î é Ñ . Ë . Î ïðîåêòèðîâàíèè ýôôåêòèâíûõ àëãîðèòìîâ ïðè-
âåäåíèÿ àâòîìàòîâ äëÿ íåêîòîðûõ îòíîøåíèé ýêâèâàëåíòíîñòè // Êèáåðíåòèêà è ñèñòåìíûé
àíàëèç. — 1989. — ¹ 6. — C. 54–61.
36. P r o c . of Conf. “Language and automata theory and applications” // LNCS. — 2009. — 5457. —
765 p.
Ïîñòóïèëà 04.11.2010
20 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 5
|