Преобразование спецификации автомата в языке в автоматно эквивалентную спецификацию в языке L
Запропоновано метод переходу від специфікації автомата мовою L* до специфікації у мові L. Спочатку завдяки введенню додаткових предикатних символів специфікація перетворюється у специфікацію автомата зі скінченною пам’яттю, яка потім перетворюється в автоматно еквівалентну специфікацію у мові L....
Збережено в:
| Дата: | 2010 |
|---|---|
| Автор: | |
| Формат: | Стаття |
| Мова: | Russian |
| Опубліковано: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2010
|
| Назва видання: | Кибернетика и системный анализ |
| Теми: | |
| Онлайн доступ: | https://nasplib.isofts.kiev.ua/handle/123456789/45244 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Цитувати: | Преобразование спецификации автомата в языке в автоматно эквивалентную спецификацию в языке L / А.Н. Чеботарев // Кибернетика и системный анализ. — 2010. — № 4. — С. 60-69. — Бібліогр.: 9 назв. — рос. |
Репозитарії
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
nasplib_isofts_kiev_ua-123456789-45244 |
|---|---|
| record_format |
dspace |
| spelling |
nasplib_isofts_kiev_ua-123456789-452442025-02-23T20:16:29Z Преобразование спецификации автомата в языке в автоматно эквивалентную спецификацию в языке L Перетворення специфікації автомата у мові L* в автоматно еквівалентну специфікацію у мові L Transformation of a language L* specification of an FSM to the automata-equivalent specification in the language L Чеботарев, А.Н. Кибернетика Запропоновано метод переходу від специфікації автомата мовою L* до специфікації у мові L. Спочатку завдяки введенню додаткових предикатних символів специфікація перетворюється у специфікацію автомата зі скінченною пам’яттю, яка потім перетворюється в автоматно еквівалентну специфікацію у мові L. A method is proposed to transform an FSM specification in the language L* into the specification in the language L. First, by using additional predicate symbols the specification is transformed to the specification of an FSM with finite memory. Then this specification is transformed to automata-equivalent specification in the language L. 2010 Article Преобразование спецификации автомата в языке в автоматно эквивалентную спецификацию в языке L / А.Н. Чеботарев // Кибернетика и системный анализ. — 2010. — № 4. — С. 60-69. — Бібліогр.: 9 назв. — рос. 0023-1274 https://nasplib.isofts.kiev.ua/handle/123456789/45244 519.713.1 ru Кибернетика и системный анализ application/pdf Інститут кібернетики ім. В.М. Глушкова НАН України |
| institution |
Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| collection |
DSpace DC |
| language |
Russian |
| topic |
Кибернетика Кибернетика |
| spellingShingle |
Кибернетика Кибернетика Чеботарев, А.Н. Преобразование спецификации автомата в языке в автоматно эквивалентную спецификацию в языке L Кибернетика и системный анализ |
| description |
Запропоновано метод переходу від специфікації автомата мовою L* до специфікації у мові L. Спочатку завдяки введенню додаткових предикатних символів специфікація перетворюється у специфікацію автомата зі скінченною пам’яттю, яка потім перетворюється в автоматно еквівалентну специфікацію у мові L. |
| format |
Article |
| author |
Чеботарев, А.Н. |
| author_facet |
Чеботарев, А.Н. |
| author_sort |
Чеботарев, А.Н. |
| title |
Преобразование спецификации автомата в языке в автоматно эквивалентную спецификацию в языке L |
| title_short |
Преобразование спецификации автомата в языке в автоматно эквивалентную спецификацию в языке L |
| title_full |
Преобразование спецификации автомата в языке в автоматно эквивалентную спецификацию в языке L |
| title_fullStr |
Преобразование спецификации автомата в языке в автоматно эквивалентную спецификацию в языке L |
| title_full_unstemmed |
Преобразование спецификации автомата в языке в автоматно эквивалентную спецификацию в языке L |
| title_sort |
преобразование спецификации автомата в языке в автоматно эквивалентную спецификацию в языке l |
| publisher |
Інститут кібернетики ім. В.М. Глушкова НАН України |
| publishDate |
2010 |
| topic_facet |
Кибернетика |
| url |
https://nasplib.isofts.kiev.ua/handle/123456789/45244 |
| citation_txt |
Преобразование спецификации автомата в языке в автоматно эквивалентную спецификацию в языке L / А.Н. Чеботарев // Кибернетика и системный анализ. — 2010. — № 4. — С. 60-69. — Бібліогр.: 9 назв. — рос. |
| series |
Кибернетика и системный анализ |
| work_keys_str_mv |
AT čebotarevan preobrazovaniespecifikaciiavtomatavâzykevavtomatnoékvivalentnuûspecifikaciûvâzykel AT čebotarevan peretvorennâspecifíkacííavtomataumovílvavtomatnoekvívalentnuspecifíkacíûumovíl AT čebotarevan transformationofalanguagelspecificationofanfsmtotheautomataequivalentspecificationinthelanguagel |
| first_indexed |
2025-11-25T03:38:08Z |
| last_indexed |
2025-11-25T03:38:08Z |
| _version_ |
1849731988644167680 |
| fulltext |
ÓÄÊ 519.713.1
À.Í. ×ÅÁÎÒÀÐÅÂ
ÏÐÅÎÁÐÀÇÎÂÀÍÈÅ ÑÏÅÖÈÔÈÊÀÖÈÈ ÀÂÒÎÌÀÒÀ  ßÇÛÊÅ L*
 ÀÂÒÎÌÀÒÍÎ ÝÊÂÈÂÀËÅÍÒÍÓÞ ÑÏÅÖÈÔÈÊÀÖÈÞ Â ßÇÛÊÅ L
Êëþ÷åâûå ñëîâà: ÿçûê ñïåöèôèêàöèè L* , �-ôîðìóëà, äâóñòîðîííåå ñâåðõñëîâî,
�-àâòîìàò, ýëèìèíàöèÿ êâàíòîðîâ, àâòîìàòíàÿ ýêâèâàëåíòíîñòü ñïåöèôèêàöèé.
ÂÂÅÄÅÍÈÅ
 îñíîâå èñïîëüçóåìîãî ïîäõîäà ê äîêàçàòåëüíîìó ïðîåêòèðîâàíèþ ðåàêòèâíûõ
àëãîðèòìîâ ëåæèò ñïåöèôèêàöèÿ ôóíêöèîíàëüíûõ òðåáîâàíèé ê àëãîðèòìó
â ÿçûêå ëîãèêè ïåðâîãî ïîðÿäêà ñ îäíîìåñòíûìè ïðåäèêàòàìè è ôîðìàëüíûé
ïåðåõîä îò ñïåöèôèêàöèè ê ïðîöåäóðíîìó ïðåäñòàâëåíèþ àëãîðèòìà. Îäíà èç
îñíîâíûõ ïðîáëåì, ñâÿçàííûõ ñî ñïåöèôèêàöèåé ñâîéñòâ àëãîðèòìà, ñîñòîèò
â ðàçðàáîòêå ïîäõîäÿùåãî ÿçûêà ñïåöèôèêàöèè. Ïðè ýòîì ïðèõîäèòñÿ èñêàòü
êîìïðîìèññ ìåæäó âûðàçèòåëüíûìè âîçìîæíîñòÿìè ÿçûêà è ñëîæíîñòüþ àëãî-
ðèòìîâ ïðîåêòèðîâàíèÿ. Äëÿ ðàçðåøåíèÿ ýòîãî ïðîòèâîðå÷èÿ èñïîëüçóþòñÿ äâà
óðîâíÿ ÿçûêà: ÿçûê èñõîäíîé ñïåöèôèêàöèè L* [1], ñ äîñòàòî÷íûìè äëÿ ïðàêòè-
÷åñêèõ íóæä âûðàçèòåëüíûìè âîçìîæíîñòÿìè è îáåñïå÷èâàþùèé óäîáñòâî çàïè-
ñè ôóíêöèîíàëüíûõ òðåáîâàíèé ê àëãîðèòìó, è ÿçûê L [2], îáëàäàþùèé ñðàâíè-
òåëüíî îãðàíè÷åííûìè âûðàçèòåëüíûìè âîçìîæíîñòÿìè, íî ýôôåêòèâíî îáðàáà-
òûâàåìûé ïðîöåäóðàìè ñèíòåçà. Âîçìîæíîñòè ñïåöèôèêàöèè â ÿçûêå L
îãðàíè÷åíû àâòîìàòàìè ñ êîíå÷íîé ïàìÿòüþ [3], ÷òî ïîçâîëèëî ðàçðàáîòàòü äëÿ
ñïåöèôèêàöèé â ýòîì ÿçûêå ýôôåêòèâíûå àëãîðèòìû ñèíòåçà, ïðîâåðêè íåïðîòè-
âîðå÷èâîñòè è âåðèôèêàöèè òåìïîðàëüíûõ ñâîéñòâ, à òàêæå ìåòîäû ïðîåêòèðî-
âàíèÿ îòêðûòûõ ñèñòåì, ê êîòîðûì îòíîñÿòñÿ ðåàêòèâíûå àëãîðèòìû. Ïîýòîìó
ÿçûê L* èñïîëüçóåòñÿ (êîãäà ýòî íåîáõîäèìî) äëÿ íà÷àëüíîé ñïåöèôèêàöèè, êî-
òîðàÿ çàòåì ïðåîáðàçóåòñÿ â ñïåöèôèêàöèþ â ÿçûêå L. Â [4] ðàññìîòðåí ñïîñîá
ïåðåõîäà ê ñïåöèôèêàöèè â ÿçûêå L, îäíàêî àâòîìàò, ñèíòåçèðîâàííûé ïî ïîëó-
÷åííîé òàêèì îáðàçîì ñïåöèôèêàöèè, ìîæåò èìåòü äîïîëíèòåëüíûå, òàê íàçûâà-
åìûå ôèêòèâíûå ñîñòîÿíèÿ. Äëÿ óñòðàíåíèÿ ôèêòèâíûõ ñîñòîÿíèé èñïîëüçóåòñÿ
ïðîöåäóðà ïðîâåðêè íåêîòîðûõ ñîñòîÿíèé àâòîìàòà íà ôèêòèâíîñòü [5]. Òàêàÿ
ïðîöåäóðà äîâîëüíî ñëîæíà è, â îòëè÷èå îò âñåõ îñòàëüíûõ ïðîöåäóð ïðîåêòè-
ðîâàíèÿ àëãîðèòìà, èñïîëüçóåò ïðîöåäóðíîå ïðåäñòàâëåíèå àâòîìàòà â âèäå ìíî-
æåñòâà ñîñòîÿíèé è ôóíêöèé ïåðåõîäîâ è âûõîäîâ, à íå ôîðìóëû ÿçûêà
ñïåöèôèêàöèè.
 íàñòîÿùåé ñòàòüå ïðåäëàãàåòñÿ ïðåîáðàçîâàíèå èñõîäíîé ñïåöèôèêàöèè â ñïå-
