Проверка эквивалентности программ с помощью двухленточных автоматов
Семантика послідовних програм визначається на основі моделей динамічної логіки. Якщо динамічна шкала ациклічна, її можна описати двострічковим детермінованим автоматом. У такому разі перевірки еквівалентності програм, семантика операторів яких визначається ациклічними динамічними шкалами, зводиться...
Gespeichert in:
| Veröffentlicht in: | Кибернетика и системный анализ |
|---|---|
| Datum: | 2010 |
| 1. Verfasser: | |
| Format: | Artikel |
| Sprache: | Russian |
| Veröffentlicht: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2010
|
| Schlagworte: | |
| Online Zugang: | https://nasplib.isofts.kiev.ua/handle/123456789/45242 |
| 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: | Проверка эквивалентности программ с помощью двухленточных автоматов / В.А. Захаров // Кибернетика и системный анализ. — 2010. — № 4. — С. 39-48. — Бібліогр.: 44 назв. — рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
nasplib_isofts_kiev_ua-123456789-45242 |
|---|---|
| record_format |
dspace |
| spelling |
Захаров, В.А. 2013-06-10T16:19:33Z 2013-06-10T16:19:33Z 2010 Проверка эквивалентности программ с помощью двухленточных автоматов / В.А. Захаров // Кибернетика и системный анализ. — 2010. — № 4. — С. 39-48. — Бібліогр.: 44 назв. — рос. 0023-1274 https://nasplib.isofts.kiev.ua/handle/123456789/45242 519.71 Семантика послідовних програм визначається на основі моделей динамічної логіки. Якщо динамічна шкала ациклічна, її можна описати двострічковим детермінованим автоматом. У такому разі перевірки еквівалентності програм, семантика операторів яких визначається ациклічними динамічними шкалами, зводиться до задачі перевірки порожнистості двострічкових автоматів (комбінованих машин). This paper shows how two-tape automata can be employed to design efficient equivalence checking procedures for sequential programs. The semantics of sequential programs is defined in terms of dynamic logic structures. If the dynamic frame is acyclic (i.e., all program statements are irreversible), it can be specified by means of a two-tape deterministic automaton. Then the equivalence checking problem for sequential programs operating on the dynamic frame can be reduced to the emptiness problem for two-tape automata (compound machine). ru Інститут кібернетики ім. В.М. Глушкова НАН України Кибернетика и системный анализ Кибернетика Проверка эквивалентности программ с помощью двухленточных автоматов Перевірка еквівалентності програм за допомогою двострічкових автоматів Program equivalence checking by two-tape automata 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 |
2010 |
| language |
Russian |
| container_title |
Кибернетика и системный анализ |
| publisher |
Інститут кібернетики ім. В.М. Глушкова НАН України |
| format |
Article |
| title_alt |
Перевірка еквівалентності програм за допомогою двострічкових автоматів Program equivalence checking by two-tape automata |
| description |
Семантика послідовних програм визначається на основі моделей динамічної логіки. Якщо динамічна шкала ациклічна, її можна описати двострічковим детермінованим автоматом. У такому разі перевірки еквівалентності програм, семантика операторів яких визначається ациклічними динамічними шкалами, зводиться до задачі перевірки порожнистості двострічкових автоматів (комбінованих машин).
This paper shows how two-tape automata can be employed to design efficient equivalence checking procedures for sequential programs. The semantics of sequential programs is defined in terms of dynamic logic structures. If the dynamic frame is acyclic (i.e., all program statements are irreversible), it can be specified by means of a two-tape deterministic automaton. Then the equivalence checking problem for sequential programs operating on the dynamic frame can be reduced to the emptiness problem for two-tape automata (compound machine).
|
| issn |
0023-1274 |
| url |
https://nasplib.isofts.kiev.ua/handle/123456789/45242 |
| citation_txt |
Проверка эквивалентности программ с помощью двухленточных автоматов / В.А. Захаров // Кибернетика и системный анализ. — 2010. — № 4. — С. 39-48. — Бібліогр.: 44 назв. — рос. |
| work_keys_str_mv |
AT zaharovva proverkaékvivalentnostiprogrammspomoŝʹûdvuhlentočnyhavtomatov AT zaharovva perevírkaekvívalentnostíprogramzadopomogoûdvostríčkovihavtomatív AT zaharovva programequivalencecheckingbytwotapeautomata |
| first_indexed |
2025-11-27T06:25:54Z |
| last_indexed |
2025-11-27T06:25:54Z |
| _version_ |
1850804848006529024 |
| fulltext |
ÓÄÊ 519.71
Â.À. ÇÀÕÀÐÎÂ
ÏÐÎÂÅÐÊÀ ÝÊÂÈÂÀËÅÍÒÍÎÑÒÈ ÏÐÎÃÐÀÌÌ
Ñ ÏÎÌÎÙÜÞ ÄÂÓÕËÅÍÒÎ×ÍÛÕ ÀÂÒÎÌÀÒÎÂ
Êëþ÷åâûå ñëîâà: ïðîãðàììà, ýêâèâàëåíòíîñòü, àëãîðèòìè÷åñêàÿ ðàçðåøè-
ìîñòü, ìíîãîëåíòî÷íûé àâòîìàò, âû÷èñëèòåëüíàÿ ñëîæíîñòü.
ÂÂÅÄÅÍÈÅ
Ïðîáëåìà ýêâèâàëåíòíîñòè ïðîãðàìì ñîñòîèò â òîì, ÷òîáû äëÿ ïðîèçâîëüíîé
ïàðû ïðîãðàìì âûÿñíèòü, èìåþò ëè îíè îäèíàêîâîå ïîâåäåíèå. Ïîâåäåíèå ïðî-
ãðàìì ìîæåò îïðåäåëÿòüñÿ â çàâèñèìîñòè îò èññëåäóåìîãî êëàññà ïðîãðàìì.
 ÷àñòíîñòè, ïîâåäåíèå âû÷èñëèòåëüíîé ïðîãðàììû ìîæåò áûòü îõàðàêòåðèçîâà-
íî ôóíêöèåé ïðåîáðàçîâàíèÿ âõîäíûõ äàííûõ ïðîãðàììû â âûõîäíûå äàííûå.
 ýòîì ñëó÷àå ïðîãðàììû ñ÷èòàþòñÿ ýêâèâàëåíòíûìè, åñëè îíè âû÷èñëÿþò îäíó