öèôèêàöèþ â ÿçûêå L, ñïåöèôèöèðóþùóþ àâòîìàò, â íåêîòîðîì ñìûñëå ýêâèâàëåíò-
íûé àâòîìàòó, ñïåöèôèöèðóåìîìó èñõîäíîé ñïåöèôèêàöèåé â ÿçûêå L* . Ïîñêîëüêó
ÿçûêè L* è L îáëàäàþò ðàçëè÷íûìè âûðàçèòåëüíûìè âîçìîæíîñòÿìè, òàêîé ïåðåõîä
îñóùåñòâëÿåòñÿ çà ñ÷åò ââåäåíèÿ äîïîëíèòåëüíûõ ïðåäèêàòíûõ ïåðåìåííûõ.
ÎÑÍÎÂÍÛÅ ÏÎÍßÒÈß
ßçûêè L* è L ïîñòðîåíû íà îñíîâå ñîîòâåòñòâóþùèõ ôðàãìåíòîâ ëîãèêè ïðåäè-
êàòîâ ïåðâîãî ïîðÿäêà ñ îäíîìåñòíûìè ïðåäèêàòàìè, îïðåäåëåííûìè íà ìíî-
æåñòâå ìîìåíòîâ äèñêðåòíîãî âðåìåíè, â êà÷åñòâå êîòîðîãî âûñòóïàåò ìíîæåñ-
òâî Z öåëûõ ÷èñåë. Ñïåöèôèêàöèÿ â îáîèõ ÿçûêàõ èìååò âèä ôîðìóëû �tF t( ) ,
ãäå F t( ) — ôîðìóëà ñ îäíîé ñâîáîäíîé ïåðåìåííîé t. Â ÿçûêå L ôîðìóëà F t( )
ñòðîèòñÿ ñ ïîìîùüþ ëîãè÷åñêèõ ñâÿçîê èç àòîìîâ âèäà p t k( )� , ãäå p — îäíî-
ìåñòíûé ïðåäèêàòíûé ñèìâîë, t — ïåðåìåííàÿ, ïðèíèìàþùàÿ çíà÷åíèÿ èç ìíî-
60 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4
© À.Í. ×åáîòàðåâ, 2010
æåñòâà Z , à k — öåëî÷èñëåííàÿ êîíñòàíòà (ñäâèã âî âðåìåíè). ßçûê L* îòëè÷à-
åòñÿ îò ÿçûêà L òåì, ÷òî ïðè ïîñòðîåíèè ôîðìóëû F t( ) íàðÿäó ñ àòîìàðíûìè ôîð-
ìóëàìè èñïîëüçóþòñÿ åùå ôîðìóëû âèäà � � �t t t k F ti i i( )& ( )&1 1 � � �t t kj i(( 2
� � � �t t k F tj j3 2) ( )) , ãäå k k k1 2 3, , �Z, F t j2 ( ) — ôîðìóëà ÿçûêà L, à F t i1 ( ) —
ôîðìóëà ÿçûêà L* . Òàêèå ôîðìóëû áóäåì íàçûâàòü �-ôîðìóëàìè. Äëÿ ôîðìóëû
F t( ) ÿçûêà L* îïðåäåëèì ïîíÿòèå ðàíãà (îáîçíà÷àåòñÿ # ( ( )))F t ñëåäóþùèì îáðàçîì:
1) # ( ( ))p t k k� (ðàíã àòîìà);
2) åñëè F t t t t k F t t t k t t k F t( ) ( )& ( )& (( ) ( � � � � � � � � �1 1 1 1 1 2 1 2 2 3 2 2 )) ,
òî # ( ( )) max( , )F t r k r k � �1 1 2 3 , ãäå r F t r F t1 1 1 2 2 2 # ( ( )), # ( ( )) ;
3) åñëè F t( ) ïîñòðîåíà èç F ti ( ), i m 1,... , , ñ ïîìîùüþ ëîãè÷åñêèõ ñâÿçîê, òî
# ( ( )) max(# ( ( )), , # ( ( )))F t F t F tm 1 � .
Ïðè îïðåäåëåíèè àâòîìàòíîé ñåìàíòèêè ÿçûêîâ ñïåöèôèêàöèè ýòè ÿçûêè è àâ-
òîìàòû ðàññìàòðèâàþòñÿ êàê ôîðìàëèçìû äëÿ çàäàíèÿ ìíîæåñòâ ñâåðõñëîâ (áåñêî-
íå÷íûõ ñëîâ) â àëôàâèòå �
( ) , ãäå
{ }p pm1 , ,� — íàáîð ïðåäèêàòíûõ ñèìâî-
ëîâ ñïåöèôèêàöèè. Àëôàâèò �
( ) ïðåäñòàâëÿåò ñîáîé ìíîæåñòâî âñåõ äâîè÷íûõ
âåêòîðîâ äëèíû m. Ñèìâîëû àëôàâèòà �
( ) èíîãäà óäîáíî ðàññìàòðèâàòü êàê îòî-
áðàæåíèÿ âèäà �: ,
� { }01. Ïóñòü
1 � , ïðîåêöèåé ñèìâîëà � ��
( ) íà
1
íàçîâåì îãðàíè÷åíèå îòîáðàæåíèÿ � íà
1.
Ïîñêîëüêó â êà÷åñòâå ñâÿçóþùåãî çâåíà ìåæäó ôîðìóëàìè è ñïåöèôèöèðóå-
ìûìè èìè àâòîìàòàìè âûñòóïàþò ìíîæåñòâà ñâåðõñëîâ, îïðåäåëèì íåîáõîäèìûå
ïîíÿòèÿ, êàñàþùèåñÿ ñâåðõñëîâ è àâòîìàòîâ.
Ïóñòü � — êîíå÷íûé àëôàâèò, Z — ìíîæåñòâî öåëûõ ÷èñåë, N Z�
� �{ | },z z 0
N z z
� �{ | }Z 0 . Îòîáðàæåíèÿ u: Z � � , l: N�
� � è g: N
� � íàçûâàþòñÿ ñîîò-
âåòñòâåííî äâóñòîðîííèì ñâåðõñëîâîì (îáîçíà÷àåòñÿ �
�u u u u u( ) ( ) ( ) ( ) ( ) )2 1 0 1 2 ,
ñâåðõñëîâîì (îáîçíà÷àåòñÿ l l( ) ( ) )1 2 � è îáðàòíûì ñâåðõñëîâîì (îáîçíà÷àåòñÿ
�
g g g( ) ( ) ( ))2 1 0 â àëôàâèòå � . Îòðåçîê u u u k( ) ( )... ( )� � �� �1 äâóñòîðîííåãî
ñâåðõñëîâà u îáîçíà÷àåòñÿ u k( , )� � � . Áåñêîíå÷íûå îòðåçêè u k( , )
� è u k( , )� �1 íà-
çîâåì ñîîòâåòñòâåííî k-ïðåôèêñîì è k-ñóôôèêñîì äâóñòîðîííåãî ñâåðõñëîâà u.
Åñëè çíà÷åíèå k íå ñóùåñòâåííî, òî áóäåì ãîâîðèòü îá �-ïðåôèêñå è �-ñóôôèêñå.
Àâòîìàòíàÿ ñåìàíòèêà ÿçûêîâ îïèñûâàåòñÿ â òåðìèíàõ �-àâòîìàòîâ [6]. Êîíå÷-
íûé íåèíèöèàëüíûé �-àâòîìàò A — ýòî òðîéêà � ��, ,Q A� , ãäå �, Q — êîíå÷íûå
ìíîæåñòâà ñîîòâåòñòâåííî âõîäíûõ ñèìâîëîâ è ñîñòîÿíèé, à �A Q Q: � �� — ÷àñ-
òè÷íàÿ ôóíêöèÿ ïåðåõîäîâ àâòîìàòà.
Ñâåðõñëîâî l � �1 2� â àëôàâèòå � äîïóñòèìî â ñîñòîÿíèè q �-àâòîìàòà A,
åñëè ñóùåñòâóåò òàêîå ñâåðõñëîâî ñîñòîÿíèé q q q0 1 2� , ãäå q q0 , ÷òî äëÿ ëþáîãî
i �0 1 2, , , q qi A i i� � 1 1� �( , ) . Ñâåðõñëîâî l äîïóñòèìî äëÿ �-àâòîìàòà A, åñëè îíî
äîïóñòèìî õîòÿ áû â îäíîì èç åãî ñîñòîÿíèé.
Êàæäîé çàìêíóòîé ôîðìóëå F ñòàâèòñÿ â ñîîòâåòñòâèå ìíîæåñòâî ìîäåëåé äëÿ
ýòîé ôîðìóëû, ò.å. ìíîæåñòâî òàêèõ èíòåðïðåòàöèé, íà êîòîðûõ F èñòèííà. Ïóñòü
{ }p pm1 ,... , — ìíîæåñòâî âñåõ ïðåäèêàòíûõ ñèìâîëîâ, âñòðå÷àþùèõñÿ â ôîð-
ìóëå F (ñèãíàòóðà ôîðìóëû). Èíòåðïðåòàöèÿ ôîðìóëû F — ýòî óïîðÿäî÷åííûé íà-
áîð îïðåäåëåííûõ íà Z îäíîìåñòíûõ ïðåäèêàòîâ � �1� �� m , ñîîòâåòñòâóþùèõ
ïðåäèêàòíûì ñèìâîëàì èç
. Èíòåðïðåòàöèþ I m � �� �1 , ,� ìîæíî ïðåäñòàâèòü
â âèäå äâóñòîðîííåãî ñâåðõñëîâà â àëôàâèòå �
( ) , à ìíîæåñòâî âñåõ ìîäåëåé äëÿ
F — â âèäå ìíîæåñòâà M F( ) äâóñòîðîííèõ ñâåðõñëîâ â ýòîì àëôàâèòå. Â äàëüíåé-
øåì èíòåðïðåòàöèè ðàññìàòðèâàþòñÿ êàê äâóñòîðîííèå ñâåðõñëîâà, ïîýòîìó áóäåì
ãîâîðèòü îá èñòèííîñòíîì çíà÷åíèè ôîðìóëû F íà äâóñòîðîííåì ñâåðõñëîâå u è
çíà÷åíèè ôîðìóëû F t( ) â íåêîòîðîé åãî ïîçèöèè �. Ðàçíîñòü ìåæäó ìàêñèìàëüíûì
è ìèíèìàëüíûì çíà÷åíèÿìè ðàíãîâ àòîìîâ, âñòðå÷àþùèõñÿ â ôîðìóëå ÿçûêà L, íà-
çûâàåòñÿ ãëóáèíîé ôîðìóëû. Ñìûñë ïîíÿòèÿ ãëóáèíû ôîðìóëû ñîñòîèò â òîì, ÷òî
èñòèííîñòíîå çíà÷åíèå ôîðìóëû F t( ) ãëóáèíû r â ïîçèöèè � èíòåðïðåòàöèè u
îïðåäåëÿåòñÿ îòðåçêîì u r( , )� �
ñîîòâåòñòâóþùåãî äâóñòîðîííåãî ñâåðõñëîâà u.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4 61
Áóäåì ïîëàãàòü, ÷òî ôîðìóëà F tF t � ( ) çàäàåò ìíîæåñòâî ñâåðõñëîâ W F( ) ,
ñîâïàäàþùåå ñ ìíîæåñòâîì âñåõ �-ñóôôèêñîâ äâóñòîðîííèõ ñâåðõñëîâ èç M F( ) .
Çàìêíóòîé ôîðìóëå F ÿçûêà L ñòàâèòñÿ â ñîîòâåòñòâèå �-àâòîìàò A, äëÿ êîòîðîãî
ìíîæåñòâî äîïóñòèìûõ ñâåðõñëîâ ñîâïàäàåò ñ ìíîæåñòâîì W F( ) ñâåðõñëîâ, çàäà-
âàåìûõ ôîðìóëîé F. Êëàññ �-àâòîìàòîâ, ñïåöèôèöèðóåìûõ ôîðìóëàìè ÿçûêà L,
ñîâïàäàåò ñ êëàññîì äåòåðìèíèðîâàííûõ öèêëè÷åñêèõ �-àâòîìàòîâ ñ êîíå÷íîé ïà-
ìÿòüþ [7]. Ôîðìóëû F tF t1 1 � ( ) è F tF t2 2 � ( ) îäíîãî è òîãî æå èëè ðàçëè÷íûõ
ÿçûêîâ, ñïåöèôèöèðóþùèå �-àâòîìàòû ñ êîíå÷íîé ïàìÿòüþ, íàçîâåì àâòîìàòíî
ýêâèâàëåíòíûìè, åñëè W F W F( ) ( )1 2 .
Äëÿ îïèñàíèÿ ïðåîáðàçîâàíèÿ ñïåöèôèêàöèè èç ÿçûêà L* â ÿçûê L òðåáóåòñÿ
ñëåäóþùàÿ ðàâíîñèëüíîñòü [4].
Ïóñòü F t t t t k F t t t k t t k F t( ) ( )& ( )& (( ) ( � � � � � � � � �1 1 1 1 1 2 1 2 2 3 2 2 )) ,
ãäå k k k1 2 3, , �Z , òîãäà
F t F t F t k( ) ( )& ( )�
� �1 2 3
� � � �
� �( ( ) ( )F t k F t k k1 1 1 2 3 1� , åñëè k k k3 1 2� � , (1)
� � � � �F t k F t k F t k k1 1 2 3 2 1 2( )& ( )& & ( )� , åñëè k k k3 1 2� � ).
Çäåñü F t k( )� îáîçíà÷àåò ôîðìóëó, ïîëó÷åííóþ èç F t( ) ïóòåì çàìåíû t íà t k� .
Ïðàâóþ ÷àñòü ðàâíîñèëüíîñòè (1) íàçîâåì 1-ðàçâåðòêîé �-ôîðìóëû F t( ) . Åå
k-ðàçâåðòêà ïîëó÷àåòñÿ â ðåçóëüòàòå èòåðàòèâíîãî ïðèìåíåíèÿ ðàâíîñèëüíîñòè (1)
k ðàç. Ïóñòü 1-ðàçâåðòêà �-ôîðìóëû F t( ) èìååò âèä F t h t g t( )& ( ) ( )
�1 , òîãäà åå
k-ðàçâåðòêà ðàâíà F t k h t k h t k k( )& ( )& & ( )
� � � � �
1 1 2 0� �� � � , ãäå
�0 g t( ), à � i ( , , )i k �
1 1 ðàâíî g t i h t i h t( )& ( )& & ( )
� �1 .
ÏÅÐÅÕÎÄ ÎÒ ßÇÛÊÀ L* Ê ßÇÛÊÓ L
Ïóñòü çàìêíóòûå ôîðìóëû F1 è F2 èìåþò ñîîòâåòñòâåííî ñèãíàòóðû
1 è
2 ,
à
— íåïóñòîå ïîäìíîæåñòâî ìíîæåñòâà
1 2� . Ôîðìóëû F1 è F2 íàçîâåì
ýêâèâàëåíòíûìè îòíîñèòåëüíî ñèãíàòóðû
, åñëè ìíîæåñòâà ïðîåêöèé âñåõ ìî-
äåëåé (äâóñòîðîííèõ ñâåðõñëîâ) èç M F( )1 è M F( )2 íà
ñîâïàäàþò. Àíà-
ëîãè÷íî, ôîðìóëû F1 è F2 àâòîìàòíî ýêâèâàëåíòíû îòíîñèòåëüíî ñèãíàòóðû
,
åñëè ìíîæåñòâî ïðîåêöèé íà
âñåõ ñâåðõñëîâ èç W F( )1 ñîâïàäàåò ñ ìíîæåñ-
òâîì ïðîåêöèé íà
âñåõ ñâåðõñëîâ èç W F( )2 .
Îñíîâíàÿ èäåÿ ñîñòîèò â òîì, ÷òîáû èñõîäíóþ ñïåöèôèêàöèþ S â ÿçûêå L*
ïðåîáðàçîâàòü â òàêóþ, ýêâèâàëåíòíóþ îòíîñèòåëüíî åå ñèãíàòóðû, ñïåöèôèêàöèþ
S1 â ÿçûêå L* , êîòîðàÿ ñïåöèôèöèðóåò �-àâòîìàò ñ êîíå÷íîé ïàìÿòüþ.  ýòîì ñëó-
÷àå ñóùåñòâóåò ñïåöèôèêàöèÿ â ÿçûêå L, àâòîìàòíî ýêâèâàëåíòíàÿ S1, ò.å. òàêàÿ
ñïåöèôèêàöèÿ F, ÷òî W S W F( ) ( )1 . Ïðåîáðàçîâàíèå S â S1 îñóùåñòâëÿåòñÿ ïóòåì
ââåäåíèÿ äîïîëíèòåëüíûõ ïðåäèêàòíûõ ñèìâîëîâ äëÿ ïðåäèêàòîâ, óäîâëåòâîðÿþ-
ùèõ �-ïîäôîðìóëàì ñïåöèôèêàöèè S .
 [4] îïèñàí ïåðåõîä îò ÿçûêà L* ê ÿçûêó L, íàçûâàåìûé ýëèìèíàöèåé êâàíòî-
ðîâ, îäíàêî ïîëó÷àåìàÿ ïðè ýòîì ñïåöèôèêàöèÿ ìîæåò íå áûòü àâòîìàòíî ýêâèâà-
ëåíòíà èñõîäíîé ñïåöèôèêàöèè S îòíîñèòåëüíî åå ñèãíàòóðû. Ïîêàçàíî, ÷òî àâòî-
ìàò, ñïåöèôèöèðóåìûé ñïåöèôèêàöèåé S , ýêâèâàëåíòåí â íåêîòîðîì ñìûñëå ïîäàâ-
òîìàòó àâòîìàòà, ñïåöèôèöèðóåìîãî ïîñòðîåííîé ñïåöèôèêàöèåé â ÿçûêå L.
Îòñþäà ñëåäóåò íåîáõîäèìîñòü âûïîëíåíèÿ äîâîëüíî ñëîæíîé ïðîöåäóðû
ïðîâåðêè íåêîòîðûõ ñîñòîÿíèé ñèíòåçèðîâàííîãî àâòîìàòà íà ôèêòèâíîñòü.
 ïðåäëàãàåìîì ïîäõîäå ê ïîñòðîåíèþ ñïåöèôèêàöèè â ÿçûêå L òàêæå èñïîëü-
çóåòñÿ ïðîöåäóðà ýëèìèíàöèè êâàíòîðîâ, îäíàêî ïîëó÷åííàÿ ñïåöèôèêàöèÿ ïðåîá-
ðàçóåòñÿ â ñïåöèôèêàöèþ, àâòîìàòíî ýêâèâàëåíòíóþ èñõîäíîé ñïåöèôèêàöèè
îòíîñèòåëüíî åå ñèãíàòóðû.
Ïðîöåäóðà ýëèìèíàöèè êâàíòîðîâ â ôîðìóëå F t( ) ñîñòîèò èç äâóõ ýòàïîâ. Íà
ïåðâîì ýòàïå ôîðìóëà F t( ) ïðåîáðàçóåòñÿ ïóòåì ââåäåíèÿ äîïîëíèòåëüíûõ ïðåäè-
êàòíûõ ñèìâîëîâ. Ïóñòü �i t( ) — ìàêñèìàëüíàÿ �-ïîäôîðìóëà ôîðìóëû F t( ) , ò.å.
62 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4
ïîäôîðìóëà, íå ñîäåðæàùàÿñÿ íè â êàêîé äðóãîé �-ïîäôîðìóëå. Êàæäàÿ òàêàÿ
�-ïîäôîðìóëà çàìåíÿåòñÿ àòîìîì âèäà z t ri i( )� , ãäå ri — ðàíã çàìåíÿåìîé �-ïîä-
ôîðìóëû, à zi — ïðåäèêàòíûé ñèìâîë, îòñóòñòâóþùèé â ôîðìóëå F t( ), è â ñïåöè-
ôèêàöèþ äîáàâëÿåòñÿ ýêâèâàëåíòíîñòü z t t ri i i( ) ( )�
� . Åñëè �-ôîðìóëû â ïðà-
âûõ ÷àñòÿõ ýêâèâàëåíòíîñòåé ñîäåðæàò îòëè÷íûå îò íèõ �-ïîäôîðìóëû, òî ñ íèìè
ïîñòóïàþò òàê æå, êàê è ñ �-ïîäôîðìóëàìè èñõîäíîé ôîðìóëû. Îíè çàìåíÿþòñÿ
ñîîòâåòñòâóþùèìè îáîçíà÷åíèÿìè íîâûõ ïðåäèêàòîâ, è äîáàâëÿþòñÿ ýêâèâàëåí-
òíîñòè âèäà z t tj j( ) ( )� � . Ýòî îñóùåñòâëÿåòñÿ äî òåõ ïîð, ïîêà íè îäíà èç �-ôîð-
ìóë � j t( ) íå áóäåò ñîäåðæàòü âõîæäåíèé �-ïîäôîðìóë, îòëè÷íûõ îò íåå.  ðåçóëü-
òàòå ïîëó÷èì ñïåöèôèêàöèþ S tF tz1 � ( ) . Êàê ïîêàçàíî â [8], ýòà ñïåöèôèêàöèÿ
ýêâèâàëåíòíà èñõîäíîé ñïåöèôèêàöèè îòíîñèòåëüíî åå ñèãíàòóðû è ñïåöèôèöèðó-
åò àâòîìàò ñ êîíå÷íîé ïàìÿòüþ. Íà âòîðîì ýòàïå â êàæäîé ýêâèâàëåíòíîñòè
z t t ri i i( ) ( )�
� �-ôîðìóëà �i it r( )
çàìåíÿåòñÿ ïðàâîé ÷àñòüþ ðàâíîñèëüíî-
ñòè (1), ãäå îáîçíà÷åíèå ôîðìóëû �i it r( )
1 çàìåíÿåòñÿ íà z ti ( )
1 . Ýòî äàåò ñïå-
öèôèêàöèþ S t f tz2 � ( ) â ÿçûêå L. Âòîðîé ýòàï ïðèâîäèò ê íåýêâèâàëåíòíîñòè
ïðåîáðàçîâàíèÿ, âûðàæàþùåéñÿ â òîì, ÷òî ïîëó÷åííàÿ ôîðìóëà S 2 ÿçûêà L èìååò
äîïîëíèòåëüíûå ìîäåëè ïî ñðàâíåíèþ ñ ôîðìóëîé �tF tz ( ) , à ñèíòåçèðîâàííûé ïî
íåé àâòîìàò ìîæåò èìåòü äîïîëíèòåëüíûå (ôèêòèâíûå) ñîñòîÿíèÿ.
Ðàññìîòðèì ïðèìåð ýëèìèíàöèè êâàíòîðîâ.
Ïðèìåð 1. Ïóñòü F t t t t x t y t t t t t( ) ( ) ( ) ( ) (( ) � �
� � � � �
�1 1 1 1 2 1 21 2 1
� � �
� � �t t t y t y t3 3 2 31( ) ( )) ( ) . Â ýòîé ôîðìóëå èìååòñÿ åäèíñòâåííàÿ ìàêñèìàëü-
íàÿ �-ïîäôîðìóëà, ðàíã êîòîðîé ðàâåí – 1. Çàìåíèâ åå àòîìîì z t1 1( )
è äîáàâèâ ñîîò-
âåòñòâóþùóþ ýêâèâàëåíòíîñòü, ïîëó÷èì ( ( ) ( ))&( ( )z t y t z t1 11
� � � ( ( )&� �t t t1 1
& ( ) ( )& (( ) ( ) ( ))))� � � � � � � �
�x t y t t t t t t t t y t1 1 2 1 2 3 3 2 32 1 .  ïðàâîé ÷àñòè äî-
áàâëåííîé ýêâèâàëåíòíîñòè èìååòñÿ �-ïîäôîðìóëà ðàíãà – 1, êîòîðóþ çàìåíÿåì
àòîìîì z t2 1( )
. Äîáàâëÿåìàÿ ýêâèâàëåíòíîñòü äëÿ z t2 ( ) èìååò âèä z t2 ( ) �
� � � �( ( ) ( ))t t t y t3 3 2 3 . Òàêèì îáðàçîì, F t z t y t z tz ( ) ( ( ) ( ))&( ( )
� � �1 11 (�t1
( ) ( ) ( ) (( ) ( )))&( ( )t t x t y t t t t t z t z t1 1 1 2 1 2 2 22 1� � � � � � �
� � � �t t t y t3 3 2 3( ) ( )) .
Çàìåíèâ ïðàâûå ÷àñòè ýêâèâàëåíòíîñòåé ñîîòâåòñòâóþùèìè 1-ðàçâåðòêàìè, â êîòî-
ðûõ oáîçíà÷åíèÿ �-ïîäôîðìóë çàìåíåíû ñîîòâåòñòâåííî àòîìàìè z t1 1( )
è
z t2 1( )
, ïîëó÷èì
S t z t2 1 1 �
( ( )�� �
�y t z t z t z t( ))&( ( ) ( ( ) ( )1 1 21 1
� �
� �x t y t x t y t( ) ( ) ( ) ( )))1 1 &( ( ) ( ( ) ( )))z t z t y t2 2 1�
� � .
Êîíåö ïðèìåðà.
Ðàññìîòðèì ôîðìóëû F t z t t t t g t t t t t h t1 1 1 1 2 1 2 2 � � � � � � � �( ( ) ( ) ( ) (( ) ( )))
è F t z t z t h t g t2 1 � �
�( ( ) ( ( ) ( ) ( ))) , ãäå g t( ) è h t( ) — ôîðìóëû ÿçûêà L, è îõàðàê-
òåðèçóåì êëàññû ìîäåëåé äëÿ ýòèõ ôîðìóë. Íåñëîæíî óáåäèòüñÿ â ñïðàâåäëèâîñòè
ñëåäóþùèõ óòâåðæäåíèé.
Óòâåðæäåíèå 1. Âñå ìîäåëè êàê äëÿ F2 , òàê è äëÿ F1 óäîâëåòâîðÿþò ôîðìóëå
� � �t z t g t h t( ( ) ( ( ) ( ))) , ò.å. ÿâëÿþòñÿ ìîäåëÿìè äëÿ ýòîé ôîðìóëû.
Óòâåðæäåíèå 2. Âñÿêàÿ ìîäåëü äëÿ F2 , óäîâëåòâîðÿþùàÿ ôîðìóëå
� � �t t t t g t1 1 1( ) ( ) , åñòü ìîäåëü äëÿ F1.
Óòâåðæäåíèå 3. Âñÿêàÿ ìîäåëü äëÿ F2 , óäîâëåòâîðÿþùàÿ ôîðìóëå
� � � �t t t t z t1 1 1( ) ( ) , åñòü ìîäåëü äëÿ F1.
Ïîêàæåì, íàïðèìåð, ñïðàâåäëèâîñòü óòâåðæäåíèÿ 2.
Ïóñòü u — ìîäåëü äëÿ F2 , óäîâëåòâîðÿþùàÿ ôîðìóëå � � �t t t t g t1 1 1( ) ( ) ,
è � — ïðîèçâîëüíàÿ ïîçèöèÿ â u. Ïîêàæåì, ÷òî èç èñòèííîñòè ôîðìóëû
z t z t h t g t( ) ( ( ) ( ) ( ))�
�1 â ïîçèöèè � ñëåäóåò èñòèííîñòü ôîðìóëû z( ) ( )� � �� 1 ,
ãäå � � � �1 1 1 1 2 1 2 2( ) ( ) ( ) (( ) ( )) � � � � � �t t g t t t t h t . Ïîñêîëüêó u óäîâëåòâîðÿåò
ôîðìóëå � � �t t t t g t1 1 1( ) ( ) , ñóùåñòâóåò � �1 � òàêîå, ÷òî g ( )�1 èñòèííà íà u. Ïóñòü
�1 — áëèæàéøåå ê � çíà÷åíèå, äëÿ êîòîðîãî g(�1) èñòèííà íà u , ò.å. äëÿ âñåõ
� �1 � �t g t( ) ëîæíà. Ðàññìîòðèì äâà ñëó÷àÿ.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4 63
1. Åñëè � �1 , òî z( )� èñòèííà íà u. Î÷åâèäíî, ÷òî �1 ( )t òàêæå èñòèííà â ïîçè-
öèè �, à çíà÷èò, z( ) ( )� � �� 1 èñòèííà íà u.
2. Ïóñòü � �1 � . Ðàññìîòðèì ñíà÷àëà ñëó÷àé, êîãäà z( )� èñòèííà íà u. Òîãäà
â ñèëó èñòèííîñòè z h g( ) ( ) ( )� � �
�1 èñòèííû z( )�
1 è h( )� . Ñëåäîâàòåëüíî, äëÿ
âñåõ � �1 � �t èñòèííà h t( ) .  ýòîì ñëó÷àå � �1 ( ) òàêæå èñòèííà, à çíà÷èò,
z( ) ( )� � �� 1 èñòèííà íà u. Åñëè z( )� ëîæíà, òî ëèáî ñóùåñòâóåò � �1 � �t òàêîå, ÷òî
h t( ) ëîæíà, â ñèëó ÷åãî � �1 ( ) ëîæíà è z( ) ( )� � �� 1 èñòèííà íà u, ëèáî äëÿ âñåõ
� �1 � �t z t( ) ëîæíà, ÷òî ïðîòèâîðå÷èò èñòèííîñòè g ( )�1 . Òàêèì îáðàçîì, âî âñåõ
ñëó÷àÿõ èç èñòèííîñòè z z h g( ) ( ( ) ( ) ( ))� � � ��
�1 ñëåäóåò èñòèííîñòü ôîðìóëû
z( ) ( )� � �� 1 , èç ÷åãî âûòåêàåò, ÷òî u — ìîäåëü äëÿ F1. Êîíåö äîêàçàòåëüñòâà.
Åñëè èíòåðïðåòàöèÿ íå îáëàäàåò ñâîéñòâîì èç óòâåðæäåíèÿ 2, ò.å. íå óäîâëåò-
âîðÿåò ôîðìóëå � � �t t t t g t1 1 1( ) ( ), òî îíà èìååò �-ïðåôèêñ, âî âñåõ ïîçèöèÿõ êîòî-
ðîãî èñòèííà �g t( ) . Åñëè èíòåðïðåòàöèÿ íå îáëàäàåò ñâîéñòâîì èç óòâåðæäåíèÿ 3,
òî îíà èìååò �-ïðåôèêñ, âî âñåõ ïîçèöèÿõ êîòîðîãî èñòèííà z t( ) . Îòñþäà ñëåäóåò,
÷òî åñëè èíòåðïðåòàöèÿ íå îáëàäàåò íè îäíèì èç ýòèõ ñâîéñòâ, òî îíà èìååò �-ïðå-
ôèêñ, âî âñåõ ïîçèöèÿõ êîòîðîãî èñòèííà �g t z t( ) ( ) , ò.å. îíà óäîâëåòâîðÿåò ôîðìó-
ëå � � � � �t t t t g t z t1 1 1 1(( ) ( ) ( )). Åñëè ñóùåñòâóåò ìîäåëü äëÿ F2 , óäîâëåòâîðÿþ-
ùàÿ ýòîé ôîðìóëå, òî â ñèëó óòâåðæäåíèÿ 1 îíà óäîâëåòâîðÿåò ôîðìóëå
� � � � �t t t t g t h t z t1 1 1 1 1(( ) ( ) ( ) ( )) . (2)
Î÷åâèäíî, ÷òî íå ñóùåñòâóåò ìîäåëåé äëÿ F1, óäîâëåòâîðÿþùèõ ýòîé ôîðìó-
ëå, ò.å. âñÿêàÿ ìîäåëü äëÿ F2 , èìåþùàÿ �-ïðåôèêñ, â êàæäîé ïîçèöèè êîòîðîãî èñ-
òèííà ôîðìóëà �g t h t z t( ) ( ) ( ) , íå ÿâëÿåòñÿ ìîäåëüþ äëÿ F1. Â òî æå âðåìÿ äëÿ F2
ñóùåñòâóþò òàêèå ìîäåëè, íàïðèìåð ìîäåëü, óäîâëåòâîðÿþùàÿ ôîðìóëå
� �t g t h t z t( ( ) ( ) ( )) . Òàêèì îáðàçîì, ñïðàâåäëèâî ñëåäóþùåå óòâåðæäåíèå.
Óòâåðæäåíèå 4. Âñå ìîäåëè äëÿ F2 , óäîâëåòâîðÿþùèå ôîðìóëå (2), è òîëüêî
îíè, íå ÿâëÿþòñÿ ìîäåëÿìè äëÿ F1.
Îòñþäà ñëåäóåò òàêæå, ÷òî âñå ìîäåëè äëÿ F1 ñîäåðæàòñÿ ñðåäè ìîäåëåé äëÿ F2 .
Âûøå ðàññìàòðèâàëàñü �-ôîðìóëà ñî çíà÷åíèÿìè k k1 3 0, è k2 1 . Óòâåð-
æäåíèå, àíàëîãè÷íîå óòâåðæäåíèþ 4, ñïðàâåäëèâî è äëÿ �-ôîðìóë ñ ëþáûìè
çíà÷åíèÿìè k ii ( , , ) 1 2 3 . Ýòî ñëåäóåò èç òîãî ôàêòà, ÷òî äëÿ êàæäîé ôîðìóëû âèäà
F t t t t k F t( ) ( )& ( )& � � �1 1 1 1 1 � � � � � �t t k t t k F t2 1 2 2 3 2 2(( ) ( )), ãäå k k1 2, ,
k3 �Z , ñóùåñòâóåò ýêâèâàëåíòíàÿ åé ôîðìóëà âèäà � � �t t t f t t1 1 1 1 2( )& ( )& ((t1 �
� � �t t f t2 2 2) ( )) . Ïóñòü 1-ðàçâåðòêà ôîðìóëû F t( ) èìååò âèä F t h t g t( )& ( ) ( )
�1 .
Ïîêàæåì, ÷òî ôîðìóëà f t t t t g t t t t t h t( ) ( )& ( )& (( ) ( )) � � � � � �1 1 1 2 1 2 2 ýêâèâà-
ëåíòíà ôîðìóëå F t( ), ò.å. ÷òî èç èñòèííîñòè F t( ) â ïîçèöèè � ïðîèçâîëüíîé èíòåð-
ïðåòàöèè u ñëåäóåò èñòèííîñòü f ( )� â ýòîé èíòåðïðåòàöèè è íàîáîðîò. Ôîðìóëà
F t( ) èñòèííà â ïîçèöèè � èíòåðïðåòàöèè u òîãäà è òîëüêî òîãäà, êîãäà ñóùåñòâóåò
òàêîå k � 0, ÷òî F k k1 1( )� �
èñòèííà â èíòåðïðåòàöèè u è äëÿ âñåõ t, óäîâëåòâîðÿþ-
ùèõ � ��
� � � �k k k t k1 2 3 , èñòèííà ôîðìóëà F t2 ( ) . Èñïîëüçóÿ ïîíÿòèå k-ðàç-
âåðòêè, ýòî óòâåðæäåíèå ìîæíî ïåðåôîðìóëèðîâàòü ñëåäóþùèì îáðàçîì.
Óòâåðæäåíèå 5. �-ôîðìóëà F t( ) èñòèííà â ïîçèöèè � äâóñòîðîííåãî ñâåðõñëî-
âà u òîãäà è òîëüêî òîãäà, êîãäà ñóùåñòâóåò òàêîå k � 1, ÷òî ôîðìóëà �k â ( )k � 1 -
ðàçâåðòêå ôîðìóëû F t( ) èñòèííà â ïîçèöèè � ýòîãî ñâåðõñëîâà.
Ïîñêîëüêó ðàçâåðòêè ôîðìóë F t( ) è f t( ) ñîâïàäàþò ñ òî÷íîñòüþ äî îáîçíà÷å-
íèÿ ôîðìóë, òî è ÷ëåíû �k â èõ ( )k � 1 -ðàçâåðòêàõ òàêæå ñîâïàäàþò. Òàêèì îáðà-
çîì, äëÿ ëþáîé èíòåðïðåòàöèè èç èñòèííîñòè îäíîé èç ýòèõ ôîðìóë â ïîçèöèè �
ñëåäóåò èñòèííîñòü äðóãîé è íàîáîðîò, ÷òî ñâèäåòåëüñòâóåò îá èõ ýêâèâàëåíòíîñòè.
Äàëåå ðàññìîòðèì, êàê äëÿ ñïåöèôèêàöèè S1 â ÿçûêå L* ïîñòðîèòü òàêóþ ñïå-
öèôèêàöèþ F â ÿçûêå L, ÷òîáû W S W F( ) ( )1 .
ÀÂÒÎÌÀÒÍÀß ÝÊÂÈÂÀËÅÍÒÍÎÑÒÜ ÑÏÅÖÈÔÈÊÀÖÈÉ
Ïóñòü S1 è S 2 — ñïåöèôèêàöèè ñîîòâåòñòâåííî â ÿçûêå L* è L òàêèå, ÷òî
M S M S( ) ( )1 2� , è G — ìíîæåñòâî âñåõ ìîäåëåé äëÿ S 2 , íå ÿâëÿþùèõñÿ ìîäå-
64 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4
ëÿìè äëÿ S1. Âñå �-ñóôôèêñû êàæäîé ìîäåëè äëÿ ñïåöèôèêàöèè ñîäåðæàòñÿ
â ìíîæåñòâå ñâåðõñëîâ, çàäàâàåìûõ ýòîé ñïåöèôèêàöèåé, ïîýòîìó ñïåöèôèêàöèÿ
S 2 àâòîìàòíî ýêâèâàëåíòíà ñïåöèôèêàöèè S1 òîãäà è òîëüêî òîãäà, êîãäà ìíî-
æåñòâî âñåõ �-ñóôôèêñîâ ìîäåëåé èç G ñîäåðæèòñÿ â W S( 1).
Äëÿ îïèñàíèÿ ñïîñîáà ïîñòðîåíèÿ ñïåöèôèêàöèè F, àâòîìàòíî ýêâèâàëåíòíîé
ñïåöèôèêàöèè S1, óäîáíî âîñïîëüçîâàòüñÿ ïîíÿòèåì ïðîñòðàíñòâà ñîñòîÿíèé, àññî-
öèèðóåìîãî ñ ôîðìóëîé âèäà �tF t( ) [7]. Ïóñòü F tF t � ( ) — ôîðìóëà ÿçûêà L ãëó-
áèíû r, ñ ñèãíàòóðîé
�{ , , }p pm1 . Ôîðìóëó F t( ) áóäåì ðàññìàòðèâàòü êàê ïðî-
ïîçèöèîíàëüíóþ ôîðìóëó ñ ïðîïîçèöèîíàëüíûìè ïåðåìåííûìè p t p tm1 ( ), , ( )� ,
p t p t p t r p t rm m1 11 1( ),... , ( ), , ( ), , ( )
�
� . Åñëè F t1 ( ) è F t2 ( ) — ëîãè÷åñêè ýê-
âèâàëåíòíûå ôîðìóëû, î÷åâèäíî, ÷òî ôîðìóëû �tF t1 ( ) è �tF t2 ( ) çàäàþò îäíî è òî
æå ìíîæåñòâî ñâåðõñëîâ. Ïîñëåäîâàòåëüíîñòü � � �0 1, , ,� r ñèìâîëîâ àëôàâèòà
�
( ) íàçîâåì ñîñòîÿíèåì ãëóáèíû r, à ìíîæåñòâî Q r( , )
âñåõ òàêèõ ïîñëåäîâà-
òåëüíîñòåé — ïðîñòðàíñòâîì ñîñòîÿíèé ãëóáèíû r äëÿ ôîðìóëû F t( ) . Íà ìíîæåñò-
âå Q r( , )
îïðåäåëèì îòíîøåíèå N íåïîñðåäñòâåííîãî ñëåäîâàíèÿ òàê, ÷òî çà ñî-
ñòîÿíèåì q r � � �0 1, , ,� íåïîñðåäñòâåííî ñëåäóþò 2m ñîñòîÿíèé âèäà
� � �1� �� r , , ãäå � ��
( ). Îòíîøåíèå, îáðàòíîå N , îáîçíà÷èì P è íàçîâåì îòíîøå-
íèåì íåïîñðåäñòâåííîãî ïðåäøåñòâîâàíèÿ. Î÷åâèäíî, ÷òî ñîñòîÿíèþ � � �0 1, , ,� r
íåïîñðåäñòâåííî ïðåäøåñòâóþò 2m ñîñòîÿíèé âèäà � � � �, , , ,0 1 1� r
, ãäå
� ��
( ) . Ïóñòü Q Q r1 � ( , )
. Îáîçíà÷èì N Q( )1 ìíîæåñòâî âñåõ ñîñòîÿíèé, íåïîñ-
ðåäñòâåííî ñëåäóþùèõ çà ñîñòîÿíèÿìè èç Q1, à P Q( )1 — àíàëîãè÷íîå ìíîæåñòâî
äëÿ îòíîøåíèÿ P. Åñëè êîìïîíåíòû âåêòîðà � i â ñîñòîÿíèè q r � �� � �0 1, � ðàñ-
ñìàòðèâàòü êàê èñòèííîñòíûå çíà÷åíèÿ ñîîòâåòñòâóþùèõ àòîìîâ ðàíãà i r
, òî
ìîæíî ãîâîðèòü î çíà÷åíèè ôîðìóëû F t( ) íà ñîñòîÿíèè q.
Ïóñòü F t( ) èìååò âèä ( ( )& ( ) ( )& ( )) ( )w t u t w t u t w t1 2 11 1
� � �
� è
� �u w w, ,1 2 . Äëÿ ýòîé ôîðìóëû r 1. Âû÷èñëèì çíà÷åíèå F t( ) íà ñîñòîÿíèè
� �0 1 101 011, , � � � �. Ïðè ýòîì àòîìû ðàíãà 0 ïðèíèìàþò çíà÷åíèÿ èç �1, à àòî-
ìû ðàíãà – 1 — èç � 0 . Òàêèì îáðàçîì, w t u t1 1 0( ) , ( ) , w t1 1( )
= 0 è w t2 1 1( ) ,
ñëåäîâàòåëüíî, F t( ) íà ñîñòîÿíèè � �0 1, ïðèíèìàåò çíà÷åíèå 1.
Ôîðìóëó F t( ) áóäåì ðàññìàòðèâàòü êàê ïðåäñòàâëåíèå ìíîæåñòâà Q F t( ( )) ñî-
ñòîÿíèé èç Q r( , )
, à èìåííî, òåõ ñîñòîÿíèé, íà êîòîðûõ îíà èñòèííà.
Èòàê, ñîñòîÿíèå èç Q r( , )
ïðåäñòàâëÿåò ñîáîé îòðåçîê äëèíû r � 1 äâóñòîðîí-
íåãî ñâåðõñëîâà. Òàêèì îáðàçîì, ëþáîé èíòåðïðåòàöèè äëÿ ôîðìóëû F ñîîòâå-
òñòâóåò äâóñòîðîííåå ñâåðõñëîâî ñîñòîÿíèé �
q q q q q q2 1 0 1 2 3 …, òàêîå, ÷òî
q N qi i� �1 ( ) äëÿ ëþáîãî i �Z. Ïóñòü u — èíòåðïðåòàöèÿ äëÿ ôîðìóëû F tF t � ( ) ,
à Q u( ) — ìíîæåñòâî âñåõ ñîñòîÿíèé, âñòðå÷àþùèõñÿ â äâóñòîðîííåì ñâåðõñëîâå
ñîñòîÿíèé, ñîîòâåòñòâóþùåì u.
Óòâåðæäåíèå 6. Èíòåðïðåòàöèÿ u ÿâëÿåòñÿ ìîäåëüþ äëÿ ôîðìóëû F òîãäà è
òîëüêî òîãäà, êîãäà Q u Q F t( ) ( ( ))� .
Ïóñòü S tF tz1 � ( ) è S t f tz2 � ( ) — ñïåöèôèêàöèè, ïîëó÷åííûå ñîîòâå-
òñòâåííî íà ïåðâîì è âòîðîì ýòàïàõ ýëèìèíàöèè êâàíòîðîâ. Ñïîñîá ïîñòðîåíèÿ
ñïåöèôèêàöèè, àâòîìàòíî ýêâèâàëåíòíîé S1, ðàññìîòðèì ñíà÷àëà äëÿ ñëó÷àÿ, êîãäà
F tz ( ) ñîäåðæèò òîëüêî îäíó �-ïîäôîðìóëó. Ïðè ýòîì M S( )1 íå ñîäåðæèò òîëüêî òå
ìîäåëè èç M S( )2 , êîòîðûå óäîâëåòâîðÿþò ôîðìóëå âèäà
� � � �� � �t t t1 1 1(( ) ( )) . (3)
Çàìåòèì, ÷òî åñëè ìîäåëü îáëàäàåò ñâîéñòâîì (3), òî âñå ñîñòîÿíèÿ, âñòðå÷àþ-
ùèåñÿ â îáðàòíîì ñâåðõñëîâå ñîñòîÿíèé, ñîîòâåòñòâóþùåì åå �-ïðåôèêñó (� óäîâ-
ëåòâîðÿåò ôîðìóëå (3)), ïðèíàäëåæàò ìíîæåñòâó Q t( ( ))� .
Ðàññìîòðèì ñëåäóþùåå ïðåîáðàçîâàíèå ôîðìóëû f tz ( ) .
Ïóñòü D — ìíîæåñòâî ñîñòîÿíèé èç Q r( , )
, çàäàâàåìîå ôîðìóëîé f tz ( ). Ôîð-
ìóëà f t tz ( )& ( )�� çàäàåò ìíîæåñòâî D Q f t tz0 �( ( )& ( ))� âñåõ ñîñòîÿíèé èç D, íå
ïðèíàäëåæàùèõ Q t( ( ))� . Ïîñòðîèì ìíîæåñòâî ñîñòîÿíèé âñåõ òàêèõ äâóñòîðîííèõ
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4 65
ñâåðõñëîâ ñîñòîÿíèé, ñîîòâåòñòâóþùèõ ìîäåëÿì äëÿ S 2 , êîòîðûå èìåþò �-ïðå-
ôèêñ ñ áåñêîíå÷íûì êîëè÷åñòâîì âõîæäåíèé ñîñòîÿíèé èç D0 .
Äëÿ ýòîãî ïîñòðîèì ìàêñèìàëüíîå ïîäìíîæåñòâî D* ñîñòîÿíèé èç D0 , äîñòè-
æèìûõ (â ñìûñëå òðàíçèòèâíîãî çàìûêàíèÿ îòíîøåíèÿ N) èç ñîñòîÿíèé ýòîãî ïîä-
ìíîæåñòâà. Òàêèì îáðàçîì, åñëè D* íå ïóñòî, êàæäîå åãî ñîñòîÿíèå äîñòèæèìî èç
íåêîòîðîãî ñîñòîÿíèÿ èç D* . Äëÿ ïðîèçâîëüíîãî ìíîæåñòâà D D1 � îáîçíà÷èì
N D� ( )1 ìíîæåñòâî âñåõ ñîñòîÿíèé èç D, äîñòèæèìûõ èç D1. Ïîñòðîèì ìíîæåñòâî
N D� ( )* , à ôîðìóëó, çàäàþùóþ ýòî ìíîæåñòâî ñîñòîÿíèé, îáîçíà÷èì F t( ) . Äëÿ
ìíîæåñòâà ìîäåëåé èç M tF t( ( ))� ñïðàâåäëèâû ñëåäóþùèå óòâåðæäåíèÿ.
Óòâåðæäåíèå 7. Âñå ìîäåëè èç M S( )1 ñîäåðæàòñÿ ñðåäè M tF t( ( ))� .
Äåéñòâèòåëüíî, M S( )1 — ýòî âñå ìîäåëè èç M t f tz( ( ))� , íå îáëàäàþùèå ñâîé-
ñòâîì (3), ò.å. íå èìåþùèå �-ïðåôèêñà, äëÿ êîòîðîãî ñîîòâåòñòâóþùåå îáðàòíîå
ñâåðõñëîâî ñîñòîÿíèé ñîäåðæèò ñîñòîÿíèÿ òîëüêî èç Q t( ( ))� . Òàêèì îáðàçîì, âñÿ-
êîå îáðàòíîå ñâåðõñëîâî ñîñòîÿíèé, ñîîòâåòñòâóþùåå �-ïðåôèêñó ìîäåëè èç
M S( )1 , èìååò áåñêîíå÷íîå êîëè÷åñòâî ïîçèöèé ñ ñîñòîÿíèÿìè èç D0 è, ñëåäîâà-
òåëüíî, âñå ñîñòîÿíèÿ äâóñòîðîííåãî ñâåðõñëîâà ñîñòîÿíèé, ñîîòâåòñòâóþùåãî ëþ-
áîé ìîäåëè èç M S( )1 , äîñòèæèìû èç ñîäåðæàùèõñÿ ñðåäè íèõ ñîñòîÿíèé èç D0 . Èç
ýòîãî ñëåäóåò, ÷òî âñå ñîñòîÿíèÿ òàêîãî ñâåðõñëîâà ñîäåðæàòñÿ âî ìíîæåñòâå
N D� ( )* , à â ñèëó óòâåðæäåíèÿ 6 ìîäåëè èç M S( )1 ñîäåðæàòñÿ ñðåäè M tF t( ( ))� .
Óòâåðæäåíèå 8. Äëÿ ëþáîãî �-ñóôôèêñà ìîäåëè èç M tF t( ( ))� , íå ïðèíàäëå-
æàùåé M S( )1 , ñóùåñòâóåò ìîäåëü èç M S( )1 ñ òàêèì æå �-ñóôôèêñîì.
Ïîñêîëüêó êàæäîå ñîñòîÿíèå èç D* äîñòèæèìî èç íåêîòîðîãî ñîñòîÿíèÿ èç D* ,
â ñèëó êîíå÷íîñòè ýòîãî ìíîæåñòâà îíî ñîäåðæèò îäíî èëè íåñêîëüêî ñîñòîÿíèé,
äîñòèæèìûõ èç ñåáÿ, è âñå ñîñòîÿíèÿ èç N D� ( )* äîñòèæèìû èç ýòèõ ñîñòîÿíèé.
Ïóñòü ìîäåëü u M tF t� �( ( )) íå ïðèíàäëåæèò M S( )1 . Ðàññìîòðèì ïðîèçâîëüíûé åå
�-ñóôôèêñ l, êîòîðîìó ñîîòâåòñòâóåò ñâåðõñëîâî ñîñòîÿíèé q q q1 2 3 � Ïîñêîëüêó q1
ïðèíàäëåæèò N D� ( )* , ñóùåñòâóåò ñîñòîÿíèå èç D* , äîñòèæèìîå èç ñåáÿ, èç êîòî-
ðîãî äîñòèæèìî q1. Èç ýòîãî ñëåäóåò, ÷òî ñóùåñòâóåò ìîäåëü äëÿ S1 ñ �-ñóôôèêñîì
l è �-ïðåôèêñîì, äëÿ êîòîðîãî ñîîòâåòñòâóþùåå åìó îáðàòíîå ñâåðõñëîâî ñîñòîÿ-
íèé ñîäåðæèò áåñêîíå÷íî ìíîãî ïîçèöèé ñ ñîñòîÿíèÿìè èç D* .
Òàêèì îáðàçîì, ôîðìóëà F tF t � ( ) àâòîìàòíî ýêâèâàëåíòíà ôîðìóëå S1.
Ðàññìîòðèì òåïåðü ñëó÷àé, êîãäà ñïåöèôèêàöèÿ S1 ñîäåðæèò äâå �-ïîäôîðìó-
ëû. Ïðåäëàãàåìûé ñïîñîá ïîñòðîåíèÿ ñïåöèôèêàöèè, àâòîìàòíî ýêâèâàëåíòíîé S1,
ëåãêî îáîáùèòü íà ôîðìóëó S1, ñîäåðæàùóþ k � 2 �-ïîäôîðìóë.
Ìíîæåñòâî M S( )1 íå ñîäåðæèò òîëüêî òå ìîäåëè èç M S( )2 , êîòîðûå óäîâëåò-
âîðÿþò ïî êðàéíåé ìåðå îäíîé èç ôîðìóë — � � � �� � �t t t1 1 1 1(( ) ( )) èëè
� � � �� � �t t t1 1 2 1(( ) ( )) , ãäå �1 ( )t è �2 ( )t îïðåäåëÿþòñÿ âèäîì ñîîòâåòñòâóþùèõ
�-ïîäôîðìóë â ôîðìóëå S1. Ïóñòü D1 — ìíîæåñòâî ñîñòîÿíèé, çàäàâàåìîå ôîðìó-
ëîé f t tz ( )& ( )��1 , à D2 — ôîðìóëîé f t tz ( )& ( )��2 . Ïîñòðîèì ìíîæåñòâî ñîñòî-
ÿíèé âñåõ òàêèõ äâóñòîðîííèõ ñâåðõñëîâ ñîñòîÿíèé, ñîîòâåòñòâóþùèõ ìîäåëÿì
äëÿ S 2 , êîòîðûå èìåþò �-ïðåôèêñ ñ áåñêîíå÷íûì êîëè÷åñòâîì âõîæäåíèé êàê ñî-
ñòîÿíèé èç D1, òàê è ñîñòîÿíèé èç D2 . Äëÿ ýòîãî îïðåäåëèì âñå òàêèå ïàðû ñîñòîÿ-
íèé ( , )q qi j , ãäå q Di � 1, q Dj � 2 , ÷òî q j äîñòèæèìî èç qi , à qi äîñòèæèìî èç q j .
Çàòåì, åñëè ýòî ìíîæåñòâî íå ïóñòî, ïîñòðîèì ìíîæåñòâî âñåõ ñîñòîÿíèé èç D, êîòî-
ðûå äîñòèæèìû èç ñîñòîÿíèé ýòèõ ïàð. Ôîðìóëà F t( ) , çàäàþùàÿ ïîëó÷åííîå ìíîæåñ-
òâî, ïðåäñòàâëÿåò ñîáîé ðåçóëüòàò òðåáóåìîãî ïðåîáðàçîâàíèÿ ôîðìóëû f tz ( ) .
Ñíà÷àëà ïîêàæåì, ÷òî âñå ìîäåëè èç M S( )1 ñîäåðæàòñÿ ñðåäè M tF t( ( ))� .
Äåéñòâèòåëüíî, M S( )1 — ýòî âñå ìîäåëè èç M t f tz( ( ))� , íå èìåþùèå �-ïðå-
ôèêñà, äëÿ êîòîðîãî ñîîòâåòñòâóþùåå îáðàòíîå ñâåðõñëîâî ñîñòîÿíèé ñîäåðæèò
ñîñòîÿíèÿ òîëüêî èç Q t( ( ))�1 èëè òîëüêî èç Q t( ( ))�2 . Òàêèì îáðàçîì, âñÿêîå îá-
ðàòíîå ñâåðõñëîâî ñîñòîÿíèé, ñîîòâåòñòâóþùåå �-ïðåôèêñó ìîäåëè èç M S( )1 ,
66 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4
èìååò áåñêîíå÷íîå êîëè÷åñòâî ïîçèöèé êàê ñ ñîñòîÿíèÿìè èç D1, òàê è ñ ñîñòîÿíèÿ-
ìè èç D2 . Ïîýòîìó êàæäîå ñîñòîÿíèå èç D1, ñîäåðæàùååñÿ â òàêîì îáðàòíîì ñâåðõ-
ñëîâå ñîñòîÿíèé, äîñòèæèìî èç èìåþùåãîñÿ â íåì ñîñòîÿíèÿ èç D2 è íàîáîðîò.
Ñëåäîâàòåëüíî, âñå ñîñòîÿíèÿ äâóñòîðîííåãî ñâåðõñëîâà ñîñòîÿíèé, ñîîòâåòñòâóþ-
ùåãî ëþáîé ìîäåëè èç M S( )1 , äîñòèæèìû èç èìåþùèõñÿ ñðåäè íèõ ñîñòîÿíèé èç
D1 è D2 . Èç ýòîãî âûòåêàåò, ÷òî âñå ñîñòîÿíèÿ òàêîãî ñâåðõñëîâà ïðèíàäëåæàò ìíî-
æåñòâó Q F t( ( )) , à â ñèëó óòâåðæäåíèÿ 6 ìîäåëè èç M S( )1 ñîäåðæàòñÿ ñðåäè
M tF t( ( ))� . Àíàëîãè÷íî òîìó, êàê ýòî ñäåëàíî âûøå, ìîæíî ïîêàçàòü, ÷òî äëÿ ëþ-
áîãî �-ñóôôèêñà ìîäåëè èç M tF t( ( ))� , íå ïðèíàäëåæàùåé M S( )1 , ñóùåñòâóåò
ìîäåëü èç M S( )1 ñ òàêèì æå �-ñóôôèêñîì.
ÏÐÅÎÁÐÀÇÎÂÀÍÈÅ ÑÏÅÖÈÔÈÊÀÖÈÈ
 îñíîâå îïèñàííûõ âûøå ïðîöåäóð ïðåîáðàçîâàíèÿ ôîðìóëû f tz ( ) ëåæàò îïå-
ðàöèè ïîñòðîåíèÿ ìíîæåñòâà ñîñòîÿíèé èç Q Q F t ( ( )), íåïîñðåäñòâåííî ñëåäóþ-
ùèõ çà çàäàííûì ìíîæåñòâîì ñîñòîÿíèé Q Q1 � , è îïåðàöèÿ ïîñòðîåíèÿ ìíî-
æåñòâà âñåõ ñîñòîÿíèé èç Q, äîñòèæèìûõ èç çàäàííîãî ìíîæåñòâà ñîñòîÿíèé.
Ðàññìîòðèì, êàê ýòè îïåðàöèè âûïîëíÿþòñÿ íà óðîâíå ïðåîáðàçîâàíèé ôîðìóë,
çàäàþùèõ ñîîòâåòñòâóþùèå ìíîæåñòâà ñîñòîÿíèé. Ìíîæåñòâî ñîñòîÿíèé èç
Q Q F t ( ( )), íåïîñðåäñòâåííî ñëåäóþùèõ çà ñîñòîÿíèÿìè èç Q Q F t1 1 ( ( )), ðàâíî
N Q Q( )1 � . Íà óðîâíå ôîðìóë ýòà îïåðàöèÿ âûãëÿäèò êàê N F t F t( ( ))& ( )1 , ãäå
ôîðìóëà N F t( ( ))1 çàäàåò ìíîæåñòâî âñåõ òåõ ñîñòîÿíèé èç Q r( , )
, êîòîðûå íå-
ïîñðåäñòâåííî ñëåäóþò çà ñîñòîÿíèÿìè èç ìíîæåñòâà, çàäàâàåìîãî ôîðìóëîé
F t1 ( ) . Äëÿ ôîðìóëû F t( ) ãëóáèíû r, çàäàííîé â ä.í.ô., N F t( ( )) ïîëó÷àåòñÿ, åñëè
â êàæäîé ýëåìåíòàðíîé êîíúþíêöèè ôîðìóëû F t( ) óäàëèòü âñå ëèòåðû ìèíè-
ìàëüíîãî ðàíãà (ò.å. ðàíãà
r) è ïîëó÷åííóþ ä.í.ô. ñäâèíóòü íà 1 âëåâî [9].
Ïîñòðîåíèå ôîðìóëû, çàäàþùåé ìíîæåñòâî âñåõ òåõ ñîñòîÿíèé èç Q F t( ( )) ,
êîòîðûå äîñòèæèìû èç åãî ïîäìíîæåñòâà Q Q F t0 0 ( ( )), îñóùåñòâëÿåòñÿ ñëå-
äóþùèì îáðàçîì. Ñíà÷àëà ñòðîèòñÿ ôîðìóëà F t N F t F t1 0( ) ( ( ))& ( ) , çàòåì, íà-
÷èíàÿ ñ i 1, èòåðàòèâíî âû÷èñëÿþòñÿ F t N F t F t F ti i i� �1 ( ) ( ( ))& ( ) ( ) äî ñòàáèëè-
çàöèè ôîðìóëû.
Ïðè íàëè÷èè òîëüêî îäíîé �-ïîäôîðìóëû â èñõîäíîé ñïåöèôèêàöèè ïðåîáðàçî-
âàíèå ôîðìóëû f tz ( ) ñâîäèòñÿ ê ïîñòðîåíèþ ìàêñèìàëüíîãî ïîäìíîæåñòâà D D*
� 0 ,
âñå ñîñòîÿíèÿ êîòîðîãî äîñòèæèìû èç D* . Ïðè ýòîì äëÿ i �0 1 2, , , ñòðîèòñÿ ïîñëå-
äîâàòåëüíîñòü ìíîæåñòâ D N D Di i i�
�
�1 ( ) äî òåõ ïîð, ïîêà äëÿ íåêîòîðîãî j íå
áóäåò ïîëó÷åíî D Dj j� 1 . Åñëè D j �, òî M S( )2 íå ñîäåðæèò ìîäåëåé èç M S( )1 è,
ñëåäîâàòåëüíî, ñïåöèôèêàöèÿ S1 ïðîòèâîðå÷èâà; åñëè D j � �, òî D Dj
* .
Ïðè íàëè÷èè äâóõ �-ïîäôîðìóë â èñõîäíîé ñïåöèôèêàöèè ïðåîáðàçîâàíèå
ôîðìóëû f tz ( ) ñâîäèòñÿ ê ïîñòðîåíèþ ïàðû ìàêñèìàëüíûõ ïîäìíîæåñòâ Q D1 1�
è Q D2 2� òàêèõ, ÷òî âñå ñîñòîÿíèÿ èç Q1 äîñòèæèìû èç Q2 , à âñå ñîñòîÿíèÿ èç Q2
äîñòèæèìû èç Q1. Íåòðóäíî ïîêàçàòü, ÷òî òàêèå ïîäìíîæåñòâà ñîäåðæàò ïî êðàéíåé
ìåðå îäíó ïàðó ñîñòîÿíèé q Q1 1� è q Q2 2� , êîòîðûå äîñòèæèìû îäíî èç äðóãîãî.
Ïóñòü Q — ìíîæåñòâî ñîñòîÿíèé, çàäàâàåìîå ôîðìóëîé f tz ( ), à Q D10 1 è
Q D20 2 . Ñòðîèì ìíîæåñòâî âñåõ òåõ ñîñòîÿíèé èç Q, êîòîðûå äîñòèæèìû èç Q10
( ( )N Q�
10 ), è áåðåì åãî ïåðåñå÷åíèÿ ñ Q10 è Q20 .  ðåçóëüòàòå ïîëó÷èì ìíîæåñòâà
Q Q11 10� è Q Q21 20� . Çàòåì ñòðîèì ìíîæåñòâî N Q� ( )21 è áåðåì åãî ïåðåñå÷åíèÿ
ñ Q11 è Q21, ÷òî äàåò ìíîæåñòâà Q Q12 11� è Q Q22 21� , è ò.ä. Â ðåçóëüòàòå òàêîãî
ïðîöåññà ïîëó÷àþòñÿ äâå ïîñëåäîâàòåëüíîñòè: Q Q Q10 11 12� � �� è
Q Q Q20 21 22� � �� Ïðîöåññ çàêàí÷èâàåòñÿ, êîãäà õîòÿ áû îäíî èç ìíîæåñòâ ýòèõ
ïîñëåäîâàòåëüíîñòåé ñòàíåò ïóñòûì, ÷òî ñâèäåòåëüñòâóåò î ïðîòèâîðå÷èâîñòè èñ-
õîäíîé ñïåöèôèêàöèè, ëèáî â êàæäîé ïîñëåäîâàòåëüíîñòè òðè ïîñëåäíèõ ìíîæåñ-
òâà áóäóò ðàâíû ìåæäó ñîáîé. Ôîðìóëà, çàäàþùàÿ ìíîæåñòâî âñåõ òåõ ñîñòîÿíèé
èç Q, êîòîðûå äîñòèæèìû èç ñîñòîÿíèé ïîñëåäíåãî ìíîæåñòâà ëþáîé ïîñëåäîâà-
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4 67
òåëüíîñòè, ïðåäñòàâëÿåò ñîáîé ðåçóëüòàò òðåáóåìîãî ïðåîáðàçîâàíèÿ ôîðìóëû
f tz ( ) . Î÷åâèäíî, ÷òî ïðèâåäåííûé àëãîðèòì ëåãêî ðàñïðîñòðàíÿåòñÿ íà ñëó÷àé íà-
ëè÷èÿ k � 2 �-ïîäôîðìóë â èñõîäíîé ñïåöèôèêàöèè. Îáîçíà÷èì Q Qk10 0, ,� ìíî-
æåñòâà ñîñòîÿíèé, çàäàâàåìûå ñîîòâåòñòâåííî ôîðìóëàìè f t tz ( )& ( )��1 ,…
... , ( )& ( )f t tz k�� . Ïðîöåññ âû÷èñëåíèÿ ñîñòîèò â ïîñòðîåíèè äëÿ j k �1, , ïîñëå-
äîâàòåëüíîñòåé Q Q Qj j j0 1 2� � �� Íà i-é èòåðàöèè ( , , )i �1 2 âû÷èñëÿþòñÿ
î÷åðåäíûå k ÷ëåíîâ ýòèõ ïîñëåäîâàòåëüíîñòåé â ñîîòâåòñòâèè ñ ôîðìóëîé
Q N Q Qji s i i j i �
�
( )( ) ( )1 , ãäå s i i k j k( ) ( ) , , ,
� �1 1 1mod . Îêîí÷àíèå ïðîöåññà
îïðåäåëÿåòñÿ ðàâåíñòâîì ïîñëåäíèõ k � 1 ÷ëåíîâ êàæäîé ïîñëåäîâàòåëüíîñòè.
Ïðèìåð 2. Èñõîäíàÿ ñïåöèôèêàöèÿ S èìååò âèä � � �t t t t( ( )1 1 � �x t( )1
�
y t x t( ))&( ( )1 ��x t( )). Ðàññìîòðèì ïîñëåäîâàòåëüíîñòü åå ïðåîáðàçîâàíèé â àâòî-
ìàòíî ýêâèâàëåíòíóþ îòíîñèòåëüíî åå ñèãíàòóðû ñïåöèôèêàöèþ â ÿçûêå L.
Ñïåöèôèêàöèÿ S1 ïðåäñòàâëÿåò ñîáîé ôîðìóëó � � �t S t t z tz ( ) ( ( ) y t( ))&
&( ( ) ( ))&( ( ) ( ) ( ))x t x t z t t t t x t
� � � � � �1 1 1 1 . Ôîðìóëà f tz ( ) â ñîîòâåòñòâóþùåé
ñïåöèôèêàöèè S 2 èìååò âèä ( ( ) ( ))&( ( ) ( ))&( ( )z t y t x t x t z t�
� � �1 ( ( )z t
�1
��
� �
�x t z t x t z t z t x t x t y t z( ))) ( ) ( ) ( ) ( ) ( ) ( ) ( ) (1 1 1 1 t x t z t) ( ) ( )� � . Ôîðìóëà �( )t
x t z t( ) ( ) õàðàêòåðèçóåò �-ïðåôèêñû ìîäåëåé èç M S( )2 , îòñóòñòâóþùèõ â M S( )1 .
Ôîðìóëà D t0 ( ), çàäàþùàÿ ìíîæåñòâî ñîñòîÿíèé D Q f t tz0 �( ( )& ( ))� , ðàâíà
f t t z t x t x t y t z t x t z tz ( )& ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )� �
� � �� 1 1 . Ïîñòðîèì òåïåðü ôîðìóëó
D t* ( ) , çàäàþùóþ ìíîæåñòâî ñîñòîÿíèé D* . Ïðè ýòîì îäíîâðåìåííî áóäåò ïîñòðî-
åíà ôîðìóëà F t( ) , çàäàþùàÿ N D� ( )* .
Ñíà÷àëà ñòðîèì ôîðìóëó D t1 ( ) :
N D t x t z t x t y t z t( ( )) ( ) ( ) ( ) ( ) ( )0 1 1 1 1 1 �
�
�
;
F t N D t f t x t z t x t z tz1 0 1 1( ) ( ( ))& ( ) ( ) ( ) ( ) ( ) �
� �
�
�
� �
�
x t y t z t x t z t x t y t z t x( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )1 1 1 1 1 1 ( ) ( ) ( )t y t z t� .
Ïîñêîëüêó N F t N D t( ( )) ( ( ))1 0 , èìååì F t N F t f tz2 1( ) ( ( ))& ( ) � F t F t1 1( ) ( )
è, ñëåäîâàòåëüíî, N D t F t�
( ( )) ( )0 1 . Òàêèì îáðàçîì, D t1 ( ) N D t� ( ( ))&0 D t0 ( )
�
� �
�
�x t z t x t z t x t y t z t x t z( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) (1 1 1 1 1 t x t y t z t) ( ) ( ) ( )&�
�
1 1 1
& ( ) ( ) ( )x t y t z t� .
Ïðè ïîñòðîåíèè D t2 ( ) ïîëó÷èì N D t x t z t( ( )) ( ) ( )1 1 1 �
� x t y t( ) ( )
1 1
�
z t N D t( ) ( ( ))1 0 , ïîýòîìó N D t N D t F t� �
( ( )) ( ( )) ( )1 0 1 . Òàêèì îáðàçîì,
D t2 ( ) N D t D t D t�
( ( ))& ( ) ( )1 1 1 , ñëåäîâàòåëüíî, D t D t* ( ) ( ) 1 , à çíà÷èò,
F t N D t F t( ) ( ( )) ( )
�
1 1 .
Ãðàô àâòîìàòà, ñïåöèôèöèðóåìîãî
ôîðìóëîé �tF t( ) , ïðèâåäåí íà ðèñ. 1.
Çàìåòèì, ÷òî àâòîìàò, ñèíòåçèðî-
âàííûé ïî ôîðìóëå S 2 , ïîëó÷åííîé
â ðåçóëüòàòå ýëèìèíàöèè êâàíòîðîâ,
èìååò òðè ñîñòîÿíèÿ, èç êîòîðûõ îäíî
ôèêòèâíîå.
ÇÀÊËÞ×ÅÍÈÅ
 èñïîëüçóåìîì ïîäõîäå ê äîêàçàòåëüíîìó ïðîåêòèðîâàíèþ ðåàêòèâíûõ àëãî-