è òó æå ôóíêöèþ. Ïðîáëåìà ôóíêöèîíàëüíîé ýêâèâàëåíòíîñòè ïðîãðàìì âîçíè-
êàåò âî ìíîãèõ çàäà÷àõ ñèñòåìíîãî è ïðèêëàäíîãî ïðîãðàììèðîâàíèÿ. Ê ñîæàëå-
íèþ, â óíèâåðñàëüíûõ ñèñòåìàõ ïðîãðàììèðîâàíèÿ ýòà ïðîáëåìà àëãîðèòìè÷åñ-
êè íåðàçðåøèìà. Ïîýòîìó äëÿ ïîëó÷åíèÿ ýôôåêòèâíî ïðîâåðÿåìûõ äîñòàòî÷íûõ
óñëîâèé ôóíêöèîíàëüíîé ýêâèâàëåíòíîñòè ïðîãðàìì ïðèõîäèòñÿ îáðàùàòüñÿ ê
àáñòðàêòíûì ìîäåëÿì ïðîãðàìì. Èíòåðåñ ïðåäñòàâëÿþò òàêèå ìîäåëè ïðîãðàìì,
â êîòîðûõ ðàçðåøèìîå îòíîøåíèå ýêâèâàëåíòíîñòè ïðîãðàìì àïïðîêñèìèðóåò
îòíîøåíèå ôóíêöèîíàëüíîé ýêâèâàëåíòíîñòè.
Íà÷èíàÿ ñ îñíîâîïîëàãàþùèõ ðàáîò [1, 2], áûë ïðåäëîæåí øèðîêèé ñïåêòð
ôîðìàëüíûõ ìîäåëåé ïðîãðàìì, îðèåíòèðîâàííûõ íà èçó÷åíèå ïðîáëåìû ôóíêöèî-
íàëüíîé ýêâèâàëåíòíîñòè, — ñòàíäàðòíûå ñõåìû ïðîãðàìì [2, 3], äèñêðåòíûå ïðå-
îáðàçîâàòåëè [5, 6], ñõåìû ðåêóðñèâíûõ ïðîãðàìì [7], àëãåáðàè÷åñêèå ìîäåëè ïðî-
ãðàìì [8] è äð. Íà îñíîâå ýòèõ ìîäåëåé â 60–70-å ãîäû ïðîøëîãî âåêà áûëà ïðåä-
ïðèíÿòà ïîïûòêà ðàçðàáîòàòü ìàòåìàòè÷åñêèå ìåòîäû îïòèìèçàöèè êîìïüþòåðíûõ
ïðîãðàìì è ìèêðîïðîöåññîðîâ [9]. Íà ïåðâîì ýòàïå èññëåäîâàíèé ïëàíèðîâàëîñü
âûäåëèòü ìîäåëè ïðîãðàìì ñ ðàçðåøèìîé ïðîáëåìîé ýêâèâàëåíòíîñòè. Èçó÷åíèå
ýòîé çàäà÷è ïðîâîäèëîñü äîñòàòî÷íî èíòåíñèâíî. Áûëî óñòàíîâëåíî, ÷òî âî âñåõ
óêàçàííûõ ìîäåëÿõ ïðîãðàìì ïðîáëåìà ýêâèâàëåíòíîñòè â îáùåì ñëó÷àå ÿâëÿåòñÿ
àëãîðèòìè÷åñêè íåðàçðåøèìîé [3, 8, 10, 11]. Áûëè òàêæå âûäåëåíû ìíîãî÷èñëåí-
íûå è îáøèðíûå êëàññû ïðîãðàìì, â êîòîðûõ ïðîáëåìà ýêâèâàëåíòíîñòè îêàçàëàñü
ðàçðåøèìîé (íàïðèìåð, [6, 12–24]). Ïîäðîáíûé îáçîð è àíàëèç áîëüøèíñòâà
óêàçàííûõ ðåçóëüòàòîâ ìîæíî íàéòè â ìîíîãðàôèè [25].
Äëÿ ðåøåíèÿ ïðîáëåìû ýêâèâàëåíòíîñòè ïðîãðàìì áûë ïðåäëîæåí ðÿä îðèãè-
íàëüíûõ ïîäõîäîâ: ìåòîä ñåòåâîé ðàçìåòêè äëÿ ñòàíäàðòíûõ ñõåì [21, 22], ìåòîä
óñòðàíåíèÿ íåñóùåñòâåííûõ âåòâëåíèé [4, 14], ìåòîä æåñòêèõ ìíîæåñòâ [26], ìåòîä
ïàðàëëåëüíîãî ñòåêèíãà [23, 27]. Êðîìå òîãî, áûëî óñòàíîâëåíî, ÷òî ðàçðåøàþùèå
ïðîöåäóðû, ñîçäàííûå íà îñíîâå ýòèõ ìåòîäîâ, èìåþò ÷ðåçâû÷àéíî âûñîêóþ âû-
÷èñëèòåëüíóþ ñëîæíîñòü è íåïðèãîäíû äëÿ ïðàêòè÷åñêîãî èñïîëüçîâàíèÿ. Ïî ìíå-
íèþ àâòîðà íàñòîÿùåé ñòàòüè, îäíèì èç âîçìîæíûõ îáúÿñíåíèé ýòîìó ÿâëåíèþ
ìîãëî áûòü æåëàíèå èññëåäîâàòåëåé äîáèòüñÿ êàê ìîæíî áîëüøåé óíèâåðñàëüíîñòè
ïðåäëîæåííûõ èìè ïîäõîäîâ ê ïðîâåðêå ýêâèâàëåíòíîñòè ïðîãðàìì. Ïî ìåðå òîãî,
êàê ðàñøèðÿëñÿ êëàññ ïðîãðàìì, ê êîòîðûì ýòîò ìåòîä ìîã áûòü ïðèìåíåí, è ñî-
âåðøåíñòâîâàëàñü ðàçðåøàþùàÿ ïðîöåäóðà, îíà ñòàíîâèëàñü âñå ìåíåå ÷óâñòâè-
òåëüíîé ê ñïåöèôè÷åñêèì îñîáåííîñòÿì àíàëèçèðóåìûõ ïðîãðàìì.  ðåçóëüòàòå
îäíè è òå æå ñðåäñòâà ïðèìåíÿëèñü êàê äëÿ ñëîæíûõ, òàê è ïðîñòûõ ñëó÷àåâ ïðè
ðàçðåøåíèè ïðîáëåìû ýêâèâàëåíòíîñòè ïðîãðàìì, è ýòî çà÷àñòóþ ïðèâîäèëî ê íå-
îïðàâäàííî áîëüøèì âû÷èñëèòåëüíûì çàòðàòàì. Íåîáõîäèìîñòü â ñîçäàíèè ïðàê-
òè÷íûõ è áûñòðûõ (ïîëèíîìèàëüíûõ ïî âðåìåíè) àëãîðèòìîâ ïðîâåðêè ýêâèâà-
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4 39
© Â.À. Çàõàðîâ, 2010
ëåíòíîñòè ïðîãðàìì, ó÷èòûâàþùèõ â áîëüøåé ìåðå èíäèâèäóàëüíûå àëãåáðàè÷åñ-
êèå ñâîéñòâà áàçîâûõ êîìïîíåíòîâ ïðîãðàììû, îòìå÷àëàñü â ðÿäå ðàáîò [9, 28].
Ñóùåñòâåííûì ïðîäâèæåíèåì â ïîñòðîåíèè áûñòðûõ àëãîðèòìîâ ïðîâåðêè ýê-
âèâàëåíòíîñòè ïðîãðàìì ñòàëà ñòàòüÿ [29], â êîòîðîé äîêàçàíà ðàçðåøèìîñòü çà ïî-
ëèíîìèàëüíîå âðåìÿ ïðîáëåìû ýêâèâàëåíòíîñòè ïðîãðàìì ñ êîììóòàòèâíûìè îïå-
ðàòîðàìè (cóùåñòâîâàíèå ðàçðåøàþùåãî àëãîðèòìà â ýòîé ìîäåëè ïðîãðàìì áûëî
óñòàíîâëåíî ðàíåå â ñòàòüÿõ [6, 13]). Ýòè ðåçóëüòàòû ïðèâåëè ê ðàçðàáîòêå íîâîãî
ìåòîäà [30–32], ïîçâîëÿþùåãî ñîçäàâàòü ïîëèíîìèàëüíûå ïî âðåìåíè àëãîðèòìû
ïðîâåðêè ýêâèâàëåíòíîñòè ïîñëåäîâàòåëüíûõ ïðîãðàìì, ñåìàíòèêà îïåðàòîðîâ êî-
òîðûõ óäîâëåòâîðÿåò îïðåäåëåííûì àëãåáðàè÷åñêèì ñîîòíîøåíèÿì. Ïðåäëîæåí-
íûé ìåòîä áûë ðàñïðîñòðàíåí è íà äðóãèå ìîäåëè ïðîãðàìì [33–37]. Êðîìå òîãî,
â ñòàòüÿõ [38, 39] ñ ïîìîùüþ ìåòîäà ñëåäîâ óäàëîñü ïîñòðîèòü ðàçðåøàþùèå àëãî-
ðèòìû (â òîì ÷èñëå ïîëèíîìèàëüíîé ñëîæíîñòè) â îäíîì êëàññå àëãåáðàè÷åñêèõ
ìîäåëåé ïðîãðàìì, îáëàäàþùèõ ñëåäóþùåé õàðàêòåðíîé îñîáåííîñòüþ: ëþáûå
äâå êîíå÷íûå ýêâèâàëåíòíûå ïîñëåäîâàòåëüíîñòè ïðîãðàììíûõ îïåðàòîðîâ èìåþò
îäèíàêîâóþ äëèíó. Áûëè îáíàðóæåíû òàêæå ïðîñòûå ìîäåëè ïðîãðàìì, â êîòîðûõ
çàäà÷à ïðîâåðêè ýêâèâàëåíòíîñòè ïðîãðàìì (â êîíå÷íîì àëôàâèòå îïåðàòîðîâ
è ïðåäèêàòîâ) ÿâëÿåòñÿ PSPACE-ïîëíîé [40].
Ïîëó÷åííûå ðåçóëüòàòû ïîñëóæèëè ïðåäïîñûëêîé äëÿ áîëåå ãëóáîêîãî èññëåäî-
âàíèÿ ñëîæíîñòíûõ àñïåêòîâ ïðîáëåìû ýêâèâàëåíòíîñòè ïðîãðàìì. Â ðåçóëüòàòå áûë
ïðåäëîæåí íîâûé ñïîñîá îïèñàíèÿ ñåìàíòèê ïðîïîçèöèîíàëüíûõ ìîäåëåé ïîñëåäîâà-
òåëüíûõ ïðîãðàìì ñ èñïîëüçîâàíèåì äâóõëåíòî÷íûõ àâòîìàòîâ è íà åãî îñíîâå ñîçäàí
îáùèé ìåòîä ðåøåíèÿ ïðîáëåìû ýêâèâàëåíòíîñòè ïðîãðàìì ïóòåì åå ñâåäåíèÿ ê çàäà-
÷å ïðîâåðêè ïóñòîòû äëÿ äâóõëåíòî÷íûõ àâòîìàòîâ, à òàêæå óñòàíîâëåíû äîñòàòî÷íûå
óñëîâèÿ ðàçðåøèìîñòè ýòîé çàäà÷è çà ïîëèíîìèàëüíîå âðåìÿ.
 íàñòîÿùåé ñòàòüå ïîêàçàíî, êàêèì îáðàçîì äâóõëåíòî÷íûå àâòîìàòû ìîæíî