ðèòìîâ ÿçûêîì èñõîäíîé ñïåöèôèêàöèè ÿâëÿåòñÿ ëîãè÷åñêèé ÿçûê L* ñ äîñòà-
òî÷íûìè äëÿ ïðàêòè÷åñêèõ çàäà÷ âûðàçèòåëüíûìè âîçìîæíîñòÿìè. Îäíàêî áîëü-
øèíñòâî ìåòîäîâ ïðîåêòèðîâàíèÿ, òàêèõ êàê ïðîâåðêà íåïðîòèâîðå÷èâîñòè ñïå-
öèôèêàöèé, èõ äåòåðìèíèçàöèÿ, ïðîâåðêà ðåàëèçóåìîñòè îòêðûòîé ñèñòåìû,
âåðèôèêàöèÿ è äðóãèå, ðàçðàáîòàíû äëÿ ñïåöèôèêàöèé â áîëåå ïðîñòîì ÿçûêå L,
÷òî ïîçâîëèëî ïîëó÷èòü ïðèåìëåìóþ ýôôåêòèâíîñòü ýòèõ ìåòîäîâ. Ïîýòîìó
âàæíîå çíà÷åíèå èìååò ïðåîáðàçîâàíèå ñïåöèôèêàöèè èç ÿçûêà L* â ÿçûê L.
68 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4
zx
1
zxyzx
2
Ðèñ. 1
Ó÷èòûâàÿ, ÷òî â ÿçûêå L ìîãóò áûòü ñïåöèôèöèðîâàíû òîëüêî àâòîìàòû ñ êî-
íå÷íîé ïàìÿòüþ, òàêîå ïðåîáðàçîâàíèå ïðåäïîëàãàåò ïåðåõîä îò ñïåöèôèêàöèè
àâòîìàòà, íå îáëàäàþùåãî êîíå÷íîé ïàìÿòüþ, ê ñïåöèôèêàöèè ñîîòâåòñòâóþùå-
ãî àâòîìàòà ñ êîíå÷íîé ïàìÿòüþ.  íàñòîÿùåé ðàáîòå ïðåäëîæåí ìåòîä ïðåîáðà-
çîâàíèÿ ñïåöèôèêàöèè â ÿçûêå L* â ñïåöèôèêàöèþ â ÿçûêå L, àâòîìàòíî ýêâèâà-
ëåíòíóþ èñõîäíîé ñïåöèôèêàöèè îòíîñèòåëüíî åå ñèãíàòóðû. Òàêîå ïðåîáðàçî-
âàíèå îñóùåñòâëÿåòñÿ â òðè ýòàïà. Íà ïåðâîì ýòàïå ñïåöèôèêàöèÿ â ÿçûêå L* çà
ñ÷åò ââåäåíèÿ äîïîëíèòåëüíûõ ïðåäèêàòíûõ ñèìâîëîâ ïðåîáðàçóåòñÿ â ýêâèâà-
ëåíòíóþ îòíîñèòåëüíî åå ñèãíàòóðû ñïåöèôèêàöèþ â ýòîì æå ÿçûêå, íî ñïåöè-
ôèöèðóþùóþ àâòîìàò ñ êîíå÷íîé ïàìÿòüþ. Íà âòîðîì ýòàïå ïîëó÷åííàÿ ñïåöè-
ôèêàöèÿ àâòîìàòà ñ êîíå÷íîé ïàìÿòüþ ïðåîáðàçóåòñÿ â ñïåöèôèêàöèþ â ÿçûêå L.
Ýòî ïðîñòîå ñèíòàêñè÷åñêîå ïðåîáðàçîâàíèå äàåò ñïåöèôèêàöèþ, àâòîìàòíî íå ýê-
âèâàëåíòíóþ ïðåîáðàçóåìîé ñïåöèôèêàöèè â ÿçûêå L* . Íà òðåòüåì ýòàïå ñïåöè-
ôèêàöèÿ â ÿçûêå L ïðåîáðàçóåòñÿ â ñïåöèôèêàöèþ â ýòîì æå ÿçûêå, àâòîìàòíî
ýêâèâàëåíòíóþ ñïåöèôèêàöèè àâòîìàòà ñ êîíå÷íîé ïàìÿòüþ â ÿçûêå L* .
Òàêèì ïóòåì ðåøàåòñÿ íåñêîëüêî ïðîáëåì: óñòðàíÿåòñÿ íåîáõîäèìîñòü ïðî-
âåðêè ñîñòîÿíèé ñèíòåçèðîâàííîãî àâòîìàòà íà ôèêòèâíîñòü; ïðîâåðêà íåïðîòèâî-
ðå÷èâîñòè ñïåöèôèêàöèè â ÿçûêå L* ñâîäèòñÿ ê ïðîâåðêå íåïðîòèâîðå÷èâîñòè ñïå-
öèôèêàöèè â ÿçûêå L, äëÿ êîòîðîé ðàçðàáîòàíû ýôôåêòèâíûå ìåòîäû; ïîÿâëÿåòñÿ
âîçìîæíîñòü ïðèìåíåíèÿ ìåòîäîâ ñèíòåçà ê ñïåöèôèêàöèÿì, íå óäîâëåòâîðÿþùèì
òåîðåìå î ñïåöèôèêàöèè [4]. Â ñâÿçè ñ ýòèì â ñòàòüå ðàññìîòðåí ðàñøèðåííûé âà-
ðèàíò ÿçûêà L* , âûõîäÿùèé çà ðàìêè òðåáîâàíèé òåîðåìû î ñïåöèôèêàöèè, íà êî-
òîðîé áûëè îñíîâàíû âñå ìåòîäû ñèíòåçà, èñïîëüçîâàâøèåñÿ äëÿ ÿçûêà L* . Ðàñøè-
ðåíèå ÿçûêà L* ñîñòîèò â òîì, ÷òî â êà÷åñòâå ïîäôîðìóë, âõîäÿùèõ â �-ôîðìóëû
ÿçûêà, ìîãóò áûòü íå òîëüêî �-ôîðìóëû è ôîðìóëû ÿçûêà L, íî è ïðîèçâîëüíûå
ôîðìóëû ÿçûêà L* .
ÑÏÈÑÎÊ ËÈÒÅÐÀÒÓÐÛ
1. × å á î ò à ð å â À . Í . Ðàñøèðåíèå ëîãè÷åñêîãî ÿçûêà ñïåöèôèêàöèè è ïðîáëåìà ñèíòåçà // Êèáåð-
íåòèêà è ñèñòåìíûé àíàëèç. — 1996. — ¹ 6. — Ñ. 11–27.
2. × å á î ò à ð å â À . Í . Îá îäíîì ïîäõîäå ê ôóíêöèîíàëüíîé ñïåöèôèêàöèè àâòîìàòíûõ ñèñòåì // Òàì
æå. — 1993. — ¹ 3. — Ñ. 31–42.
3. à è ë ë À . Ââåäåíèå â òåîðèþ êîíå÷íûõ àâòîìàòîâ. — Ì.: Íàóêà, 1966. — 227 ñ.
4. × å á î ò à ð å â À . Í . Ñèíòåç ïðîöåäóðíîãî ïðåäñòàâëåíèÿ àâòîìàòà, ñïåöèôèöèðîâàííîãî â ëîãè-
÷åñêîì ÿçûêå L*. I // Êèáåðíåòèêà è ñèñòåìíûé àíàëèç. — 1997. — ¹ 4. — Ñ. 60–74.
5. × å á î ò à ð å â À . Í . Ñèíòåç ïðîöåäóðíîãî ïðåäñòàâëåíèÿ àâòîìàòà, ñïåöèôèöèðîâàííîãî â ëîãè-
÷åñêîì ÿçûêå L*. II // Òàì æå. — 1997. — ¹ 6. — Ñ. 115–127.
6. × å á î ò à ð å â À . Í . Ñèíòåç àëãîðèòìà ïî åãî ëîãè÷åñêîé ñïåöèôèêàöèè // Óïðàâëÿþùèå ñèñòåìû è
ìàøèíû. — 2004. — ¹ 5. — Ñ. 53–60.
7. × å á î ò à ð å â À . Í . Ñèíòåç íåäåòåðìèíèðîâàííîãî àâòîìàòà ïî åãî ëîãè÷åñêîé ñïåöèôèêàöèè. I //
Êèáåðíåòèêà è ñèñòåìíûé àíàëèç. — 1995. — ¹ 5. — Ñ. 3–15.
8. × å á î ò à ð å â À . Í . Î êëàññå ôîðìóë ÿçûêà L*, ñïåöèôèöèðóþùèõ àâòîìàòû ñ êîíå÷íîé ïàìÿòüþ //
Òàì æå. — 2010. — ¹ 1. — Ñ. 3–9.
9. × å á î ò à ð å â À . Í . , Ê ó ð è â ÷ à ê Î . È . Àïïðîêñèìàöèÿ ìíîæåñòâ ñâåðõñëîâ ôîðìóëàìè ÿçûêà L
// Òàì æå. — 2007. — ¹ 6. — Ñ. 18–26.
Ïîñòóïèëà 22.04.2009
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4 69
|