ïðèìåíÿòü äëÿ îïèñàíèÿ ñåìàíòèê íåêîòîðûõ ïðîïîçèöèîíàëüíûõ ìîäåëåé ïîñëå-
äîâàòåëüíûõ ïðîãðàìì, à òàêæå äëÿ ïðîåêòèðîâàíèÿ ïðîöåäóð ïðîâåðêè ýêâèâà-
ëåíòíîñòè ïðîãðàìì â ýòèõ ìîäåëÿõ.
ÏÐÎÏÎÇÈÖÈÎÍÀËÜÍÀß ÌÎÄÅËÜ ÏÐÎÃÐÀÌÌ
Îïðåäåëèì ñèíòàêñèñ è ñåìàíòèêó ðàññìàòðèâàåìîãî êëàññà ïðîãðàìì. Ïóñòü çà-
äàíû äâà êîíå÷íûõ àëôàâèòà: A a ar� � �{ }1 � è P p pk� � �{ }1 � . Ýëåìåíòû ìíî-
æåñòâà àëôàâèòà A íàçûâàþòñÿ îïåðàòîðàìè. Îíè ñîîòâåòñòâóþò ïðîãðàììíûì
êîìàíäàì. Êîíå÷íóþ ïîñëåäîâàòåëüíîñòü îïåðàòîðîâ áóäåì íàçûâàòü A-öåïî÷-
êîé. Ìíîæåñòâî âñåõ A-öåïî÷åê îáîçíà÷èì A * . Ïóñòóþ A-öåïî÷êó îáîçíà-
÷èì � ; çàïèñü h h1 2 áóäåò îáîçíà÷àòü êîíêàòåíàöèþ A-öåïî÷åê h1 è h2 . Ýëåìåí-
òàìè ìíîæåñòâà P ÿâëÿþòñÿ ïðåäèêàòû. Â ëþáîì ñîñòîÿíèè äàííûõ êàæäûé
ïðåäèêàò ìîæåò ïðèíèìàòü îäíî èç äâóõ çíà÷åíèé: 0 èëè 1. Äâîè÷íûå íàáîðû
� � � �� �1 � k çíà÷åíèé ïðåäèêàòîâ íàçîâåì óñëîâèÿìè. Ìíîæåñòâî âñåõ óñëîâèé
îáîçíà÷èì C ; óñëîâèÿ èç C áóäåì îáîçíà÷àòü �1 , �2 , ...
Ïðîãðàììà ïðåäñòàâëÿåòñÿ êîíå÷íîé ðàçìå÷åííîé ñèñòåìîé ïåðåõîäîâ
� � � �V entry exit T B, , , , , â êîòîðîé V — íåïóñòîå êîíå÷íîå ìíîæåñòâî òî÷åê ïðî-
ãðàììû, entry — òî÷êà âõîäà, exit — òî÷êà âûõîäà, T V exit C V: ( \ ){ } � � — ôóíêöèÿ
ïåðåõîäîâ, B V exit A: ( \ ){ } � — ôóíêöèÿ ïðèâÿçêè. Ôóíêöèÿ ïåðåõîäîâ çàäàåò ïî-
òîê óïðàâëåíèÿ ïðîãðàììû, à ôóíêöèÿ ïðèâÿçêè àññîöèèðóåò îïåðàòîð ñ êàæäîé
òî÷êîé ïðîãðàììû, îòëè÷íîé îò òî÷êè âûõîäà. Ðàçìåð | |� ïðîãðàììû � — ýòî
êîëè÷åñòâî òî÷åê ïðîãðàììû.
Òðàññîé â ïðîãðàììå � íàçûâàåòñÿ ëþáàÿ ïîñëåäîâàòåëüíîñòü ïàð tr v� ( , )1 1� ,
( , )v2 2� , ... , óäîâëåòâîðÿþùàÿ äëÿ êàæäîãî i i, 1, ñîîòíîøåíèÿì v Vi
, �i C
è
v T vi i i� �1 ( , )� . Åñëè v entry1 � , òî òðàññà tr íàçûâàåòñÿ íà÷àëüíîé. Åñëè íà÷àëüíàÿ
òðàññà áåñêîíå÷íà èëè çàâåðøàåòñÿ òàêîé ïàðîé ( , )vn n� , ÷òî T v exitn n( , )� � , òî
òðàññà íàçûâàåòñÿ ïîëíîé. Äëÿ êîíå÷íîé òðàññû tr çàïèñü tri áóäåò îáîçíà÷àòü ïðå-
ôèêñ tr äëèíû i, à B tr( ) áóäåò îáîçíà÷àòü A-öåïî÷êó B v B v B vn( ), ( ), ... , ( )1 2 îïåðà-
òîðîâ, ïðèïèñàííûõ òî÷êàì ýòîé òðàññû. Òî÷êà v ïðîãðàììû � íàçûâàåòñÿ ìåðòâîé,
åñëè îíà íå ñîäåðæèòñÿ íè â îäíîé ïîëíîé òðàññå ýòîé ïðîãðàììû.
40 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4
Ñåìàíòèêà ïðîãðàìì îïðåäåëÿåòñÿ íà îñíîâå ìîäåëåé Êðèïêå, èñïîëüçóåìûõ
â ïðîïîçèöèîíàëüíûõ äèíàìè÷åñêèõ ëîãèêàõ ïðîãðàìì [41]. Äèíàìè÷åñêîé øêàëîé
íàçûâàåòñÿ òðîéêà F S s R� � �, ,0 , â êîòîðîé S — íåïóñòîå ìíîæåñòâî ñîñòîÿíèé äàí-
íûõ, s0 — íà÷àëüíîå ñîñòîÿíèå (s S0
) è R S A S: � � — èíòåðïðåòàöèÿ îïåðàòîðîâ,
âû÷èñëÿþùàÿ òî ñîñòîÿíèå äàííûõ R s a( , ) , â êîòîðîå îïåðàòîð a ïðåîáðàçóåò ñîñòî-
ÿíèå äàííûõ s . Ôóíêöèþ R ìîæíî ðàñïðîñòðàíèòü íà ìíîæåñòâî îïåðàòîðíûõ
öåïî÷åê, ââåäÿ ôóíêöèþ R * , óäîâëåòâîðÿþùóþ ñîîòíîøåíèÿì R s s* ( , )� � ,
R s ha R R s h a* *( , ) ( ( , ), )� . Ñîñòîÿíèå äàííûõ ��s íàçûâàåòñÿ äîñòèæèìûì èç ñîñòîÿ-
íèÿ s� (îáîçíà÷àåòñÿ s sF� ��� ), åñëè �� � �s R s h( , ) äëÿ íåêîòîðîé öåïî÷êè h A
* .
Åñëè îòíîøåíèå äîñòèæèìîñòè � F ÿâëÿåòñÿ îòíîøåíèåì ÷àñòè÷íîãî ïîðÿäêà íà S ,
òî øêàëà F íàçûâàåòñÿ óïîðÿäî÷åííîé. Çàïèñü [ ]h F èñïîëüçóåòñÿ äëÿ îáîçíà÷åíèÿ
ñîñòîÿíèÿ äàííûõ R s h* ( , )0 .
Äèíàìè÷åñêàÿ ìîäåëü Êðèïêå — ýòî ïàðà M F� ( , )� , ãäå F — øêàëà Êðèï-
êå, à �:S C� — îöåíêà (èñòèííîñòè ïðåäèêàòîâ). Ìîäåëü Êðèïêå âèäà ( , )F � áóäåì
íàçûâàòü F-ìîäåëüþ. Âû÷èñëåíèåì ïðîãðàììû � � � �V entry exit T B, , , , íà äèíàìè-
÷åñêîé ìîäåëè Êðèïêå M F� ( , )� íàçûâàåòñÿ ìàêñèìàëüíàÿ ïîñëåäîâàòåëüíîñòü ïàð
comp M v s v s( , ) ( , ), ( , )� � 0 0 1 1 , … , ( , )v si i , ( , )v si i� �1 1 , …,
óäîâëåòâîðÿþùàÿ ñëåäóþùèì óñëîâèÿì:
1) s0 — íà÷àëüíîå ñîñòîÿíèå øêàëû F è v entry0 � ;
2) v T v si i i� �1 ( , ( ))� è s R s B vi i i� �1 ( , ( )) äëÿ âñåõ i , i 0 .
Åñëè âû÷èñëåíèå ÿâëÿåòñÿ áåñêîíå÷íûì, òî ñ÷èòàåòñÿ, ÷òî îíî áåçðåçóëüòàòíî
çàöèêëèâàåòñÿ.  ïðîòèâíîì ñëó÷àå ïîñëåäîâàòåëüíîñòü comp M( , )� îêàí÷èâàåòñÿ
ïàðîé ( , )exit sn , è òîãäà âû÷èñëåíèå çàâåðøàåòñÿ ñ ðåçóëüòàòîì sn . Çàïèñü
[ ( , )]comp M� áóäåò îáîçíà÷àòü ðåçóëüòàò ýòîãî âû÷èñëåíèÿ. Åñëè âû÷èñëåíèå çà-
öèêëèâàåòñÿ, òî åãî ðåçóëüòàò ñ÷èòàåòñÿ íåîïðåäåëåííûì. Î÷åâèäíî, ÷òî êàæäîå
âû÷èñëåíèå comp M( , )� íà ìîäåëè M ïðîêëàäûâàåò â ïðîãðàììå � ïîëíóþ òðàññó
tr M v s v s v si i( , ) ( , ( )), ( , ( )),... , ( , ( ))� � � �� 0 0 1 1 , …
Åñëè âû÷èñëåíèå comp M( , )� çàâåðøàåòñÿ, òî [ ( , )] [ ( ( , ))]comp M B tr M� �� .
Ïðîãðàììû �� è ��� íàçûâàþòñÿ ýêâèâàëåíòíûìè íà øêàëå F (� ��
��F ), åñëè ðàâåí-
ñòâî [ ( , )] [ ( , )]comp M comp M� �� � �� âûïîëíÿåòñÿ äëÿ ëþáîé F-ìîäåëè M. Ïðîáëåìà
ýêâèâàëåíòíîñòè ïðîãðàìì íà äèíàìè÷åñêîé øêàëå F ñîñòîèò â òîì, ÷òîáû äëÿ ïðîèç-
âîëüíîé ïàðû ïðîãðàìì �� , ��� ïðîâåðèòü âûïîëíèìîñòü îòíîøåíèÿ � ��
��F .
ÄÂÓÕËÅÍÒÎ×ÍÛÅ ÌÀØÈÍÛ
Äëÿ èññëåäîâàíèÿ àëãîðèòìè÷åñêîé ðàçðåøèìîñòè è ñëîæíîñòè ïðîáëåìû ýêâè-
âàëåíòíîñòè ïðîãðàìì íåîáõîäèìî ðàññìîòðåòü ýôôåêòèâíûé ñïîñîá îïèñàíèÿ
äèíàìè÷åñêèõ øêàë. Êàæäàÿ øêàëà F èíäóöèðóåò îòíîøåíèå ýêâèâàëåíòíîñòè íà
ìíîæåñòâå A * : öåïî÷êè h1 è h2 ñ÷èòàþòñÿ ýêâèâàëåíòíûìè íà øêàëå F, åñëè
[ ] [ ]h hF F1 2� . Èçâåñòíî [42], ÷òî îòíîøåíèÿ íà ìíîæåñòâå êîíå÷íûõ ñëîâ ìîæ-
íî çàäàâàòü ìíîãîëåíòî÷íûìè àâòîìàòàìè ïîäîáíî òîìó, êàê ÿçûêè çàäàþòñÿ c
ïîìîùüþ îäíîëåíòî÷íûõ àâòîìàòîâ.  ÷àñòíîñòè, íåêîòîðûå îòíîøåíèÿ ýêâèâà-
ëåíòíîñòè íà ìíîæåñòâå êîíå÷íûõ ñëîâ ìîæíî çàäàâàòü ñ ïîìîùüþ äâóõëåíòî÷-
íûõ àâòîìàòîâ. Ïîýòîìó äëÿ îïèñàíèÿ íåêîòîðûõ êëàññîâ äèíàìè÷åñêèõ øêàë
öåëåñîîáðàçíî âîñïîëüçîâàòüñÿ äâóõëåíòî÷íûìè äåòåðìèíèðîâàííûìè àâòîìàòà-
ìè (ìàøèíàìè).
Äâóõëåíòî÷íîé äåòåðìèíèðîâàííîé ìàøèíîé (2-DM) íàçûâàåòñÿ ñèñòåìà
D Q Q q Qaccept� � ��, , , , ,1 2 0 � , ñîñòîÿùàÿ èç âõîäíîãî àëôàâèòà � , äâóõ íåïåðåñåêà-
þùèõñÿ ìíîæåñòâ âíóòðåííèõ ñîñòîÿíèé: Q1 è Q2 , íà÷àëüíîãî ñîñòîÿíèÿ
q q Q Q0 0 1 2,
� , ìíîæåñòâà äîïóñêàþùèõ ñîñòîÿíèé Qaccept , Q Q Qaccept � �1 2 ,
è ôóíêöèè ïåðåõîäîâ � : ( )Q Q Q Q1 2 1 2� � � �� . Ìàøèíà D ïðî÷èòûâàåò ïàðó
ñëîâ w1 è w2 , çàïèñàííûõ íà ëåíòàõ 1 è 2. Êîãäà ìàøèíà D ïðåáûâàåò âî âíóòðåí-
íåì ñîñòîÿíèè q q Q,
� , �
{ }1 2, , îíà ïðî÷èòûâàåò î÷åðåäíóþ áóêâó x (åñëè òàêî-
âàÿ åñòü) ñëîâà w� , ðàçìåùåííîãî íà ëåíòå � , è ïåðåõîäèò â ñîñòîÿíèå q q x� � �( , ) .
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4 41
Ïàðà ñëîâ � �w w1 2, äîïóñêàåòñÿ ìàøèíîé D, åñëè îíà ïðî÷èòûâàåò îáà ñëîâà w1 è
w2 è îêàçûâàåòñÿ ïî ïðî÷òåíèè ýòèõ ñëîâ â äîïóñêàþùåì ñîñòîÿíèè. Áîëåå
ôîðìàëüíî ïîâåäåíèå ìàøèíû D îïðåäåëÿåòñÿ ñëåäóþùèì îáðàçîì.
Ïðîãîíîì 2-DM D íàçûâàåòñÿ êîíå÷íàÿ èëè áåñêîíå÷íàÿ ïîñëåäîâàòåëüíîñòü
ïàð � � ( , ), ( , ), ... , ( , )q x q x q xi i1 1 2 2 , … , xi
� , óäîâëåòâîðÿþùàÿ ñîîòíîøåíèÿì
q Q Qi
�1 2 è q q xi i i� �1 �( , ) äëÿ âñåõ i , i 1. Åñëè ýòà ïîñëåäîâàòåëüíîñòü îêàí-
÷èâàåòñÿ ïàðîé ( , )q xn n , òî ñ÷èòàþò, ÷òî ïðîãîí � íà÷èíàåòñÿ â ñîñòîÿíèè q1 è äî-
ñòèãàåò ñîñòîÿíèÿ q q xn n� �1 �( , ) . Äëÿ �
{ }1 2, ðàññìîòðèì ïîäïîñëåäîâàòåëüíîñòü
�� � ( , ), ( , ),...q x q xi i i i1 1 2 2
, ñîñòîÿùóþ èç âñåõ òåõ ïàð ( , )q xi ij j
ïîñëåäîâàòåëüíî-
ñòè � , êîòîðûå óäîâëåòâîðÿþò óñëîâèþ q Qij
� . Òîãäà �-ïðîåêöèåé ïðîãîíà �
áóäåì íàçûâàòü ñëîâî � �[ ] � x xi i1 2
... Ôóíêöèþ ïåðåõîäîâ 2-DM D ìîæíî ðàñïðî-
ñòðàíèòü íà ìíîæåñòâî ïàð ñëîâ � �* *� ñëåäóþùèì îáðàçîì: �* ( , , )q w w q1 2 � � ,
åñëè ñóùåñòâóåò ïðîãîí � ìàøèíû D, êîòîðûé íà÷èíàåòñÿ â ñîñòîÿíèè q, äîñòèãàåò
ñîñòîÿíèÿ �q , ïðè ýòîì �[ ]1 1� w , �[ ]2 2� w .  ïðîòèâíîì ñëó÷àå çíà÷åíèå
�* ( , , )q w w1 2 íå îïðåäåëåíî. Êàæäàÿ 2-DM D Q Q q Qaccept� � ��, , , , ,1 2 0 � ïîðîæäàåò
áèíàðíîå îòíîøåíèå E w w q w w QD accept� � �
{ }1 2 0 1 2, : * ( , , )� . Áóäåì ãîâîðèòü, ÷òî
2-DM D îïèñûâàåò øêàëó F, åñëè äëÿ ëþáîé ïàðû A *-öåïî÷åê h1 è h2 èìååò ìåñòî
ñîîòíîøåíèå [ ] [ ] ,h h h h EF F D1 2 1 2� � � �
.
Òåîðåìà 1. Äèíàìè÷åñêàÿ øêàëà F ìîæåò áûòü îïèñàíà íåêîòîðîé 2-DM òîãäà
è òîëüêî òîãäà, êîãäà F óïîðÿäî÷åíà.
Äîêàçàòåëüñòâî. (�) Äëÿ ëþáîé øêàëû F îòíîøåíèå äîñòèæèìîñòè � F ðåô-
ëåêñèâíî è òðàíçèòèâíî. Åñëè áû îíî íå áûëî àíòèñèììåòðè÷íûì, òî ñóùåñòâîâà-
ëà áû òàêàÿ ïàðà A-öåïî÷åê h h� ��, , ÷òî �� �h �, [ ] [ ]h h hF F� �� � � . Ïîñêîëüêó øêàëó F
îïèñûâàåò 2-DM D, òî â ýòîì ñëó÷àå ñóùåñòâîâàëà áû ïàðà äîïóñêàþùèõ ñîñòîÿ-
íèé q q h h� � � ��* ( , , )0 è �� � � � ��q q h h h�* ( , , )0 . Íî ýòî îçíà÷àëî áû, ÷òî q Q�
2 è,
ñëåäîâàòåëüíî, çíà÷åíèå �* ( , , )q h h h1 � �� � íå îïðåäåëåíî âîïðåêè òîìó, ÷òî
[ ] [ ]h h hF F� �� � � .
(�) Äëÿ óïîðÿäî÷åííîé øêàëû F S s R� � �, ,0 ðàññìîòðèì 2-DM D A� � ,
Q1 , Q2 , q0 , Qaccept , ��, ãäå Q s s1 � � ��{( , ): s�, ��
s S , s sF� ��� }, Q2 � ( ) \S S Q� 1 ,
q s s0 0 0� ( , ) , Q s s s Saccept �
{ }( , ): è ôóíêöèÿ ïåðåõîäîâ îïðåäåëåíà ñîîòíîøåíèÿ-
ìè �(( , ), ) ( ( , ), )s s a R s a s� �� � � �� , åñëè ( , )s s Q� ��
1 , è �(( , ), )s s a� �� � ( , ( , ))s R s a� �� ,
åñëè ( , )s s Q� � �
2 . Äëÿ ëþáîé ïàðû A-öåïî÷åê h h1 2, ëèáî åñòü òàêîé ïðåôèêñ h�1
öåïî÷êè h1 , ÷òî �* ( , , )q h h0 1 2� îïðåäåëåíî, ëèáî åñòü òàêîé ïðåôèêñ h� 2 öåïî÷êè
h2 , ÷òî �* ( , , )q h h0 1 2� îïðåäåëåíî. Ïðåäïîëîæèì, ÷òî [ ] [ ]h hF F1 2� ,
h h a a ak1 1 1 2� � � è �* ( , , )q h h q0 1 2� � � . Îòíîøåíèå äîñòèæèìîñòè � F ÿâëÿåòñÿ
÷àñòè÷íûì ïîðÿäêîì, è ïîýòîìó [ ] [ ]h a a a hi F F F�1 1 2 2� � âûïîëíÿåòñÿ äëÿ âñåõ
i , 1� �i k . Ïðèìåíÿÿ èíäóêöèþ ïî i , ìîæíî óáåäèòüñÿ, ÷òî �* ( ,q h a a0 1 1 2� �
... , ) ([ ] ,[ ] )a h h a a a h Qi i F F2 1 1 2 2 1� �
� äëÿ âñåõ i i k, 1� � . Ïîýòîìó çíà÷åíèå
�* ( , , )q h h0 1 2 îïðåäåëåíî è ðàâíî ([ ] [ ] ),h hF F1 2 . Êàê âèäíî èç îïèñàíèÿ D, äîñ-
òèãíóòîå ñîñòîÿíèå �* ( , , )q h h0 1 2 ÿâëÿåòñÿ äîïóñêàþùèì. Òåîðåìà äîêàçàíà.
ÊÎÌÁÈÍÈÐÎÂÀÍÍÛÅ ÄÂÓÕËÅÍÒÎ×ÍÛÅ ÌÀØÈÍÛ
Öåëü íàñòîÿùåé ñòàòüè — ñîçäàíèå îáùåãî òåîðåòèêî-àâòîìàòíîãî ìåòîäà ïðî-
âåðêè ýêâèâàëåíòíîñòè ïðîãðàìì, ñåìàíòèêà îïåðàòîðîâ êîòîðûõ îïðåäåëÿåòñÿ
óïîðÿäî÷åííûìè äèíàìè÷åñêèìè øêàëàìè.  ðàìêàõ ýòîãî ïîäõîäà ïðîãðàììû
ìîæíî ðàññìàòðèâàòü êàê êîíå÷íûå àâòîìàòû, ïîðîæäàþùèå òðàññû. Ïîýòîìó
îòíîøåíèå ýêâèâàëåíòíîñòè ïðîãðàìì � ��
��F öåëåñîîáðàçíî îïðåäåëèòü â òåð-
ìèíàõ ïðîãðàììíûõ òðàññ.
Äëÿ çàäàííîé øêàëû F íà÷àëüíàÿ òðàññà tr v v� ( , ), ( , )1 1 2 2� � , ... â ïðîãðàììå �
íàçûâàåòñÿ F-íåïðîòèâîðå÷èâîé, åñëè äëÿ ëþáîé ïàðû i j, èç ðàâåíñòâà
� � � � �B tr B tri
F
j
F( ) ( ) ñëåäóåò � �i j� ��1 1 . Î÷åâèäíà ñïðàâåäëèâîñòü ñëåäóþ-
ùèõ óòâåðæäåíèé.
42 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4
Óòâåðæäåíèå 1. Òðàññà tr â ïðîãðàììå � ÿâëÿåòñÿ F-íåïðîòèâîðå÷èâîé òîãäà
è òîëüêî òîãäà, êîãäà îíà ÿâëÿåòñÿ ïðåôèêñîì òðàññû tr M( , )� äëÿ íåêîòîðîé F-ìî-
äåëè M.
Óòâåðæäåíèå 2. Øêàëà F ÿâëÿåòñÿ óïîðÿäî÷åííîé òîãäà è òîëüêî òîãäà, êîãäà
êàæäàÿ íà÷àëüíàÿ òðàññà â ëþáîé ïðîãðàììå ÿâëÿåòñÿ F-íåïðîòèâîðå÷èâîé.
Òàêèì îáðàçîì, F-íåïðîòèâîðå÷èâûå òðàññû — ýòî â òî÷íîñòè òå ïðîãðàì-
ìíûå òðàññû, êîòîðûå ïðîêëàäûâàþòñÿ âû÷èñëåíèÿìè íà F-ìîäåëÿõ.
F-íåïðîòèâîðå÷èâûå òðàññû tr v v1 1 1 2 2� � � � �( , ), ( , ),...� � è tr v2 1 1� �� ��( , )� ,
( , )�� ��v2 2� , ... â ïðîãðàììàõ �1 è � 2 íàçûâàþòñÿ F-ñîâìåñòíûìè, åñëè äëÿ ëþáîé
ïàðû i j, èç ðàâåíñòâà [ ( )] [ ( )]B tr B tri
F
j
F1 2
� ñëåäóåò � �� � ��� �i j1 1 .
Óòâåðæäåíèå 3. Òðàññû tr1 è tr2 â ïðîãðàììàõ �1 è � 2 ñîîòâåòñòâåííî ÿâëÿþò-
ñÿ F-ñîâìåñòíûìè òîãäà è òîëüêî òîãäà, êîãäà îíè ÿâëÿþòñÿ ïðåôèêñàìè òðàññ
tr M( , )�1 è tr M( , )� 2 äëÿ íåêîòîðîé F-ìîäåëè M.
Èç ýòèõ óòâåðæäåíèé ñëåäóåò òåîðåìà.
Òåîðåìà 2. Ïðîãðàììû �1 è � 2 íåýêâèâàëåíòíû íà øêàëå F òîãäà è òîëüêî
òîãäà, êîãäà â ýòèõ ïðîãðàììàõ ñóùåñòâóåò ïàðà F-ñîâìåñòíûõ ïîëíûõ òðàññ tr1 è
tr2 , óäîâëåòâîðÿþùèõ îäíîìó èç äâóõ óñëîâèé: ëèáî â òî÷íîñòè îäíà èç ýòèõ òðàññ
êîíå÷íà, ëèáî îáå òðàññû êîíå÷íû è ïðè ýòîì [ ( )] [ ( )]B tr B trF F1 1 2 2� .
Òåîðåòèêî-àâòîìàòíûé ïîäõîä ïðåäóñìàòðèâàåò ïðåäñòàâëåíèå àíàëèçèðóå-
ìûõ ïðîãðàìì è èõ ñïåöèôèêàöèé â âèäå êîíå÷íûõ àâòîìàòîâ (ñì. [43, 44]). Áëàãî-
äàðÿ ýòîìó âåðèôèêàöèÿ ïðîãðàììû ñâîäèòñÿ ê êîíñòðóèðîâàíèþ ðàçëè÷íûõ êîì-
ïîçèöèé àâòîìàòîâ è ïðîâåðêå èõ ñâîéñòâ. Äâóõëåíòî÷íûå ìàøèíû ìîæíî èñïîëü-
çîâàòü íå òîëüêî äëÿ îïèñàíèÿ äèíàìè÷åñêèõ øêàë, íî è äëÿ ðåøåíèÿ ñ èõ
ïîìîùüþ ïðîáëåìû ýêâèâàëåíòíîñòè ïðîãðàìì. Äëÿ çàäàííîé ïàðû ïðîãðàìì �1 è
� 2 , à òàêæå 2-DM D, îïèñûâàþùåé óïîðÿäî÷åííóþ øêàëó F, ñòðîèòñÿ êîìáèíèðî-
âàííàÿ 2-DM K D( , , )� �1 2 , ñîñòîÿùàÿ èç òðåõ âçàèìîäåéñòâóþùèõ êîìïîíåíòîâ:
�1 , � 2 è D. Íà âõîä ýòîé ìàøèíû ïîäàåòñÿ ïàðà êîíå÷íûõ ïîñëåäîâàòåëüíîñòåé
âèäà tr v v�
� � � �� ( , ), ( , )
1 1 2 2
� � , … , � � 1 2, . Êàæäàÿ êîìïîíåíòà � � ïðîâåðÿåò, ÿâëÿ-
åòñÿ ëè tr� òðàññîé â ïðîãðàììå � � . Êîìïîíåíòå D îòâîäèòñÿ ðîëü ñèíõðîíèçàòî-
ðà, ïîçâîëÿþùåãî ïðî÷èòûâàòü äî êîíöà òîëüêî ïàðû F-ñîâìåñòíûõ òðàññ tr1 è tr2 .
Êîìáèíèðîâàííàÿ 2-DM K D( , , )� �1 2 äîïóñêàåò òîëüêî òàêèå ïàðû F-ñîâìåñòíûõ
òðàññû â ïðîãðàììàõ �1 è � 2 , êîòîðûå óäîâëåòâîðÿþò òðåáîâàíèÿì òåîðåìû 2.
Òàêèì îáðàçîì, ñîîòíîøåíèå � �1 2
F áóäåò âûïîëíÿòüñÿ â òîì è òîëüêî òîì
ñëó÷àå, êîãäà êîìáèíèðîâàííàÿ 2-DM K D( , , )� �1 2 ïîðîæäàåò ïóñòîå áèíàðíîå
îòíîøåíèå.
Äàäèì ñòðîãîå îïðåäåëåíèå 2-DM K D( , , )� �1 2 . Ïóñòü çàäàíû ïðîãðàììû
� � � � �� � �V entry exit T B, , , , , � � 1 2, , è ìàøèíà D A Q Q q Qaccept� � �, , , , ,1 2 0 � ,
îïèñûâàþùàÿ óïîðÿäî÷åííóþ äèíàìè÷åñêóþ øêàëó F S s R� � �, ,0 . Ââåäåì âñïî-
ìîãàòåëüíûé ñèìâîë � , � �C. Òîãäà K D Q Q q Qaccept( , , ) � , � , � , � , � �,� � �1 2 1 2 0� � �� , ãäå
• � ( ) ( )� � � � �V C V C1 2 ,
• � ( )Q V V Q C� �� � � � � �1 2 { } , � � 1, 2 ,
• � ( , , , )q entry entry q0 0� � ,
• �� — ÷àñòè÷íàÿ ôóíêöèÿ ïåðåõîäîâ, çíà÷åíèÿ � ( , , , , ( , ))� � �v v q z v1 2 � êîòîðîé
â ñëó÷àå q Q
1 îïðåäåëÿþòñÿ ñëåäóþùèìè ñîîòíîøåíèÿìè:
� ( , , , , ( , )) ( , ), , ( , ( )),� �� �� � � ��v v q v T v v q B v1 2 1 1 2 1 1� � , åñëè v v� 1 , q F� è v1
íå ÿâëÿåòñÿ íè âûõîäîì exit, íè ìåðòâîé òî÷êîé;
� ( , , , , ( , )) ( , ), , ( , ( )),� �� �� � � �v v q v T v v q B v1 2 1 1 2 1 1� � � , åñëè v v� 1 , q F
è v1 íå
ÿâëÿåòñÿ íè âûõîäîì exit, íè ìåðòâîé òî÷êîé;
� ( , , , , ( , ))� � ��v v q v1 2 � íå îïðåäåëåíî âî âñåõ îñòàëüíûõ ñëó÷àÿõ;
� ( , , , , ( , )) ( , ), , ( , ( )),� �� � � � � ��v v q v T v v q B v1 2 1 1 2 1 1� � � , åñëè v v� 1 , q F� è v1
íå ÿâëÿåòñÿ íè âûõîäîì exit, íè ìåðòâîé òî÷êîé è � �� � ;
� ( , , , , ( , )) ( , ), , ( , ( )),� �� � � � � ��v v q v T v v q B v1 2 1 1 2 1 1� � � , åñëè v v� 1 , q F
, v1
íå ÿâëÿåòñÿ íè âûõîäîì exit, íè ìåðòâîé òî÷êîé è � �� � ;
� ( , , , , ( , ))� � ��v v q v1 2 � íå îïðåäåëåíî âî âñåõ îñòàëüíûõ ñëó÷àÿõ.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4 43
Ïðè q Q
2 çíà÷åíèå � ( , , , , ( , ))� � �v v q z v1 2 � îïðåäåëÿåòñÿ àíàëîãè÷íî.
Ìíîæåñòâî �Qaccept ñîñòîèò èç âñåõ ÷åòâåðîê � �v v q z1 2, , , , óäîâëåòâîðÿþùèõ
îäíîìó èç ñëåäóþùèõ òðåáîâàíèé:
1) v exit1 � , v exit2 � è q Qaccept� ;
2) v exiti � , v exiti3� � è q Qi
, ãäå i � 1, 2;
3) vi ÿâëÿåòñÿ ìåðòâîé òî÷êîé, v i3� òàêîâîé íå ÿâëÿåòñÿ è ïðè ýòîì q Qi
,
ãäå i � 1 2, .
Âî èçáåæàíèå òåðìèíîëîãè÷åñêèõ êîëëèçèé óñëîâèìñÿ ñîñòîÿíèÿ � �v v q z1 2, , ,
êîìáèíèðîâàííûõ ìàøèí íàçûâàòü ìåòà-ñîñòîÿíèÿìè. Ôóíêöèÿ ïåðåõîäîâ �� âû-
ñòóïàåò â äâîÿêîé ðîëè. Ñ îäíîé ñòîðîíû, �� îáåñïå÷èâàåò ïðî÷òåíèå ìàøèíîé
K D( , , )� �1 2 òîëüêî òàêèõ ïàð ïîñëåäîâàòåëüíîñòåé âèäà tr v� ( , )
1 1
� , ( , )v
2 2
� , …,
êîòîðûå ÿâëÿþòñÿ F-ñîâìåñòíûìè òðàññàìè â ïðîãðàììàõ �1 è � 2 .  ñëó÷àå íàðó-
øåíèÿ òðåáîâàíèé F-ñîâìåñòíîñòè çíà÷åíèå ôóíêöèè �� ñòàíîâèòñÿ íåîïðåäåëåí-
íûì. Ñ äðóãîé ñòîðîíû, ìàøèíà K D( , , )� �1 2 ïðîâåðÿåò, îäèíàêîâû ëè ðåçóëüòàòû
òåõ âû÷èñëåíèé, êîòîðûå ïðîêëàäûâàþò ýòè òðàññû â ïðîãðàììàõ �1 è � 2 . Çíà÷å-
íèå �� ñòàíîâèòñÿ íåîïðåäåëåííûì (è, ñëåäîâàòåëüíî, ïðîãîí ìàøèíû ïðåêðàùàåò-
ñÿ), êàê òîëüêî ñòàíîâèòñÿ ÿñíî, ñîâïàäàþò èëè íå ñîâïàäàþò ýòè ðåçóëüòàòû. Â ïî-
ñëåäíåì ñëó÷àå êîìáèíèðîâàííàÿ ìàøèíà äîïóñêàåò ýòó ïàðó òðàññ. Áîëåå
ôîðìàëüíî ýòè ñâîéñòâà êîìáèíèðîâàííîé ìàøèíû óñòàíîâëåíû â ñëåäóþùèõ
ëåììàõ.
Ëåììà 1. Ïðåäïîëîæèì, ÷òî ïðîãîí �� êîìáèíèðîâàííîé ìàøèíû
K D( , , )� �1 2 íà÷èíàåòñÿ â ìåòà-ñîñòîÿíèè � �v v q z1 2, , , è äîñòèãàåò ìåòà-ñîñòîÿíèÿ
� � � � � �v v q z1 2, , , . Òîãäà ïðîåêöèè � [ ]� 1 è � [ ]� 2 ýòîãî ïðîãîíà ÿâëÿþòñÿ òðàññàìè â ïðî-
ãðàììàõ �1 è � 2 , âåäóùèìè èç òî÷åê v1 è v2 â òî÷êè �v1 è �v2 ñîîòâåòñòâåííî.
Äîêàçàòåëüñòâî ïðîâîäèòñÿ èíäóêöèåé ïî äëèíå ïðîãîíà �� .
Ëåììà 2. Äëÿ ëþáîãî íà÷àëüíîãî ïðîãîíà �� êîìáèíèðîâàííîé ìàøèíû
K D( , , )� �1 2 ïðîåêöèè � [ ]� 1 è � [ ]� 2 ÿâëÿþòñÿ F-ñîâìåñòíûìè òðàññàìè â ïðîãðàì-
ìàõ �1 è � 2 .
Äîêàçàòåëüñòâî. Ñîãëàñíî ëåììå 1 ïðîåêöèè � [ ]� 1 è � [ ]� 2 ÿâëÿþòñÿ íà÷àëüíû-
ìè òðàññàìè â �1 è � 2 . ×òîáû óáåäèòüñÿ â F-ñîâìåñòíîñòè ýòèõ òðàññ, îãðàíè÷èì-
ñÿ ðàññìîòðåíèåì ñëó÷àÿ, êîãäà � [ ] , ( , )� 1 1 1 1� � �tr v � , � [ ] , ( , )� 2 2 2 2� � �tr v � è ïðè
ýòîì [ ( )] [ ( )]B tr B trF F1 1 2 2� . Ïîñêîëüêó 2-DM D îïèñûâàåò øêàëó F, òî ñïðàâåä-
ëèâî, ÷òî �* ( , ( ), ( ))q B tr B tr q Qaccept0 1 1 2 2 � �
. Äëÿ îïðåäåëåííîñòè áóäåì
ñ÷èòàòü, ÷òî q Q�
1 . Ïðåäïîëîæèì, ÷òî � * ( � , , ) , , ,� q tr tr v v q z0 1 2 1 2� � � � � � . Ïî îïðåäå-
ëåíèþ �� âåðíû ðàâåíñòâà � * ( � , � [ ], )� �q tr0 21 � � ( , , ,� � � � � �v v q z1 2 , ( , ))� � �v1 1�
� � � �T v1 1 1( , )� , �v2 , �( , ( )),q B v� � � �1 1 1� . Òàê êàê D îïèñûâàåò øêàëó F è
[ ( )] [ ( [ ])]B tr BF F2 2 1 1� � , òî ñîñòîÿíèå q q B v� � � � ��( , ( ))1 1 ïðèíàäëåæèò ìíîæåñòâó
Q2 . Çíà÷èò, ïî îïðåäåëåíèþ ôóíêöèè ïåðåõîäîâ �� èìååò ìåñòî ðàâåíñòâî
� * ( � , [ ], [ ]) � ( ( , ), , , , (� � � �q T v v q0 1 1 1 2 11 2 � � � � � �� � � �� � v2 2, ))�� . Çíà÷åíèå â åãî ëåâîé ÷àñòè
îïðåäåëåíî, à çíà÷èò, îïðåäåëåíî è çíà÷åíèå â åãî ïðàâîé ÷àñòè. Ýòî âîçìîæíî
ëèøü â ñëó÷àå � � �� �1 2 , ÷òî ñâèäåòåëüñòâóåò î F-ñîâìåñòíîñòè òðàññ � [ ]� 1 è � [ ]� 2 .
Ëåììà äîêàçàíà.
Íà÷àëüíûé ïðîãîí �� ìàøèíû K D( , , )� �1 2 íàçîâåì ìàêñèìàëüíûì, åñëè �� ëèáî
ÿâëÿåòñÿ áåñêîíå÷íûì, ëèáî ÿâëÿåòñÿ êîíå÷íûì, íî íå ìîæåò áûòü ïðîäîëæåí.
Ëåììà 3. Äëÿ ëþáîé ïàðû F-ñîâìåñòíûõ òðàññ tr1 è tr2 â ïðîãðàììàõ �1 è � 2
ñóùåñòâóåò òàêîé ìàêñèìàëüíûé ïðîãîí �� ìàøèíû K D( , , )� �1 2 , ÷òî � [ ]� 1 ÿâëÿåò-
ñÿ ïðåôèêñîì tr1 è � [ ]� 2 ÿâëÿåòñÿ ïðåôèêñîì tr2 .
Äîêàçàòåëüñòâî. Ñïðàâåäëèâîñòü óòâåðæäåíèÿ ñëåäóåò íåïîñðåäñòâåííî èç
îïðåäåëåíèÿ êîìáèíèðîâàííîé ìàøèíû K D( , , )� �1 2 .
Òåîðåìà 3. Åñëè 2-DM D îïèñûâàåò øêàëó F, òî � �1 2
F òîãäà è òîëüêî òîã-
äà, êîãäà êîìáèíèðîâàííàÿ ìàøèíà K D( , , )� �1 2 óäîâëåòâîðÿåò ñëåäóþùèì òðåáî-
âàíèÿì.
A. K D( , , )� �1 2 ïîðîæäàåò ïóñòîå áèíàðíîå îòíîøåíèå EK D( , , )� �1 2
.
B. Äëÿ êàæäîãî áåñêîíå÷íîãî ïðîãîíà �� ìàøèíû K D( , , )� �1 2 îáå ïðîåêöèè
�[ ]� 1 è �[ ]� 2 ÿâëÿþòñÿ áåñêîíå÷íûìè òðàññàìè.
44 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4
Äîêàçàòåëüñòâî. Äàëåå äëÿ êðàòêîñòè îáîçíà÷åíèÿ êîìáèíèðîâàííîé ìàøèíû
K D( , , )� �1 2 áóäåì èñïîëüçîâàòü çàïèñü �K .
(�) Ïîêàæåì, ÷òî èç íåâûïîëíèìîñòè ëþáîãî èç òðåáîâàíèé A èëè B ñëåäóåò
íåýêâèâàëåíòíîñòü ïðîãðàìì �1 è � 2 .
Òðåáîâàíèå A. Ïðåäïîëîæèì, ÷òî E
K�
� � . Òîãäà íåêîòîðûé íà÷àëüíûé ïðî-
ãîí �� ïðèâîäèò �K ê äîïóñêàþùåìó ìåòà-ñîñòîÿíèþ � , , , �q v v q z Qaccept� � �
1 2 . Êàê
ñëåäóåò èç îïðåäåëåíèÿ ìíîæåñòâà äîïóñêàþùèõ ñîñòîÿíèé �Qaccept , âîçìîæíû òðè
ñëó÷àÿ.
1. Åñëè v exit1 � , v exit2 � è q Qaccept� , òî ñîãëàñíî ëåììàì 1 è 2 ïðîåêöèè
� [ ]� 1 è � [ ]� 2 ÿâëÿþòñÿ ïîëíûìè F-ñîâìåñòíûìè òðàññàìè â ïðîãðàììàõ �1 è � 2 , çà-
âåðøàþùèìèñÿ â òî÷êå exit. Òàê êàê 2-DM D îïèñûâàåò øêàëó F è q Qaccept� , òî
ñïðàâåäëèâî íåðàâåíñòâî [ ( �[ ])] [ ( �[ ])]B BF F1 21 2� �� ñëåäîâàòåëüíî, ïî òåîðåìå 2
ïðîãðàììû �1 è � 2 íåýêâèâàëåíòíû íà øêàëå F.
2. Ïðåäïîëîæèì, ÷òî v exit1 � , v exit2 � è q Q
1 . Òîãäà ïî ëåììå 1 ïðîåêöèÿ
� [ ]� 1 — ýòî ïîëíàÿ òðàññà â �1, çàâåðøàþùàÿñÿ â òî÷êå exit, � [ ]� 2 — ýòî íà÷àëüíàÿ
òðàññà â � 2 , âåäóùàÿ â òî÷êó v2 , ïðè ýòîì � � �* ( , ( � [ ]), ( � [ ]))q B B q0 1 21 2 � . Ïî
ëåììå 2 òðàññû � [ ]� 1 è � [ ]� 2 ÿâëÿþòñÿ F-ñîâìåñòíûìè. Èç óòâåðæäåíèÿ 3 ñëåäóåò, ÷òî
� [ ]� 1 è � [ ]� 2 — ïðåôèêñû òðàññ tr M( , )�1 è tr M( , )� 2 äëÿ íåêîòîðîé F-ìîäåëè M.
Åñëè òðàññà tr M( , )� 2 áåñêîíå÷íà, òî [ ( , )] [ ( , )]comp M comp MF F� �1 2� . Eñëè
òðàññà tr M( , )� 2 êîíå÷íà , òî îíà ïðåäñòàâèìà â âèäå tr M( , )� 2 �
� � [ ]� 2 tr äëÿ íåêîòîðîé òðàññû tr, âåäóùåé èç òî÷êè v2 â exit. Ïîñêîëüêó �* (q0 ,
B1 1( � [ ])� , B tr2 2( � [ ] ))� � � �* ( , , )q tr è q Q
1 , çíà÷åíèå �* (q0 ,B1 1( � [ ])� , B tr2 2( � [ ] ))�
íå îïðåäåëåíî. Ó÷èòûâàÿ, ÷òî 2-DM D îïèñûâàåò øêàëó F, ïðèõîäèì ê âûâîäó, ÷òî
[ ( , )]comp M F�1 � [ ( � [ ])]B F1 1� � [ ( � [ ] )]B tr F2 2� � [ ( , )]comp M F� 2 . Îòñþäà ñëå-
äóåò, ÷òî ïðîãðàììû �1 è � 2 íåýêâèâàëåíòíû íà øêàëå F.
3. Ïðåäïîëîæèì, ÷òî v1 ÿâëÿåòñÿ ìåðòâîé òî÷êîé, v2 òàêîâîé íå ÿâëÿåòñÿ è
q Q
1 . Ñîãëàñíî ëåììàì 1 è 2 ïðîåêöèè � [ ]� 1 è � [ ]� 2 — ýòî F-ñîâìåñòíûå òðàññû â
ïðîãðàììàõ �1 è � 2 , âåäóùèå â òî÷êè v1 è v2 ñîîòâåòñòâåííî, ïðè ýòîì
� � �* ( , ( � [ ]), ( � [ ]))q B B q0 1 21 2 � . Ðàññìîòðèì ïðîèçâîëüíóþ òðàññó tr, âåäóùóþ â
ïðîãðàììå � 2 èç òî÷êè v2 â òî÷êó exit. Òàê êàê äëÿ ëþáîãî i i tr, | |1� � , ñïðàâåäëèâî
ðàâåíñòâî � � � � �* ( , ( � [ ]), ( � [ ] )) * ( , , ( ))q B B tr q B tri i
0 1 2 21 2 � è q Q
1 , òî çíà÷åíèÿ
� � �* ( , ( � [ ]), ( � [ ] ))q B B tri
0 1 21 2 íå îïðåäåëåíû. Ó÷èòûâàÿ, ÷òî 2-DM D îïèñûâàåò
øêàëó F, ýòî îçíà÷àåò, ÷òî � � �* ( , ( � [ ]), ( � [ ] ))q B B tri
0 1 21 2 äëÿ ëþáîãî i i tr, | |1� � .
Oòñþäà cîãëàñíî óòâåðæäåíèþ 2 ñëåäóåò, ÷òî � [ ]� 1 è � [ ]� 2 tr — F-ñîâìåñòíûå
òðàññû. Ñîãëàñíî óòâåðæäåíèþ 3 � [ ]� 1 è � [ ]� 2 tr — ïðåôèêñû òðàññ tr M( , )�1 è
tr M( , )� 2 äëÿ íåêîòîðîé F-ìîäåëè M. Íî ïîñêîëüêó � [ ]� 1 âåäåò â ìåðòâóþ òî÷êó,
òðàññà tr M( , )�1 íå ìîæåò çàâåðøàòüñÿ â òî÷êå exit. Çíà÷èò, âû÷èñëåíèå
comp M( , )�1 áåñêîíå÷íî è, ñëåäîâàòåëüíî, ïðîãðàììû �1 è � 2 íåýêâèâàëåíòíû
íà øêàëå F.
Òðåáîâàíèå B. Ïðåäïîëîæèì, ÷òî ñóùåñòâóåò òàêîé áåñêîíå÷íûé íà÷àëüíûé
ïðîãîí �� êîìáèíèðîâàííîé ìàøèíû �K , îäíà èç ïðîåêöèé êîòîðîãî (íàïðèìåð,
� [ ])� 1 ÿâëÿåòñÿ áåñêîíå÷íîé òðàññîé, à äðóãàÿ (â äàííîì ñëó÷àå � [ ]� 2 ) — êîíå÷íàÿ
òðàññà, âåäóùàÿ â òî÷êó v2 . Òîãäà ïî îïðåäåëåíèþ �K ñóùåñòâóåò òàêîå i i0 0 0, � ,
÷òî äëÿ êàæäîãî j j i, 0 , èìååò ìåñòî âêëþ÷åíèå � �* ( , ( � [ ] ),q B j
0 1 1 B2 2( � [ ]))� �
�
q Qj 1 . Çàìåòèì, ÷òî q Qj accept� , ïîñêîëüêó â ïðîòèâíîì ñëó÷àå äëÿ ëþáîãî
îïåðàòîðà a a A,
, âûïîëíÿëîñü áû ðàâåíñòâî � � � � �B a B aj
F F1 21 2( � [ ] ) ( � [ ]� � .
Ó÷èòûâàÿ, ÷òî 2-DM D îïèñûâàåò øêàëó F, ýòî ðàâåíñòâî ïðèâåëî áû ê íåîïðåäå-
ëåííîìó çíà÷åíèþ � � �* ( , ( � [ ] ), ( � [ ]))q B Bj
0 1
2
21 2� .
Äàëåå ðàññìîòðèì äâà ñëó÷àÿ.
1. Òî÷êà v2 ÿâëÿåòñÿ ìåðòâîé. Äëÿ ïðîèçâîëüíîãî j0 , j i0 0 , ðàññìîòðèì
òî÷êó v1 , â êîòîðóþ â ïðîãðàììå �1 âåäåò òðàññà �[ ]1 0j . Êàê ñëåäóåò èç îïðåäå-
ëåíèÿ ôóíêöèè ïåðåõîäîâ �� , òî÷êà v1 íå ìîæåò áûòü ìåðòâîé, ïîñêîëüêó â ïðî-
òèâíîì ñëó÷àå òàêîé áåñêîíå÷íûé ïðîãîí �� áûë áû íåâîçìîæåí. Ïîýòîìó â ïðî-
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4 45
ãðàììå �1 åñòü òðàññà tr, âåäóùàÿ èç òî÷êè v1 â exit. Çàìåòèì, ÷òî òðàññû �[ ]1 0j tr è
�[ ]2 ÿâëÿþòñÿ F-ñîâìåñòíûìè. Äåéñòâèòåëüíî, â ïðîòèâíîì ñëó÷àå ðàâåíñòâî
� � � � �B tr B
j k
F
m
F1 21 20( � [ ] ) ( � [ ] )� � âûïîëíÿëîñü áû äëÿ íåêîòîðûõ k , m , à ýòî ïðè-
âåëî áû ê òîìó, ÷òî îáà çíà÷åíèÿ � � �* ( , ( � [ ] ), ( � [ ]))q B B
j
0 1 21 20 è �* ( ,q0
B tr
j k
1 1 0( � [ ] )� , B m
2 2( � [ ] ))� áûëè áû îïðåäåëåíû âîïðåêè òîìó, ÷òî D ÿâëÿåòñÿ äå-
òåðìèíèðîâàííîé ìàøèíîé. Ñîãëàñíî óòâåðæäåíèþ 3 F-ñîâìåñòíîñòü òðàññ
�[ ]1 0j tr è �[ ]2 ãàðàíòèðóåò ñóùåñòâîâàíèå òàêîé F-ìîäåëè M, äëÿ êîòîðîé
� �[ ] ( , )1 0
1
j
tr tr M� , à �[ ]2 ÿâëÿåòñÿ ïðåôèêñîì tr M( , )� 2 . Ïîñêîëüêó v2 — ýòî
ìåðòâàÿ òî÷êà, ïîëíàÿ òðàññà tr M( , )� 2 íå ìîæåò âåñòè â òî÷êó exit è ïîýòîìó ÿâëÿ-
åòñÿ áåñêîíå÷íîé òðàññîé. Òàêèì îáðàçîì, âû÷èñëåíèå comp M( , )�1 îêàçûâàåòñÿ
êîíå÷íûì, à âû÷èñëåíèå comp M( , )� 2 — áåñêîíå÷íûì. Ýòî îçíà÷àåò, ÷òî ïðîãðàì-
ìû �1 è � 2 íåýêâèâàëåíòíû íà øêàëå F.
2. Òî÷êà v2 íå ÿâëÿåòñÿ ìåðòâîé. Ðàññìîòðèì â ïðîãðàììå � 2 ïðîèçâîëüíóþ
òðàññó tr, âåäóùóþ èç òî÷êè v2 â òî÷êó exit. Êàê áûëî îòìå÷åíî ðàíåå, äëÿ ëþáîãî
j j i, 0 , âûïîëíÿåòñÿ âêëþ÷åíèå � �* ( , ( � [ ] )q B j
0 1 1 , B q Qj2 12( � [ ]))� �
. Ïîýòîìó
äëÿ ëþáîé ïàðû j m j i m tr, , , | | � �0 0 , çíà÷åíèå � � �* ( , ( � [ ] ), ( � [ ] ))q B B trj m
0 1 21 2
íå îïðåäåëåíî. Èñõîäÿ èç òîãî, ÷òî 2-DM D îïèñûâàåò øêàëó F, íåðàâåíñòâî
� � � � �B B trj
F
m
F1 21 2( � [ ] ) ( � [ ] )� � âûïîëíÿåòñÿ äëÿ êàæäîé òàêîé ïàðû j m, . Ñëåäî-
âàòåëüíî, � [ ]� 1 è � [ ]� 2 tr — ïîëíûå F-ñîâìåñòíûå òðàññû â ïðîãðàììàõ �1 è � 2 ,
ïðè÷åì îäíà èç íèõ ÿâëÿåòñÿ áåñêîíå÷íîé, à äðóãàÿ — êîíå÷íîé. Ñîãëàñíî òåîðå-
ìå 2 ýòî îçíà÷àåò, ÷òî ïðîãðàììû �1 è � 2 íåýêâèâàëåíòíû íà øêàëå F.
(�) Ðàññìîòðèì ïðîèçâîëüíóþ ïàðó ïîëíûõ F-ñîâìåñòíûõ òðàññ tr1 è tr2
â ïðîãðàììàõ �1 è � 2 . Ñîãëàñíî ëåììå 3 êîìáèíèðîâàííàÿ ìàøèíà �K èìååò ìàê-
ñèìàëüíûé ïðîãîí �� , ïðîåêöèè � [ ]� 1 è � [ ]� 2 êîòîðîãî ÿâëÿþòñÿ ïðåôèêñàìè òðàññ tr1
è tr2 ñîîòâåòñòâåííî. Âîçìîæíû äâà âàðèàíòà óñòðîéñòâà ïðîãîíà �� .
1. Ìàêñèìàëüíûé ïðîãîí �� ÿâëÿåòñÿ êîíå÷íûì. Òîãäà îí äîñòèãàåò òàêîãî
ìåòà-ñîñòîÿíèÿ � , , ,q v v q z� � �1 2 , äëÿ êîòîðîãî çíà÷åíèå ôóíêöèè ïåðåõîäîâ
� ( �, ( , ))� q v � íå îïðåäåëåíî íè äëÿ îäíîé ïàðû ( , )v � . Ïîñêîëüêó òðåáîâàíèå A âû-
ïîëíåíî, ìåòà-ñîñòîÿíèå �q íå ìîæåò áûòü äîïóñêàþùèì. Ïîýòîìó ñóùåñòâóþò
ëèøü äâå ïðè÷èíû, íå ïîçâîëÿþùèå ïðîäîëæèòü ïðîãîí �� : ëèáî v exit1 � , v exit2 �
è q Qaccept
, ëèáî îáå òî÷êè v1 è v2 ÿâëÿþòñÿ ìåðòâûìè.
Òàê êàê 2-DM D îïèñûâàåò øêàëó F, â ïåðâîì ñëó÷àå âûïîëíÿåòñÿ ðàâåíñòâî
[ ( )] [ ( )]B tr B trF F1 1 2 2� , à âî âòîðîì ñëó÷àå îáå òðàññû tr1 è tr2 ÿâëÿþòñÿ áåñêîíå÷íûìè.
2. Ìàêñèìàëüíûé ïðîãîí �� ÿâëÿåòñÿ áåñêîíå÷íûì. Òîãäà òðåáîâàíèå  ãàðàí-
òèðóåò, ÷òî îáå ïðîåêöèè tr1 1� �[ ] è tr2 1� �[ ] ÿâëÿþòñÿ áåñêîíå÷íûìè òðàññàìè.
Òàêèì îáðàçîì, äëÿ ëþáîé ïàðû ïîëíûõ F-ñîâìåñòíûõ òðàññ tr1 è tr2 â ïðî-
ãðàììàõ �1 è � 2 ëèáî îáå òðàññû îêàçûâàþòñÿ áåñêîíå÷íûìè, ëèáî [ ( )]B tr F1 1 �
� [ ( )]B tr F2 2 . Ñîãëàñíî òåîðåìå 2 ýòî îçíà÷àåò, ÷òî � �1 2
F .
Òåîðåìà äîêàçàíà.
Îñíîâíîå äîñòîèíñòâî òåîðåìû 3 ñîñòîèò â òîì, ÷òî çàäà÷à ïðîâåðêè ýêâèâà-
ëåíòíîñòè ïðîãðàìì � �1 2
F ñâîäèòñÿ ê ïðîâåðêå ïóñòîòû 2-DM K D( , , )� �1 2 , â
ñòðóêòóðå êîòîðîé îòðàæàþòñÿ èíäèâèäóàëüíûå îñîáåííîñòè ñåìàíòèêè ïðîãðàì-
ìíûõ îïåðàòîðîâ. Âûäåëèâ êëàññû êîìáèíèðîâàííûõ ìàøèí, äëÿ êîòîðûõ ïðîáëå-
ìà ïóñòîòû ðåøàåòñÿ ýôôåêòèâíî, ìîæíî óñòàíîâèòü è òå àëãåáðàè÷åñêèå ñâîéñòâà
îïåðàòîðîâ, êîòîðûå öåëåñîîáðàçíî ó÷èòûâàòü ïðè ðàçðàáîòêå áûñòðûõ àëãîðèò-
ìîâ ïðîâåðêè ýêâèâàëåíòíîñòè è ìèíèìèçàöèè ïðîãðàìì. Ýòà çàäà÷à òðåáóåò ïðî-
âåäåíèÿ îòäåëüíîãî èññëåäîâàíèÿ, ðåçóëüòàòû êîòîðîãî áóäóò îïóáëèêîâàíû â ïî-
ñëåäóþùèõ ðàáîòàõ. Ïðèâåäåííîå íèæå ïðîñòîå ñëåäñòâèå èç òåîðåìû 3 ïîêàçûâà-
åò, ÷òî ýòî íàïðàâëåíèå èññëåäîâàíèé ÿâëÿåòñÿ ïåðñïåêòèâíûì.
Òåîðåìà 4. Åñëè äèíàìè÷åñêàÿ øêàëà F ìîæåò áûòü îïèñàíà 2-DM ñ êîíå÷-
íûì ÷èñëîì ñîñòîÿíèé (äâóõëåíòî÷íûì äåòåðìèíèðîâàííûì êîíå÷íûì àâòîìà-
òîì), òî çàäà÷à ïðîâåðêè ýêâèâàëåíòíîñòè ïðîãðàìì � �1 2
F ïðèíàäëåæèò êëàññó
ñëîæíîñòè NLOGSPACE.
46 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4
Äîêàçàòåëüñòâî. Åñëè 2-DM D, îïèñûâàþùàÿ øêàëó F, èìååò n ñîñòîÿíèé, òî
êîìáèíèðîâàííàÿ ìàøèíà K D( , , )� �1 2 èìååò O n( | | | | )� �1 2 ìåòà-ñîñòîÿíèé. Ïðîâåð-
êà òðåáîâàíèé A è Â èç òåîðåìû 3 ñâîäèòñÿ, òàêèì îáðàçîì, ê NLOGSPACE-ïîëíîé
çàäà÷å ïðîâåðêè äîñòèæèìîñòè âåðøèí â êîíå÷íîì îðèåíòèðîâàííîì ãðàôå.
Ñóùåñòâóåò öåëûé ðÿä øêàë, îòðàæàþùèõ àëãåáðàè÷åñêèå ñâîéñòâà ðåàëüíûõ
ïðîãðàììíûõ îïåðàòîðîâ è óäîâëåòâîðÿþùèõ óñëîâèÿì òåîðåìû 4. Ïîëóãðóïïû
îïåðàòîðîâ ÿâëÿþòñÿ ÷àñòíûì ñëó÷àåì äèíàìè÷åñêèõ øêàë: íåéòðàëüíûé ýëåìåíò
ñëóæèò íà÷àëüíûì ñîñòîÿíèåì äàííûõ, à èíòåðïðåòàöèÿ îïåðàòîðîâ îïðåäåëÿåòñÿ
ðàâåíñòâîì R s a s a( , ) � � . Òîãäà óñëîâèÿì òåîðåìû 4 óäîâëåòâîðÿþò, íàïðèìåð,
ïîëóãðóïïîâûå øêàëû, çàäàííûå ñèñòåìàìè òîæäåñòâ ñëåäóþùåãî âèäà:
1) ab b� (â ñëó÷àå, êîãäà èç ýòèõ òîæäåñòâ íå ñëåäóåò ðàâåíñòâà aa a� ),
2) ab ac� ,
3) ba ca� .
Çäåñü a b c, , — ïðîãðàììíûå îïåðàòîðû.
Âîçìîæíîñòè ïðèìåíåíèÿ íîâîãî ìåòîäà, ñâîäÿùåãî ðåøåíèå ïðîáëåìû ýêâè-
âàëåíòíîñòè ïðîãðàìì ê ïðîâåðêå ïóñòîòû äâóõëåíòî÷íûõ ìàøèí ñïåöèàëüíîãî
âèäà, íå èñ÷åðïûâàþòñÿ ýòèì ïðîñòûì ïðèìåðîì.  ïîñëåäóþùåé ðàáîòå áóäåò ïî-
êàçàíî, ÷òî êîìáèíèðîâàííûå ìàøèíû K D( , , )� �1 2 îáëàäàþò öåëûì ðÿäîì çàìå-
÷àòåëüíûõ ñâîéñòâ. Îïèðàÿñü íà ýòè ñâîéñòâà, âî ìíîãèõ ñëó÷àÿõ óäàåòñÿ êîíñòðóè-
ðîâàòü áûñòðûå àëãîðèòìû ïðîâåðêè ýêâèâàëåíòíîñòè ïðîãðàìì, ñåìàíòèêà
îïåðàòîðîâ êîòîðûõ îïèñûâàåòñÿ ñ ïîìîùüþ óïîðÿäî÷åííûõ äèíàìè÷åñêèõ øêàë.
ÑÏÈÑÎÊ ËÈÒÅÐÀÒÓÐÛ
1. Ë ÿ ï ó í î â À . À . , ß í î â Þ . È . Î ëîãè÷åñêèõ ñõåìàõ ïðîãðàìì // Òð. êîíô. «Ïóòè ðàçâèòèÿ
ñîâåòñêîãî ìàòåìàòè÷åñêîãî ìàøèíîñòðîåíèÿ è ïðèáîðîñòðîåíèÿ». ×. 3, 1956. — Ñ. 5–8.
2. ß í î â Þ . È . Î ëîãè÷åñêèõ ñõåìàõ àëãîðèòìîâ // Ïðîáëåìû êèáåðíåòèêè. Âûï. 1. — Ì.: Ôèçìàòãèç,
1958. — Ñ. 75–121.
3. Ã ë ó ø ê î â Â . Ì . Òåîðèÿ àâòîìàòîâ è ôîðìàëüíûå ïðåîáðàçîâàíèÿ ìèêðîïðîãðàìì //
Êèáåðíåòèêà. — 1965. — ¹ 5. — Ñ. 1–9.
4. Ã ë ó ø ê î â Â . Ì . , Ë å ò è ÷ å â ñ ê è é À . À . Òåîðèÿ äèñêðåòíûõ ïðåîáðàçîâàòåëåé // Èçáðàííûå
âîïðîñû àëãåáðû è ëîãèêè: ñá. ñòàòåé. — Íîâîñèáèðñê: Íàóêà, 1973. — Ñ. 5–39.
5. L u c k h a m D . C . , P a r k D . M . , P a t e r s o n M . S . On formalized computer programs // J. of Computer
and System Science. — 1970. — 4, N 3. — P. 220–249.
6. P a t e r s o n M . S . Program schemata // Machine Intelligence. — Edinburg: Univ. Press., 1968. — 3. — P.
19–31.
7. D e B e k k e r J . W . , S k o t t D . A . Theory of programs. Unpublished notes. — Vienna: IBM Seminar,
1969.
8. Ï î ä ë î â ÷ å í ê î Ð . È . Ïîëóãðóïïîâûå ìîäåëè ïðîãðàìì // Ïðîãðàììèðîâàíèå. — 1981. — ¹ 4. —
Ñ. 3–13.
9. Å ð ø î â À . Ï . Ñîâðåìåííîå ñîñòîÿíèå òåîðèè ñõåì ïðîãðàìì // Ïðîáëåìû êèáåðíåòèêè,
Âûï. 27. — Ì.: Íàóêà, 1973. — Ñ. 87–110.
10. Ë å ò è ÷ å â ñ ê è é À . À . Ôóíêöèîíàëüíàÿ ýêâèâàëåíòíîñòü äèñêðåòíûõ ïðåîáðàçîâàòåëåé. II //
Êèáåðíåòèêà. — 1970. — ¹ 2 — Ñ. 14–28.
11. à î ä ë å â ñ ê è é À . Á . Îá îäíîì ñëó÷àå ñïåöèàëüíîé ïðîáëåìû ôóíêöèîíàëüíîé ýêâèâàëåíòíîñòè
äèñêðåòíûõ ïðåîáðàçîâàòåëåé // Êèáåðíåòèêà. — 1974. — ¹ 3. — Ñ. 32–36.
12. Ë å ò è ÷ å â ñ ê è é À . À . Ýêâèâàëåíòíîñòü àâòîìàòîâ ñ çàêëþ÷èòåëüíûì ñîñòîÿíèåì îòíîñèòåëüíî
ñâîáîäíîé ïîëóãðóïïû ñ ïðàâûì íóëåì // Äîêë. ÀÍ ÑÑÑÐ. — 1968. — 182, ¹ 5.
13. Ë å ò è ÷ å â ñ ê è é À . À . Ôóíêöèîíàëüíàÿ ýêâèâàëåíòíîñòü äèñêðåòíûõ ïðåîáðàçîâàòåëåé. III //
Êèáåðíåòèêà. — 1972. — ¹ 1. — Ñ. 1–4.
14. Ë å ò è ÷ å â ñ ê è é À . À . Ýêâèâàëåíòíîñòü àâòîìàòîâ îòíîñèòåëüíî ïîëóãðóïï ñ ñîêðàùåíèåì //
Ïðîáëåìû êèáåðíåòèêè. Âûï. 27. — Ì.: Ôèçìàòãèç, 1973. — Ñ. 195–212.
15. Ë å ò è ÷ å â ñ ê è é À . À . , Ñ ì è ê ó í Ë . Á . Î ãðóïïàõ ñ ðàçðåøèìîé ïðîáëåìîé ýêâèâàëåíòíîñòè //
Òåç. 4-é Âñåñîþç. êîíô. ïî ìàòåìàòè÷åñêîé ëîãèêå, 1976. — Ñ. 77.
16. Ò à é ö ë è í Ì . À . Ýêâèâàëåíòíîñòü àâòîìàòîâ îòíîñèòåëüíî êîììóòàòèâíîé ïîëóãðóïïû // Àëãåáðà
è ëîãèêà. — 1968. — 8, ¹ 5. — Ñ. 553–600.
17. Ë è ñ î â è ê Ë . Ï . Ìåòàëèíåéíûå ñõåìû ñ çàñûëêàìè êîíñòàíò // Ïðîãðàììèðîâàíèå. — 1985. —
¹ 2. — Ñ. 29–38.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4 47
18. Ë è ñ î â è ê Ë . Ï . Ñòàíäàðòíûå ñõåìû ñ ìàãàçèíàìè // Äîêë. ÀÍ ÓÑÑÐ. — 1989. — ¹ 12. — Ñ. 23–27.
19. Ï å ò ð î ñ ÿ í à . Í . Ïðîáëåìà âêëþ÷åíèÿ íà ïîäïàìÿòè äëÿ îïåðàòîðíûõ ñõåì è ñëó÷àé åå
ðàçðåøåíèÿ // Ñèñòåìíîå è òåîðåòè÷åñêîå ïðîãðàììèðîâàíèå. — Íîâîñèáèðñê: ÂÖ ÑÎ ÀÍ ÑÑÑÐ,
1974. — Ñ. 130–151.
20. Ñ à á å ë ü ô å ë ü ä Â . Ê . Î ïðåîáðàçîâàíèÿõ óíàðíûõ ëèíåéíûõ ðåêóðñèâíûõ ïðîãðàìì //
Êèáåðíåòèêà. — 1975. — ¹ 5. — Ñ. 55–63.
21. Ñ à á å ë ü ô å ë ü ä Â . Ê . Ïîëèíîìèàëüíàÿ îöåíêà ñëîæíîñòè ðàñïîçíàâàíèÿ ëîãèêî-òåðìàëüíîé
ýêâèâàëåíòíîñòè // Äîêë. ÀÍ ÑÑÑÐ. — 1979. — 249, ¹ 4. — Ñ. 793–796.
22. Ñ à á å ë ü ô å ë ü ä Â . Ê . Íîâûé êëàññ ñõåì ñ ðàçðåøèìîé ôóíêöèîíàëüíîé ýêâèâàëåíòíîñòüþ //
Èíôîðìàòèêà: èíñòðóìåíòàëüíûå ñðåäñòâà. — Íîâîñèáèðñê, 1988. — Ñ. 109–126.
23. A s h c r o f t E . , M a n n a Z . , P n u e l i A . A decidable properties of monadic functional schemes // J. of
the ACM. — 1973. — 20, N 3. — P. 489–499.
24. P a t e r s o n M . S . Decision problems in computational models // SIGPLAN Notices. — 1972. — 7. —
P. 74–82.
25. Ê î ò î â Â . Å . , Ñ à á å ë ü ô å ë ü ä Â . Ê . Òåîðèÿ ñõåì ïðîãðàìì. — Ì.: Íàóêà, 1991. — 348 ñ.
26. Ë è ñ î â è ê Ë . Ï . Ñõåìû ïðîãðàìì è ïðåîáðàçîâàòåëè íàä ðàçìå÷åííûìè äåðåâüÿìè. Âûï. 2 // Ìàò.
âîïðîñû êèáåðíåòèêè. — Ì.: Íàóêà, 1996. — Ñ. 281–320.
27. V a l i a n t L . G . The equivalence problem for deterministic finite-turn push-down automata // Information
and Control. — 1974. — 25, N 2. — P. 123–133.
28. Ë å ò è ÷ å â ñ ê è é À . À . Ïðàêòè÷åñêèå ìåòîäû ðàñïîçíàâàíèÿ ýêâèâàëåíòíîñòè äèñêðåòíûõ
ïðåîáðàçîâàòåëåé è ñõåì ïðîãðàìì // Êèáåðíåòèêà. — 1973. — ¹ 4. — Ñ. 15–26.
29. Ï î ä ë î â ÷ å í ê î Ð . È . , Ç à õ à ð î â Â . À . Ïîëèíîìèàëüíûé ïî ñëîæíîñòè àëãîðèòì, ðàñïîçíàþùèé
êîììóòàòèâíóþ ýêâèâàëåíòíîñòü ñõåì ïðîãðàìì // Äîêë. ÐÀÍ. — 1998. — 362, ¹ 6. — Ñ. 27–31.
30. Ç à õ à ð î â Â . À . Áûñòðûå àëãîðèòìû ðàçðåøåíèÿ ýêâèâàëåíòíîñòè îïåðàòîðíûõ ïðîãðàìì íà
óðàâíîâåøåííûõ øêàëàõ // Ìàò. âîïðîñû êèáåðíåòèêè. Âûï. 7. — Ì.: Íàóêà, 1998. — Ñ. 303–324.
31. Z a k h a r o v V . A . An efficient and unified approach to the decidability of equivalence of propositional
programs // Lecture Notes in Computer Science. — 1998. — 1443. — P. 247–259.
32. Ç à õ à ð î â Â . À . Áûñòðûå àëãîðèòìû ðàçðåøåíèÿ ýêâèâàëåíòíîñòè ïðîïîçèöèîíàëüíûõ
îïåðàòîðíûõ ïðîãðàìì íà óïîðÿäî÷åííûõ ïîëóãðóïïîâûõ øêàëàõ // Âåñòíèê Ìîñê. óí-òà. Ñåð. 15.
Âû÷èñë. ìàòåìàòèêà è êèáåðíåòèêà. — 1999. — ¹ 3. — Ñ. 29–35.
33. Ç à õ à ð î â Â . À . Îá ýôôåêòèâíîé ðàçðåøèìîñòè ïðîáëåìû ýêâèâàëåíòíîñòè ëèíåéíûõ óíàðíûõ
ðåêóðñèâíûõ ïðîãðàìì // Ìàò. âîïðîñû êèáåðíåòèêè. Âûï. 8. — Ì.: Íàóêà, 1999. — Ñ. 255–273.
34. Z a k h a r o v V . A . On the decidability of the equivalence problem for orthogonal sequential programs //
Grammars. — 1999. — 2, N 3. — P. 271–181.
35. Z a k h a r o v V . A . On the decidability of the equivalence problem for monadic recursive programs // The-
oretical Informatics and Applications. — 2000. — 34, N 2. — P. 157–171.
36. Z a k h a r o v V . , Z a k h a r y a s c h e v I . On the equivalence-checking problem for a model of programs re-
lated with multi-tape automata // Lecture Notes in Computer Science. — 2005. — 3317. — P. 293–305.
37. Ù å ð á è í à Â . Ë . , Ç à õ à ð î â Â . À . Ýôôåêòèâíûå àëãîðèòìû ïðîâåðêè ýêâèâàëåíòíîñòè ïðîãðàìì
â ìîäåëÿõ, ñâÿçàííûõ ñ îáðàáîòêîé ïðåðûâàíèé // Âåñòíèê Ìîñêîâ. óí-òà. Ñåð. 15. Âû÷èñë.
ìàòåìàòèêà è êèáåðíåòèêà. — 2008. — ¹ 2. — Ñ. 33–41.
38. Ï î ä ë î â ÷ å í ê î Ð . È . Òåõíèêà ñëåäîâ â ðàçðåøåíèè ïðîáëåìû ýêâèâàëåíòíîñòè â àëãåáðàè÷åñêèõ
ìîäåëÿõ ïðîãðàìì // Êèáåðíåòèêà è ñèñòåìíûé àíàëèç. — 2009. — ¹ 5. — Ñ. 25–37.
39. Ï î ä ë î â ÷ å í ê î Ð . È . Èåðàðõèÿ ìîäåëåé ïðîãðàìì // Ïðîãðàììèðîâàíèå. — 1981. — ¹ 2. —
Ñ. 3–14.
40. P o d l o v c h e n k o R . , R u s a k o v D . , Z a k h a r o v V . On the equivalence problem for programs with
mode switching // Lecture Notes in Computer Science. — 2006. — 3845. — P. 351–352.
41. H a r e l D . Dynamic logics // Handbook of Philosophical Logics, D. Gabbay and F. Guenthner (eds.),
1984. — P. 497–604.
42. J o h n s o n J . H . Rational equivalence relations // Theoretical Computer Science. — 1986. — 47, N 1. —
P. 39–60.
43. V a r d i M . Y . , W o l p e r P . Automata-theoretic techniques for modal logics of programs // J. of Com-
puter and System Science. — 1986. — 32, N 2. — P. 183–221.
44. B o u a j j a n i A . , E s p a r z a J . , M a l l e r O . Reachability analysis of pushdown automata: application to
model checking // Lecture Notes in Computer Science. — 1997. — 1243. — P. 135–150.
Ïîñòóïèëà 09.04.2010
48 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4
|