Анализ фиктивности состояний автомата, синтезированного по спецификации, преобразованной из языка L* в язык L
Розглянуто метод синтезу скінченного автомата, специфікованого логічною мовою L*. Цей метод базується на трансляції специфікації у менш виразну мову L і застосуванні існуючого методу синтезу автомата за специфікацією у цій мові. Автомат, що синтезується у такий спосіб, може мати зайві (фіктивні) ста...
Збережено в:
| Опубліковано в: : | Кибернетика и системный анализ |
|---|---|
| Дата: | 2013 |
| Автор: | |
| Формат: | Стаття |
| Мова: | Російська |
| Опубліковано: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2013
|
| Теми: | |
| Онлайн доступ: | https://nasplib.isofts.kiev.ua/handle/123456789/86159 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Цитувати: | Анализ фиктивности состояний автомата, синтезированного по спецификации, преобразованной из языка L* в язык L / А.Н. Чеботарев // Кибернетика и системный анализ. — 2013. — Т. 49, № 1. — С. 3-10. — Бібліогр.: 8 назв. — рос. |
Репозитарії
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1859649257955393536 |
|---|---|
| author | Чеботарев, А.Н. |
| author_facet | Чеботарев, А.Н. |
| citation_txt | Анализ фиктивности состояний автомата, синтезированного по спецификации, преобразованной из языка L* в язык L / А.Н. Чеботарев // Кибернетика и системный анализ. — 2013. — Т. 49, № 1. — С. 3-10. — Бібліогр.: 8 назв. — рос. |
| collection | DSpace DC |
| container_title | Кибернетика и системный анализ |
| description | Розглянуто метод синтезу скінченного автомата, специфікованого логічною мовою L*. Цей метод базується на трансляції специфікації у менш виразну мову L і застосуванні існуючого методу синтезу автомата за специфікацією у цій мові. Автомат, що синтезується у такий спосіб, може мати зайві (фіктивні) стани, які мають бути вилученими. Запропоновано простий метод перевірки станів на фіктивність.
A method for synthesizing an FSM specified in the logical language L* is considered. The method is based on translating the specification into the less expressive language L and applying the available method for synthesizing an FSM from the specification in this language. The resulting FSM may contain extra states called fictitious that have to be deleted. A simple method for checking the states for fictitiousness is proposed.
|
| first_indexed | 2025-12-07T13:31:32Z |
| format | Article |
| fulltext |
À.Í. ×ÅÁÎÒÀÐÅÂ
ÓÄÊ 519.713.1 ÀÍÀËÈÇ ÔÈÊÒÈÂÍÎÑÒÈ ÑÎÑÒÎßÍÈÉ
ÀÂÒÎÌÀÒÀ, ÑÈÍÒÅÇÈÐÎÂÀÍÍÎÃÎ
ÏÎ ÑÏÅÖÈÔÈÊÀÖÈÈ, ÏÐÅÎÁÐÀÇÎÂÀÍÍÎÉ
ÈÇ ßÇÛÊÀ L*  ßÇÛÊ L
Êëþ÷åâûå ñëîâà: ÿçûê ñïåöèôèêàöèè L*, �-ôîðìóëà, îáðàòíîå ñâåðõñëîâî,
ýëèìèíàöèÿ êâàíòîðîâ, ñèíòåç àâòîìàòà, ôèêòèâíîå ñîñòîÿíèå.
ÂÂÅÄÅÍÈÅ
Ðàññìàòðèâàåìûé ïîäõîä ê äîêàçàòåëüíîìó ïðîåêòèðîâàíèþ ðåàêòèâíûõ àëãî-
ðèòìîâ îñíîâàí íà ñïåöèôèêàöèè ôóíêöèîíàëüíûõ ñâîéñòâ àëãîðèòìà â ÿçûêå
ëîãèêè ïåðâîãî ïîðÿäêà ñ îäíîìåñòíûìè ïðåäèêàòàìè è ôîðìàëüíîì ïåðåõîäå
îò ñïåöèôèêàöèè ê ïðîöåäóðíîìó ïðåäñòàâëåíèþ àëãîðèòìà. Îäíà èç ïðî-
áëåì, ñâÿçàííûõ ñî ñïåöèôèêàöèåé ñâîéñòâ àëãîðèòìà, ñîñòîèò â ðàçðàáîòêå
ïîäõîäÿùåãî ÿçûêà ñïåöèôèêàöèè. Ïîñêîëüêó ñ óâåëè÷åíèåì âûðàçèòåëüíîñòè
ÿçûêà ðàñòåò ñëîæíîñòü àëãîðèòìîâ ïðîåêòèðîâàíèÿ, íåîáõîäèìî íàéòè êîì-
ïðîìèññ ìåæäó âûðàçèòåëüíîñòüþ ÿçûêà è ñëîæíîñòüþ ïðîåêòèðîâàíèÿ. Äëÿ
ýòîãî èñïîëüçóþòñÿ äâà óðîâíÿ ÿçûêà: ÿçûê èñõîäíîé ñïåöèôèêàöèè L* [1],
îáëàäàþùèé äîñòàòî÷íûìè äëÿ ïðàêòè÷åñêèõ íóæä âûðàçèòåëüíûìè âîçìîæ-
íîñòÿìè è îáåñïå÷èâàþùèé óäîáñòâî çàïèñè ôóíêöèîíàëüíûõ òðåáîâàíèé
ê àëãîðèòìó, è ÿçûê L [2], ñî ñðàâíèòåëüíî îãðàíè÷åííûìè âûðàçèòåëüíûìè
âîçìîæíîñòÿìè, íî ýôôåêòèâíî îáðàáàòûâàåìûé ïðîöåäóðàìè ñèíòåçà.
Àâòîìàòíûé ïîäõîä ê ïðîåêòèðîâàíèþ ðåàêòèâíîãî àëãîðèòìà õàðàêòåðèçó-
åòñÿ òåì, ÷òî â êà÷åñòâå ìîäåëè àëãîðèòìà ðàññìàòðèâàåòñÿ ñåòü âçàèìîäåéñòâóþ-
ùèõ àâòîìàòîâ. Òàêèì îáðàçîì, îñíîâíûå çàäà÷è ïðîåêòèðîâàíèÿ ñâÿçàíû ñî ñïå-
öèôèêàöèåé è ñèíòåçîì êîíå÷íûõ àâòîìàòîâ. Âîçìîæíîñòè ñïåöèôèêàöèè â ÿçû-
êå L îãðàíè÷åíû àâòîìàòàìè ñ êîíå÷íîé ïàìÿòüþ [3], ÷òî ïîçâîëèëî ðàçðàáîòàòü
äëÿ íåãî ýôôåêòèâíûå àëãîðèòìû ñèíòåçà, ïðîâåðêè íåïðîòèâîðå÷èâîñòè ñïåöè-
ôèêàöèè è âåðèôèêàöèè òåìïîðàëüíûõ ñâîéñòâ, à òàêæå ìåòîäû ïðîåêòèðîâàíèÿ
îòêðûòûõ ñèñòåì, ê êîòîðûì îòíîñÿòñÿ ðåàêòèâíûå àëãîðèòìû. Ïîýòîìó ÿçûê L*
èñïîëüçóåòñÿ (ïðè íåîáõîäèìîñòè) äëÿ íà÷àëüíîé ñïåöèôèêàöèè àâòîìàòîâ.
Ðàññìàòðèâàåìûé ìåòîä ñèíòåçà àâòîìàòà ïî ñïåöèôèêàöèè â ÿçûêå L*
îñíîâàí íà ïåðåõîäå îò íåå ê ñïåöèôèêàöèè â ÿçûêå L [4].  ðåçóëüòàòå ïîëó÷à-
åòñÿ ñïåöèôèêàöèÿ, íå ýêâèâàëåíòíàÿ èñõîäíîé, îäíàêî, êàê ïîêàçàíî â [4], ñèí-
òåçèðîâàííûé ïî íåé àâòîìàò ñîäåðæèò ïîäàâòîìàò, ñîâïàäàþùèé ñ àâòîìàòîì,
ñïåöèôèöèðîâàííûì â ÿçûêå L*. Ñîñòîÿíèÿ, íå ïðèíàäëåæàùèå ýòîìó ïîäàâòî-
ìàòó, íàçûâàþòñÿ ôèêòèâíûìè. Çàäà÷à ñîñòîèò â óäàëåíèè èç ñèíòåçèðîâàííîãî
àâòîìàòà âñåõ ôèêòèâíûõ ñîñòîÿíèé. Â [5] ðàññìîòðåí ìåòîä îïðåäåëåíèÿ ôèê-
òèâíîñòè ñîñòîÿíèÿ ïóòåì ïðîâåðêè âûïîëíèìîñòè â íåì ôîðìóë ÿçûêà L*. Â íà-
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 1 3
© À.Í. ×åáîòàðåâ, 2013
ñòîÿùåé ðàáîòå íà îñíîâå ðåçóëüòàòîâ, ïîëó÷åííûõ â [6], ïðåäëàãàåòñÿ ôèêòèâ-
íîñòü ñîñòîÿíèÿ îïðåäåëÿòü ñ ïîìîùüþ ïðîâåðêè âûïîëíèìîñòè â ñîñòîÿíèè
äîñòàòî÷íî ïðîñòîé ôîðìóëû ÿçûêà L, ÷òî ñóùåñòâåííî óìåíüøàåò ñëîæíîñòü
ïðîöåäóðû îïðåäåëåíèÿ ôèêòèâíîñòè ñîñòîÿíèÿ.
ßÇÛÊÈ ÑÏÅÖÈÔÈÊÀÖÈÈ L È L*
ßçûêè L è L* ïîñòðîåíû íà îñíîâå ñîîòâåòñòâóþùèõ ôðàãìåíòîâ ëîãèêè
ïðåäèêàòîâ ïåðâîãî ïîðÿäêà ñ îäíîìåñòíûìè ïðåäèêàòàìè, îïðåäåëåííûìè íà
ìíîæåñòâå ìîìåíòîâ äèñêðåòíîãî âðåìåíè, â êà÷åñòâå êîòîðîãî âûñòóïàåò
ìíîæåñòâî Z öåëûõ ÷èñåë. Ñïåöèôèêàöèÿ â îáîèõ ÿçûêàõ èìååò âèä ôîðìóëû
�tF t( ), ãäå F t( ) — ôîðìóëà ñ îäíîé ñâîáîäíîé ïåðåìåííîé t. Â ÿçûêå L ôîð-
ìóëà F t( ) ñòðîèòñÿ ñ ïîìîùüþ ëîãè÷åñêèõ ñâÿçîê èç àòîìîâ âèäà p t k( )� , ãäå
p — îäíîìåñòíûé ïðåäèêàòíûé ñèìâîë, t — ïåðåìåííàÿ, ïðèíèìàþùàÿ çíà-
÷åíèÿ èç ìíîæåñòâà Z , à k — öåëî÷èñëåííàÿ êîíñòàíòà (ñäâèã âî âðåìåíè).
ßçûê L* îòëè÷àåòñÿ îò ÿçûêà L òåì, ÷òî ïðè ïîñòðîåíèè ôîðìóëû F t( ) íàðÿ-
äó ñ àòîìàðíûìè ôîðìóëàìè èñïîëüçóþòñÿ ôîðìóëû âèäà
� � � � � � � � �t t t k F t t t k t t k F ti i i j i j j( )& ( )& (( ) ( ))1 1 2 3 2 ,
ãäå k k k1 2 3, , �Z , F t j2 ( ) — ôîðìóëà ÿçûêà L, à F ti1 ( ) — ôîðìóëà ÿçûêà L*.
Òàêèå ôîðìóëû áóäåì íàçûâàòü �-ôîðìóëàìè. Äëÿ èõ ýêâèâàëåíòíîãî ïðåîá-
ðàçîâàíèÿ ÷àñòî èñïîëüçóåòñÿ ðàâíîñèëüíîñòü [4]
F t F t h t g t( ) ( ( )& ( ) ( ))�
1 , (1)
ãäå F t( ) 1 îáîçíà÷àåò ôîðìóëó, ïîëó÷åííóþ èç F t( ) çàìåíîé t íà t 1 ,
h t F t k( ) ( )� �2 3 , à g t F t k F t k k( ) ( ( ) ( )� �
� � �
� �1 1 1 2 3 1 , åñëè k3
k k1 2� ,
èëè F t k F t k F t k k1 1 2 3 2 1 2( )& ( )& & ( )� � � �� , åñëè k k k3 1 2� � ). Ïðàâóþ
÷àñòü ðàâíîñèëüíîñòè (1) íàçîâåì 1-ðàçâåðòêîé �-ôîðìóëû F t( ) .
Äëÿ ôîðìóëû 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 t1 1 1� # ( ( )), r F t2 2 2� # ( ( )) ;
3) åñëè F t( ) ïîñòðîåíà èç F ti ( ), i m�1, ..., , ñ ïîìîùüþ ëîãè÷åñêèõ ñâÿçîê, òî
# ( ( )) max (# ( ( )), , # ( ( )))F t F t F tm� 1 � .
Äëÿ ôîðìóëû ÿçûêà L ðàçíîñòü ìåæäó ìàêñèìàëüíûì è ìèíèìàëüíûì çíà-
÷åíèåì ðàíãîâ âõîäÿùèõ â íåå àòîìîâ íàçûâàåòñÿ ãëóáèíîé ôîðìóëû.
Ôîðìóëû, ðàíã êîòîðûõ íå ïðåâûøàåò 0, íàçûâàþòñÿ 0-îãðàíè÷åííûìè.
Ïîñêîëüêó êàæäàÿ ôîðìóëà âèäà �tF t( ) ìîæåò áûòü ýêâèâàëåíòíî ïðåîáðàçîâà-
íà â 0-îãðàíè÷åííóþ ôîðìóëó, â äàëüíåéøåì áóäóò ðàññìàòðèâàòüñÿ òîëüêî
òàêèå ôîðìóëû.
Îáúåêòîì ñïåöèôèêàöèè è ñèíòåçà ÿâëÿåòñÿ ÷àñòè÷íûé, íåèíèöèàëüíûé, äå-
òåðìèíèðîâàííûé àâòîìàò áåç âûõîäîâ A Q A�
��, , � , ãäå � — êîíå÷íûé âõîä-
íîé àëôàâèò, Q — êîíå÷íîå ìíîæåñòâî ñîñòîÿíèé, �A Q Q: � �� — ÷àñòè÷íàÿ
ôóíêöèÿ ïåðåõîäîâ. Òàêîé àâòîìàò íàçîâåì �-àâòîìàòîì. Àâòîìàòíàÿ ñåìàíòèêà
ÿçûêîâ îïèñûâàåòñÿ â òåðìèíàõ öèêëè÷åñêèõ �-àâòîìàòîâ [4].
�-àâòîìàò A Q A�
��, , � íàçûâàåòñÿ öèêëè÷åñêèì, åñëè äëÿ êàæäîãî q Q�
ñóùåñòâóþò òàêèå � �1 2, �� è q q Q1 2, � , ÷òî q qA1 1�� �( , ) è q qA�� �( , )2 2 .
Ïîâåäåíèå öèêëè÷åñêîãî �-àâòîìàòà óäîáíî îïèñûâàòü â òåðìèíàõ ìíî-
æåñòâ ñâåðõñëîâ (�-ñëîâ) â àëôàâèòå �, ïîýòîìó ïðèâåäåì ñâÿçàííûå ñ íèìè
îïðåäåëåíèÿ.
4 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 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 � ) è îáðàòíûì
ñâåðõcëîâîì (îáîçíà÷àåòñÿ � g g g( ) ( ) ( ) 2 1 0 ) â àëôàâèòå � . Îòðåçîê
u u u k( ) ( ) ( )� � �� �1 � äâóñòîðîííåãî ñâåðõñëîâà u îáîçíà÷àåòñÿ u k( , )� � � . Áåñêî-
íå÷íûå îòðåçêè u k( , ) � è u k( , )� �1 íàçîâåì ñîîòâåòñòâåííî k-ïðåôèêñîì è
k-ñóôôèêñîì äâóñòîðîííåãî ñâåðõñëîâà u. Åñëè çíà÷åíèå k íåñóùåñòâåííî, òî
áóäåì ãîâîðèòü îá �-ïðåôèêñå è �-ñóôôèêñå. Äëÿ k �
�N ñëîâî l l k( ) ( )1 � íàçî-
âåì k-ïðåôèêñîì ñâåðõñëîâà l l l� ( ) ( )1 2 � , à îáðàòíîå ñëîâî g k g( )... ( ) �1 0 —
k-ñóôôèêñîì îáðàòíîãî ñâåðõñëîâà g g g g� � ( ) ( ) ( )2 1 0 . Îáðàòíîå ñâåðõñëîâî
� rrr, îáðàçîâàííîå ïîâòîðåíèåì ñëîâà r, îáîçíà÷èì r � .
Ñâåðõñëîâî l � � �1 2 � â àëôàâèòå � äîïóñòèìî â ñîñòîÿíèè q �-àâòîìàòà A,
åñëè ñóùåñòâóåò òàêîå ñâåðõñëîâî ñîñòîÿíèé q q q0 1 2� , ãäå q q0 � , ÷òî äëÿ ëþ-
áîãî i �1 2, , � � �A i i iq q( , )� ��1 1. Ìíîæåñòâî âñåõ ñâåðõñëîâ, äîïóñòèìûõ
â ñîñòîÿíèè q, îáîçíà÷èì W q( ) .
Îáðàòíîå ñâåðõñëîâî � � � 1 0 â àëôàâèòå � ïðåäñòàâèìî ñîñòîÿíèåì q �-àâ-
òîìàòà A , åñëè ñóùåñòâóåò òàêîå îáðàòíîå ñâåðõñëîâî ñîñòîÿíèé � q q q 2 1 0
,
ãäå q q0 � , ÷òî äëÿ ëþáîãî i � 1 2, ,� âûïîëíÿåòñÿ � �A i i iq q( , )� ��1 1. Òàêèì
îáðàçîì, ñ êàæäûì ñîñòîÿíèåì q öèêëè÷åñêîãî �-àâòîìàòà àññîöèèðóþòñÿ äâà
ìíîæåñòâà ñâåðõñëîâ: ìíîæåñòâî W q( ) âñåõ ñâåðõñëîâ, äîïóñòèìûõ â ñîñòîÿíèè q,
è ìíîæåñòâî P q( ) âñåõ îáðàòíûõ ñâåðõñëîâ, ïðåäñòàâèìûõ ñîñòîÿíèåì q. Ïîíÿ-
òèå ïðåäñòàâèìîñòè îáðàòíûõ ñâåðõñëîâ ñîñòîÿíèåì q åñòåñòâåííûì îáðàçîì
ðàñïðîñòðàíÿåòñÿ íà èõ k-ñóôôèêñû (îáðàòíûå ñëîâà äëèíû k).
Ïîâåäåíèå àâòîìàòà A ñ ìíîæåñòâîì ñîñòîÿíèé Q q qA n� { }1, ..., ïðåäñòàâ-
ëÿåò ñîáîé ñåìåéñòâî ìíîæåñòâ ñâåðõñëîâ S A W Wn( ) ( , , )� 1 � , ãäå W W qi i� ( )
( , , )i n�1 � .
Äâà íåèíèöèàëüíûõ �-àâòîìàòà, A1 è A2 , ñ ïîâåäåíèÿìè ñîîòâåòñòâåííî
( , , )� �W Wn1 � è ( , , )�� ��W Wm1 � íàçûâàþòñÿ ñòðîãî ýêâèâàëåíòíûìè, åñëè êàæäîå �Wi
( , ,i n�1 � ) ñîäåðæèòñÿ ñðåäè �� ��W Wm1, ,� è êàæäîå ��Wi (i m�1, ,� ) ñîäåðæèòñÿ
ñðåäè � �W Wn1, ,� .
Ïóñòü � � { }p pm1, ,� — ìíîæåñòâî âñåõ ïðåäèêàòíûõ ñèìâîëîâ, âñòðå÷àþ-
ùèõñÿ â ôîðìóëå F (ñèãíàòóðà ôîðìóëû). Èíòåðïðåòàöèÿ ôîðìóëû F — ýòî óïî-
ðÿäî÷åííûé íàáîð îïðåäåëåííûõ íà Z îäíîìåñòíûõ ïðåäèêàòîâ � �1, ,� m , ñîîò-
âåòñòâóþùèõ ïðåäèêàòíûì ñèìâîëàì èç � . Èíòåðïðåòàöèþ I m�
�� �1, ,�
ìîæíî ïðåäñòàâèòü â âèäå äâóñòîðîííåãî ñâåðõñëîâà â àëôàâèòå � �( ), ÿâëÿþ-
ùåìñÿ ìíîæåñòâîì âñåõ äâîè÷íûõ âåêòîðîâ ðàçìåðíîñòè m. Êàæäûé òàêîé âåê-
òîð îïðåäåëÿåò çíà÷åíèÿ ïðåäèêàòîâ � �1, ,� m â íåêîòîðûé ìîìåíò âðåìåíè.
Ñèìâîëû àëôàâèòà � �( ) èíîãäà óäîáíî ðàññìàòðèâàòü êàê îòîáðàæåíèÿ âèäà
�: ,� � { }0 1 . Ïóñòü � �1 � . Ïðîåêöèåé ñèìâîëà � �� �( ) íà �1 íàçîâåì îãðàíè-
÷åíèå îòîáðàæåíèÿ � íà �1. Ïîíÿòèå ïðîåêöèè ñèìâîëà íà �1 åñòåñòâåííûì îá-
ðàçîì ðàñïðîñòðàíÿåòñÿ íà ñëîâà è ñâåðõñëîâà, òàê ÷òî ïðîåêöèÿ ñâåðõñëîâà â àë-
ôàâèòå � �( ) íà �1 åñòü ñâåðõñëîâî â àëôàâèòå � �( )1 . Â äàëüíåéøåì íå áóäåì
ðàçëè÷àòü èíòåðïðåòàöèè è ñîîòâåòñòâóþùèå èì äâóñòîðîííèå ñâåðõñëîâà, ïîý-
òîìó ìîæíî ãîâîðèòü îá èñòèííîñòíîì çíà÷åíèè çàìêíóòîé ôîðìóëû F íà äâó-
ñòîðîííåì ñâåðõñëîâå u è çíà÷åíèè ôîðìóëû F t( ) â íåêîòîðîé ïîçèöèè � äâóñòî-
ðîííåãî ñâåðõñëîâà u.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 1 5
Êàæäîé çàìêíóòîé ôîðìóëå F ñòàâèòñÿ â ñîîòâåòñòâèå ìíîæåñòâî M F( ) ìî-
äåëåé äëÿ ýòîé ôîðìóëû, ò.å. ìíîæåñòâî òàêèõ èíòåðïðåòàöèé, íà êîòîðûõ F
èñòèííà.
Îáîçíà÷èì W F( ) ìíîæåñòâî 0-ñóôôèêñîâ âñåõ ìîäåëåé èç M F( ), à P F( ) —
ìíîæåñòâî 0-ïðåôèêñîâ ýòèõ ìîäåëåé.
Äâóñòîðîííåå ñâåðõñëîâî u � íàçûâàåòñÿ k-ñäâèãîì (k �Z) äâóñòîðîííåãî
ñâåðõñëîâà u, åñëè äëÿ âñåõ t �Z âûïîëíÿåòñÿ ðàâåíñòâî � � �u t u t k( ) ( ). Åñëè u —
ìîäåëü äëÿ F , òî è ëþáîé åå k-ñäâèã ïðèíàäëåæèò M F( ) . Îòñþäà ñëåäóåò, ÷òî
ëþáîé �-ñóôôèêñ ìîäåëè äëÿ F ïðèíàäëåæèò W F( ) è ëþáîé åå �-ïðåôèêñ ïðè-
íàäëåæèò P F( ) .
Ïóñòü g P F� ( ) . Îáîçíà÷èì S g( ) ìíîæåñòâî âñåõ òàêèõ ñâåðõñëîâ, êîíêàòå-
íàöèÿ êàæäîãî èç êîòîðûõ ñ 0-ïðåôèêñîì g ñîîòâåòñòâóåò ìîäåëè äëÿ F . Òàêèå
ñâåðõñëîâà íàçîâåì äîïóñòèìûìè ïðîäîëæåíèÿìè 0-ïðåôèêñà g, à k-ïðåôèêñû
ñâåðõñëîâ èç S g( ) — äîïóñòèìûìè k-ïðîäîëæåíèÿìè g.
Ôîðìóëà F îäíîçíà÷íî îïðåäåëÿåò êîíå÷íóþ ñîâîêóïíîñòü ìíîæåñòâ ñâåðõ-
ñëîâ S F S S S m( ) , , ,� { }1 2 � [4] òàêóþ, ÷òî äëÿ êàæäîãî g P F� ( ) èìååò ìåñòî
S g S F( ) ( )� è, íàîáîðîò, äëÿ êàæäîãî S S Fi � ( ) ñóùåñòâóåò g P F� ( ) , äëÿ êîòî-
ðîãî S g S i( ) � .
Äâà �-ïðåôèêñà, g1 è g2 , ìîäåëåé äëÿ F ýêâèâàëåíòíû, åñëè S g S g( ) ( )1 2� .
Ïóñòü P P Pm1 2, , ,� — êëàññû ýêâèâàëåíòíîñòè �-ïðåôèêñîâ èç P F( ), ñîîòâåò-
ñòâóþùèå S S S m1 2, , ,� , òîãäà P S M Fi i
i
m
�
�
1
� ( ) .
Ôîðìóëå F ïîñòàâèì â ñîîòâåòñòâèå ïðèâåäåííûé àâòîìàò A F( ), ñîñòîÿíèÿ
q qm1, ,� êîòîðîãî ñîîòâåòñòâóþò êëàññàì P P Pm1 2, , ,� , à ôóíêöèÿ ïåðåõîäîâ
îïðåäåëÿåòñÿ ñëåäóþùèì îáðàçîì. Ïóñòü g — ïðîèçâîëüíûé 0-ïðåôèêñ èç Pi è
� �i ik1
, ,� — âñå äîïóñòèìûå 1-ïðîäîëæåíèÿ g, òîãäà � �( , )q qi i ij j
�
( j k�1, ,� ), ãäå q
ij
òàêîâî, ÷òî �-ïðåôèêñ g ij
� ïðèíàäëåæèò Pij
. Äëÿ âñåõ ñèìâî-
ëîâ àëôàâèòà � �( ), îòëè÷íûõ îò � �i ik1
, ,� , ïåðåõîä èç qi
íå îïðåäåëåí. Î÷åâèä-
íî, ÷òî äëÿ êàæäîãî qi (i m�1, ,� ) ñóùåñòâóåò ïî êðàéíåé ìåðå îäèí ñèìâîë, äëÿ
êîòîðîãî çíà÷åíèå ôóíêöèè ïåðåõîäîâ îïðåäåëåíî, à òàêæå ñîñòîÿíèå q j , èç êî-
òîðîãî èìååòñÿ ïåðåõîä â qi . Ñëåäîâàòåëüíî, àâòîìàò A F( ) öèêëè÷åñêèé.
Óòâåðæäåíèå 1. Ôîðìóëà F ñïåöèôèöèðóåò àâòîìàò A ñ ïîâåäåíèåì
S A W W Wn( ) ( , , , )� 1 2 � , åñëè ñóùåñòâóåò òàêîå ðàçáèåíèå { � � �P P Pn1 2, , ,� } ìíî-
æåñòâà P F( ) , ÷òî � �
�
P W M Fi i
i
n
1
� ( ) è âñå �-ïðåôèêñû, ïðèíàäëåæàùèå îäíîìó è
òîìó æå êëàññó ðàçáèåíèÿ, ýêâèâàëåíòíû. Ñïåöèôèöèðóåìûé àâòîìàò îïðåäåëÿ-
åòñÿ òàêèì æå ñïîñîáîì, êàê è A F( ) .
Îòñþäà ñëåäóåò, ÷òî êàæäîå Wi (i n�1, ,� ) ïðèíàäëåæèò S F( ) . Ïîýòîìó âñå
àâòîìàòû, ñïåöèôèöèðóåìûå ôîðìóëîé F , ñòðîãî ýêâèâàëåíòíû àâòîìàòó A F( ) .
Ïóñòü çàìêíóòûå ôîðìóëû F1 è F2 èìåþò ñîîòâåòñòâåííî ñèãíàòóðû �1 è � 2 ,
à � — íåïóñòîå ïîäìíîæåñòâî ìíîæåñòâà � �1 2� . Ôîðìóëû F1 è F2 íàçîâåì
ýêâèâàëåíòíûìè îòíîñèòåëüíî ñèãíàòóðû �, åñëè ìíîæåñòâà ïðîåêöèé âñåõ ìî-
äåëåé (äâóñòîðîííèõ ñâåðõñëîâ) èç M F( )1 è M F( )2 íà � ñîâïàäàþò.
6 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 1
ÏÅÐÅÕÎÄ ÎÒ ßÇÛÊÀ L* Ê ßÇÛÊÓ L
Ïðåîáðàçîâàíèå èñõîäíîé ñïåöèôèêàöèè â ñïåöèôèêàöèþ â ÿçûêå L îñóùå-
ñòâëÿåòñÿ â äâà ýòàïà. Íà ïåðâîì ýòàïå ñïåöèôèêàöèÿ F tF t� � ( ) â ÿçûêå L*
ïðåîáðàçóåòñÿ â òàêóþ ýêâèâàëåíòíóþ îòíîñèòåëüíî åå ñèãíàòóðû ôîðìóëó
F tF t1 1� � ( ) ÿçûêà L*, êîòîðàÿ ñïåöèôèöèðóåò àâòîìàò ñ êîíå÷íîé ïàìÿòüþ. Ïðå-
îáðàçîâàíèå F t( ) â F t1 ( ) îñíîâàíî íà ââåäåíèè äîïîëíèòåëüíûõ ïðåäèêàòíûõ ñèì-
âîëîâ äëÿ ïðåäèêàòîâ, óäîâëåòâîðÿþùèõ �-ïîäôîðìóëàì èñõîäíîé ñïåöèôèêàöèè.
Ïóñòü � i t( ) — ìàêñèìàëüíàÿ �-ïîäôîðìóëà ôîðìóëû F t( ), ò.å. ïîäôîðìóëà,
íå ñîäåðæàùàÿñÿ íè â êàêîé äðóãîé �-ïîäôîðìóëå. Êàæäàÿ òàêàÿ �-ïîäôîðìóëà
çàìåíÿåòñÿ àòîìîì âèäà z t ri i( )� , ãäå ri — ðàíã çàìåíÿåìîé �-ïîäôîðìóëû, à zi —
ïðåäèêàòíûé ñèìâîë, îòñóòñòâóþùèé â ôîðìóëå F t( ), êðîìå òîãî, â ñïåöèôèêà-
öèþ äîáàâëÿåòñÿ ýêâèâàëåíòíîñòü z t t ri i i( ) ( )� � . Åñëè �-ôîðìóëû â ïðàâûõ
÷àñòÿõ äîáàâëåííûõ ýêâèâàëåíòíîñòåé ñîäåðæàò îòëè÷íûå îò íèõ �-ïîäôîðìóëû,
òî âûïîëíÿþòñÿ òå æå äåéñòâèÿ, ÷òî è äëÿ �-ïîäôîðìóë èñõîäíîé ôîðìóëû.
Ìàêñèìàëüíûå òàêèå ïîäôîðìóëû çàìåíÿþòñÿ ñîîòâåòñòâóþùèìè îáîçíà÷åíèÿ-
ìè íîâûõ ïðåäèêàòîâ, è äîáàâëÿþòñÿ ýêâèâàëåíòíîñòè âèäà z t tj j( ) ( )� � . Òà-
êèå äåéñòâèÿ âûïîëíÿþòñÿ äî òåõ ïîð, ïîêà íè îäíà �-ôîðìóëà � j t( ) íå áóäåò
ñîäåðæàòü âõîæäåíèé �-ïîäôîðìóë, îòëè÷íûõ îò íåå.  ðåçóëüòàòå ïîëó÷àåì
ñïåöèôèêàöèþ F tF t1 1� � ( ) . Êàê ïîêàçàíî â [7], ýòà ñïåöèôèêàöèÿ ýêâèâàëåíòíà
èñõîäíîé ñïåöèôèêàöèè îòíîñèòåëüíî åå ñèãíàòóðû è ñïåöèôèöèðóåò àâòîìàò
ñ êîíå÷íîé ïàìÿòüþ. Íà âòîðîì ýòàïå â êàæäîé ýêâèâàëåíòíîñòè z t t ri i i( ) ( )� �
�-ôîðìóëà � i it r( ) çàìåíÿåòñÿ ïðàâîé ÷àñòüþ ðàâíîñèëüíîñòè (1), ãäå âûðàæå-
íèå � i it r( ) 1 çàìåíÿåòñÿ âûðàæåíèåì z ti ( ) 1 . Òàêèì îáðàçîì, ðàññìàòðè-
âàåìûå ýêâèâàëåíòíîñòè ïðèîáðåòàþò âèä z t z ti i( ) ( ( )&� 1 h t g ti i( ) ( ))
, ãäå
h ti ( ) è g ti ( ) îïðåäåëÿþòñÿ 1-ðàçâåðòêîé ôîðìóëû � i t( ).  ðåçóëüòàòå ïîëó÷èì
ñïåöèôèêàöèþ F t f tz2 � � ( ) â ÿçûêå L. Ýòà ñïåöèôèêàöèÿ íå ýêâèâàëåíòíà ñïå-
öèôèêàöèè F1, ïîñêîëüêó ôîðìóëà F2 ÿçûêà L èìååò äîïîëíèòåëüíûå ïî ñðàâíå-
íèþ ñ F1 ìîäåëè, à ñèíòåçèðîâàííûé ïî íåé àâòîìàò ìîæåò èìåòü äîïîëíèòåëü-
íûå ñîñòîÿíèÿ.
ÔÈÊÒÈÂÍÛÅ ÑÎÑÒÎßÍÈß
Äëÿ ôîðìóëû F t( ) ÿçûêà L ñ ñèãíàòóðîé �, ïîñòðîåííîé èç àòîìîâ âèäà
p t p t r( ), , ( )� , îïðåäåëèì åå èñòèííîñòíîå çíà÷åíèå íà îáðàòíîì ñëîâå
� � r � 0 (� i �� �( )), ïîëàãàÿ, ÷òî àòîìû âèäà p t k( ) (k r� 0 1, , ,� ) ïðèíèìà-
þò çíà÷åíèÿ èç âåêòîðà � k . Òàêàÿ ôîðìóëà èñòèííà â ïîçèöèè � (� �
N ) îá-
ðàòíîãî ñâåðõñëîâà g, åñëè îíà èñòèííà íà åãî îòðåçêå g r( , )� � .
Ñ êàæäîé ôîðìóëîé âèäà z t z t h t g ti i i i( ) ( ( )& ( ) ( ))�
1 â ñïåöèôèêàöèè F2
àññîöèèðóåòñÿ óñëîâèå C t g t h t z ti i i i( ) ( ) ( ) ( )� � . Ïóñòü â ñïåöèôèêàöèè F2 èìååò-
ñÿ k òàêèõ ýêâèâàëåíòíîñòåé. Êàê ïîêàçàíî â [6], M F M F( ) ( )1 2� è ìîäåëü èç
M F( )2 íå ïðèíàäëåæèò M F( )1 òîëüêî â òîì ñëó÷àå, åñëè îíà èìååò �-ïðåôèêñ,
âî âñåõ ïîçèöèÿõ êîòîðîãî èñòèííà îäíà è òà æå ôîðìóëà C ti ( ) . Òàêèì îáðàçîì,
P F P F( ) ( )1 2� è äëÿ ëþáîãî 0-ïðåôèêñà èç P F( )1 íå ñóùåñòâóåò óñëîâèÿ C ti ( )
( , , )i k�{ }1 � , èñòèííîãî âî âñåõ åãî ïîçèöèÿõ. Îòñþäà òàêæå ñëåäóåò, ÷òî
S F S F( ) ( )1 2� , ò.å. àâòîìàò, ñïåöèôèöèðóåìûé ôîðìóëîé F2 , èìååò ïîäàâòîìàò,
ñòðîãî ýêâèâàëåíòíûé àâòîìàòó A F( )1 . Âñå ñîñòîÿíèÿ, íå ïðèíàäëåæàùèå ýòîìó
ïîäàâòîìàòó, äîëæíû áûòü óäàëåíû. Íàçîâåì òàêèå ñîñòîÿíèÿ ôèêòèâíûìè.
Ïóñòü àâòîìàòó A2 , ñèíòåçèðîâàííîìó ïî ôîðìóëå F2 , ñîîòâåòñòâóåò ðàçáè-
åíèå { � � �P P Pn1 2, , ,� } ìíîæåñòâà P F( )2 íà êëàññû ýêâèâàëåíòíûõ 0-ïðåôèêñîâ.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 1 7
Åñëè �Pi ñîäåðæèò 0-ïðåôèêñ èç P F( )1 , òî ñîîòâåòñòâóþùåå ìíîæåñòâî ñâåðõñëîâ Wi
ïðèíàäëåæèò S F( )1 è, ñëåäîâàòåëüíî, ñîñòîÿíèå qi àâòîìàòà A2 ýêâèâàëåíòíî îä-
íîìó èç ñîñòîÿíèé àâòîìàòà A F( )1 , ñïåöèôèöèðóåìîãî ôîðìóëîé F1. Òàêèì îá-
ðàçîì, ñîñòîÿíèå àâòîìàòà A2 , íå ïðèíàäëåæàùåå ïîäàâòîìàòó, ñòðîãî ýêâèâà-
ëåíòíîìó àâòîìàòó A F( )1
, ñîîòâåòñòâóåò êëàññó èç { � � �P P Pn1 2, , ,� }, íå ñîäåðæà-
ùåìó 0-ïðåôèêñîâ èç P F( )1 .
Ïóñòü ôîðìóëà F ñïåöèôèöèðóåò àâòîìàò A.
Óòâåðæäåíèå 2. Êàæäûé 0-ïðåôèêñ èç P F( ) ïðåäñòàâèì ñîñòîÿíèåì àâòîìàòà A.
Äîêàçàòåëüñòâî. Ïóñòü ñîñòîÿíèÿ àâòîìàòà A ñîîòâåòñòâóþò êëàññàì ðàçáè-
åíèÿ { � � �P P Pn1 2, , ,� } ìíîæåñòâà P F( ) . Ðàññìîòðèì 0-ïðåôèêñ ïðîèçâîëüíîé ìî-
äåëè u äëÿ ôîðìóëû F . Äëÿ êàæäîãî k � 0 k-ïðåôèêñ u k( , ) � ïðèíàäëåæèò íåêî-
òîðîìó êëàññó èç { � � �P P Pn1 2, , ,� }. Òàêèì îáðàçîì, 0-ïðåôèêñ ìîäåëè u îïðåäåëÿ-
åò ïîñëåäîâàòåëüíîñòü P P P0 1 2, , � êëàññîâ èç { � � �P P Pn1 2, , ,� }, à çíà÷èò,
è ñîîòâåòñòâóþùåå îáðàòíîå ñâåðõñëîâî ñîñòîÿíèé � q q q 2 1 0 . Ïóñòü äëÿ ïðî-
èçâîëüíîãî k
0 u k u k k( , ) ( , ) � � � � �1 1� . Òîãäà ñîãëàñíî îïðåäåëåíèþ àâòî-
ìàòà, ñïåöèôèöèðóåìîãî ôîðìóëîé F , � �( , )q qk k k� ��1 1. Îòñþäà ñëåäóåò, ÷òî
0-ïðåôèêñ u( , ) � 0 ïðåäñòàâèì ñîñòîÿíèåì q0 .
Òàê êàê F2 — ôîðìóëà ÿçûêà L, òî äëÿ âñÿêîãî ñîñòîÿíèÿ qi àâòîìàòà A2
ìíîæåñòâî ïðåäñòàâèìûõ èì îáðàòíûõ ñâåðõñëîâ ñîâïàäàåò ñ �Pi . Ïðèâåäåííûå
ðàññóæäåíèÿ ïîêàçûâàþò, ÷òî ñîñòîÿíèå àâòîìàòà A2 ôèêòèâíî òîãäà è òîëüêî
òîãäà, êîãäà âñå ïðåäñòàâèìûå èì îáðàòíûå ñâåðõñëîâà íå ïðèíàäëåæàò P F( )1 .
Íåñëîæíî óáåäèòüñÿ â ñïðàâåäëèâîñòè ñëåäóþùèõ óòâåðæäåíèé.
Óòâåðæäåíèå 3. Åñëè 0-ïðåôèêñ g ìîäåëè äëÿ F2 ïðèíàäëåæèò P F( )1 , òî è
ëþáîå îáðàòíîå ñâåðõñëîâî gr, ãäå r — äîïóñòèìîå k-ïðîäîëæåíèå g (k �
�N ) ,
òàêæå ïðèíàäëåæèò P F( )1 .
Óòâåðæäåíèå 4. Åñëè 0-ïðåôèêñ g ìîäåëè äëÿ F2 íå ïðèíàäëåæèò P F( )1 , òî
è âñå åãî �-ïðåôèêñû íå ïðèíàäëåæàò P F( )1 .
Èç ýòèõ óòâåðæäåíèé ñëåäóåò:
1) åñëè ñîñòîÿíèå íå ôèêòèâíî, òî âñå äîñòèæèìûå èç íåãî ñîñòîÿíèÿ òàêæå
íå ôèêòèâíû;
2) åñëè ñîñòîÿíèå ôèêòèâíî, òî è âñå ñîñòîÿíèÿ, èç êîòîðûõ îíî äîñòèæèìî,
òàêæå ôèêòèâíû.
Ýòî ïîçâîëÿåò ïðè àíàëèçå ôèêòèâíîñòè ñîñòîÿíèé îãðàíè÷èòüñÿ òîëüêî ñîñòî-
ÿíèÿìè íà÷àëüíûõ ñèëüíî ñâÿçíûõ ïîäàâòîìàòîâ (ÍÑÑÏ), ò.å. òàêèõ ñèëüíî ñâÿçíûõ
ïîäàâòîìàòîâ, ñîñòîÿíèÿ êîòîðûõ íå äîñòèæèìû èç îñòàëüíûõ ñîñòîÿíèé àâòîìàòà.
Î÷åâèäíî, ÷òî ëèáî âñå ñîñòîÿíèÿ ÍÑÑÏ ôèêòèâíû, ëèáî âñå îíè íå ôèêòèâíû.
Åñëè àâòîìàò èìååò ôèêòèâíûå ñîñòîÿíèÿ, òî èìååòñÿ ÍÑÑÏ, âñå ñîñòîÿíèÿ êîòîðî-
ãî ôèêòèâíû. Âñå ôèêòèâíûå ñîñòîÿíèÿ äîñòèæèìû èç ñîñòîÿíèé òàêèõ ÍÑÑÏ.
Åñëè ñîñòîÿíèÿ ÍÑÑÏ àâòîìàòà A2 ôèêòèâíû, òî èõ óäàëåíèå ñîõðàíÿåò íàëè-
÷èå â ïîëó÷åííîì àâòîìàòå ïîäàâòîìàòà, ñòðîãî ýêâèâàëåíòíîãî àâòîìàòó A F( )1 .
Ðàññìîòðèì ñïîñîá íàõîæäåíèÿ ôèêòèâíûõ ñîñòîÿíèé â àâòîìàòå A2 .
Óòâåðæäåíèå 5. Ñîñòîÿíèå q ÍÑÑÏ ôèêòèâíî òîãäà è òîëüêî òîãäà, êîãäà
âñå ïðåäñòàâèìûå èì îáðàòíûå ñâåðõñëîâà óäîâëåòâîðÿþò îäíîé è òîé æå ôîð-
ìóëå � � �t t t C ti1 1 1(( ) ( )), ò.å. âî âñåõ ïîçèöèÿõ ýòèõ îáðàòíûõ ñâåðõñëîâ èñ-
òèííà ôîðìóëà C ti ( ) .
Äîñòàòî÷íîñòü íåïîñðåäñòâåííî ñëåäóåò èç îïðåäåëåíèÿ ôèêòèâíîñòè ñîñòî-
ÿíèÿ. Äëÿ äîêàçàòåëüñòâà íåîáõîäèìîñòè ïîêàæåì, ÷òî, åñëè âñå îáðàòíûå ñâåðõ-
8 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 1
ñëîâà, ïðåäñòàâèìûå ñîñòîÿíèåì q, íå ïðèíàäëåæàò P F( )1 , òî ñóùåñòâóåò ôîðìó-
ëà C ti ( ), i k�1 2, , ,� , èñòèííàÿ âî âñåõ ïîçèöèÿõ âñåõ òàêèõ ñâåðõñëîâ. Äîïóñòèì
ïðîòèâíîå, ò.å. äëÿ êàæäîé ôîðìóëû C ti ( ), i k�1 2, , ,� , P q( ) ñîäåðæèò îáðàòíîå
ñâåðõñëîâî, â íåêîòîðîé ïîçèöèè êîòîðîãî ýòà ôîðìóëà ëîæíà. Ïîñêîëüêó q ïðè-
íàäëåæèò ñèëüíî ñâÿçíîìó ïîäàâòîìàòó, òî ñóùåñòâóþò òàêèå ñëîâà ri
(i k�1, ,� ), ïåðåâîäÿùèå ñîñòîÿíèå q â ñåáÿ, ÷òî â íåêîòîðîé ïîçèöèè ñëîâà ri
ëîæíà ôîðìóëà C ti ( ) . Îáðàòíîå ñâåðõñëîâî ( )r rk1 �
� , ïðèíàäëåæàùåå P q( ) ,
íå èìååò �-ïðåôèêñà, â êàæäîé ïîçèöèè êîòîðîãî èñòèííà îäíà èç ôîðìóë C ti ( ) ,
è, ñëåäîâàòåëüíî, îíî ïðèíàäëåæèò P F( )1 . Òàêèì îáðàçîì, ñîñòîÿíèå q íå
ôèêòèâíî. Ïîëó÷åííîå ïðîòèâîðå÷èå äîêàçûâàåò íåîáõîäèìîñòü.
Çàìåòèì, ÷òî êàæäîå îáðàòíîå ñâåðõñëîâî, ïðåäñòàâèìîå ñîñòîÿíèåì ÍÑÑÏ,
ÿâëÿåòñÿ �-ïðåôèêñîì îáðàòíîãî ñâåðõñëîâà, ïðåäñòàâèìîãî ëþáûì äðóãèì ñî-
ñòîÿíèåì ýòîãî ÍÑÑÏ. Ïîýòîìó, åñëè âî âñåõ ïîçèöèÿõ âñåõ ñâåðõñëîâ, ïðåäñòà-
âèìûõ ñîñòîÿíèåì ÍÑÑÏ, èñòèííà ôîðìóëà C ti ( ), òî ýòî ñïðàâåäëèâî è äëÿ âñåõ
îñòàëüíûõ åãî ñîñòîÿíèé.
Áóäåì ãîâîðèòü, ÷òî ÍÑÑÏ ôèêòèâåí, åñëè âî âñåõ ïîçèöèÿõ âñåõ îáðàòíûõ
ñâåðõñëîâ, ïðåäñòàâèìûõ åãî ñîñòîÿíèÿìè, èñòèííà îäíà èç ôîðìóë C ti ( )
( , , )i k�1 � . ×òîáû âûÿñíèòü, ôèêòèâåí ÍÑÑÏ èëè íåò, äàííîå óñëîâèå íåîáõî-
äèìî ïðîâåðÿòü äëÿ êàæäîãî C ti ( ) (i k�1, ,� ). Äëÿ íàèáîëåå îáùåãî âèäà ôîðìó-
ëû C ti ( ) ïðîâåðêà îñóùåñòâëÿåòñÿ ñëåäóþùèì îáðàçîì. Ïóñòü ôîðìóëà C ti ( )
èìååò ãëóáèíó r.  òàêîì ñëó÷àå äëÿ êàæäîãî ñîñòîÿíèÿ ÍÑÑÏ ñòðîèòñÿ ìíîæåñ-
òâî âñåõ ïðåäñòàâèìûõ èì îáðàòíûõ ñëîâ äëèíû r �1 . Íåòðóäíî âèäåòü, ÷òî
C ti ( ) èñòèííà âî âñåõ ïîçèöèÿõ âñåõ îáðàòíûõ ñâåðõñëîâ, ïðåäñòàâèìûõ ñîñòîÿ-
íèÿìè ÍÑÑÏ, òîãäà è òîëüêî òîãäà, êîãäà îíà èñòèííà íà âñåõ îáðàòíûõ ñëîâàõ,
ïðåäñòàâèìûõ ýòèìè ñîñòîÿíèÿìè.
 íåêîòîðûõ äîâîëüíî ÷àñòî âñòðå÷àþùèõñÿ ñëó÷àÿõ ïðîâåðêà ìîæåò áûòü
óïðîùåíà.
Åñëè ôîðìóëà C ti ( ) (i k�1, ,� ) ñîäåðæèò àòîìû òîëüêî ðàíãà 0, òî îíà èñ-
òèííà âî âñåõ ïîçèöèÿõ îáðàòíûõ ñâåðõñëîâ, ïðåäñòàâèìûõ âñåìè ñîñòîÿíèÿìè
ÍÑÑÏ, òîëüêî â òîì ñëó÷àå, åñëè îòìåòêè âñåõ ïåðåõîäîâ ýòîãî ÍÑÑÏ, ðàññìàò-
ðèâàåìûå êàê ôîðìóëû ÿçûêà L, èìïëèöèðóþò C ti ( ) .
Åñëè C ti ( ) èìååò âèä c t s c ti is
( )& & ( ) �
0
, ãäå ôîðìóëà c t ji j
( ) ïîñòðîåíà
èç àòîìîâ ðàíãà j, òî îíà ïðåîáðàçóåòñÿ â ôîðìóëó � �C t c t c ti i is
( ) ( )& & ( )�
0
ãëó-
áèíû 0. Òàêàÿ ôîðìóëà C ti ( ) èñòèííà âî âñåõ ïîçèöèÿõ îáðàòíûõ ñâåðõñëîâ, ïðåä-
ñòàâèìûõ âñåìè ñîñòîÿíèÿìè ÍÑÑÏ, òîëüêî â òîì ñëó÷àå, åñëè �C ti ( ) èñòèííà âî
âñåõ ïîçèöèÿõ ýòèõ ñâåðõñëîâ, ÷òî ñâîäèò ïðîâåðêó ê ïðåäûäóùåìó ñëó÷àþ.
Åñëè ÍÑÑÏ ñîñòîèò èç îäíîãî ñîñòîÿíèÿ q (ïåòëÿ â ñîñòîÿíèè q ñ îòìåòêîé �),
à ôîðìóëà C ti ( ) èìååò âèä c t c tk1 ( ) ( )
� , ãäå êàæäàÿ ôîðìóëà c ti ( ) ïðåäñòàâ-
ëÿåò ñîáîé êîíúþíêöèþ ðàññìîòðåííîãî âûøå âèäà, òî C ti ( ) ïðåîáðàçóåòñÿ
â ôîðìóëó � � �
�C t c t c ti k( ) ( ) ( )1 � ãëóáèíû 0. Ôîðìóëà C ti ( ) èñòèííà âî âñåõ
ïîçèöèÿõ îáðàòíûõ ñâåðõñëîâ, ïðåäñòàâèìûõ ñîñòîÿíèåì q, åñëè îòìåòêà � èì-
ïëèöèðóåò �C ti ( ) .
Âî âñåõ ðàññìîòðåííûõ ÷àñòíûõ ñëó÷àÿõ ïðîâåðÿåòñÿ èñòèííîñòü ôîðìóëû
ãëóáèíû 0, ïîýòîìó ïðîâåðêà îñóùåñòâëÿåòñÿ íà ñëîâàõ äëèíû 1, ïðåäñòàâèìûõ
âñåìè ñîñòîÿíèÿìè ÍÑÑÏ, ò.å. íà îòìåòêàõ âñåõ ïåðåõîäîâ â ÍÑÑÏ.
Ôîðìóëó F t( ) ÿçûêà L, èìåþùóþ ãëóáèíó r, è ñèãíàòóðó � � { }p pm1, ,� ìîæ-
íî ðàññìàòðèâàòü êàê ïðîïîçèöèîíàëüíóþ ôîðìóëó ñ ïåðåìåííûìè p t p tm1 ( ), , ( ),�
p t p t p t r p t rm m1 11 1( ), , ( ), , ( ), , ( ) � � � . Òàêèì îáðàçîì, ïðîâåðêà ôèê-
òèâíîñòè ñîñòîÿíèé ÍÑÑÏ ñîñòîèò â ïðîâåðêå èñòèííîñòè êàæäîé èç ïðîïîçèöè-
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 1 9
îíàëüíûõ ôîðìóë, ñîîòâåòñòâóþùèõ ôîðìóëàì C ti ( ) ( , ,i k�1 � ) íà íàáîðàõ çíà-
÷åíèé èõ àðãóìåíòîâ, îïðåäåëÿåìûõ îòìåòêàìè ïåðåõîäîâ â ÍÑÑÏ.
Ôèêòèâíûå ñîñòîÿíèÿ óäàëÿþòñÿ èç àâòîìàòà. Ïðè óäàëåíèè ñîñòîÿíèé êàêî-
ãî-ëèáî èç ÍÑÑÏ è âñåõ ñîñòîÿíèé, íå ïðèíàäëåæàùèõ öèêëè÷åñêîìó ïîäàâòîìàòó
àâòîìàòà, ïîëó÷åííîãî ïîñëå óäàëåíèÿ ÍÑÑÏ, ìîãóò ïîÿâèòüñÿ íîâûå ÍÑÑÏ, äëÿ
êîòîðûõ âûïîëíÿåòñÿ àíàëîãè÷íàÿ ïðîâåðêà.  ðåçóëüòàòå óäàëåíèÿ âñåõ ôèêòèâíûõ
ñîñòîÿíèé ïîëó÷àåòñÿ àâòîìàò, ñïåöèôèöèðóåìûé ôîðìóëîé F1. Åñëè áóäóò óäàëå-
íû âñå ñîñòîÿíèÿ àâòîìàòà A2 , òî èñõîäíàÿ ñïåöèôèêàöèÿ F ïðîòèâîðå÷èâà.
ÇÀÊËÞ×ÅÍÈÅ
Ðàññìîòðåííûé â íàñòîÿùåé ðàáîòå ïîäõîä ê ñèíòåçó àâòîìàòà, ñïåöèôèöèðî-
âàííîãî â ÿçûêå L*, ñîñòîèò â ñëåäóþùåì.
Ñïåöèôèêàöèÿ F â ÿçûêå L* ïðåîáðàçóåòñÿ â ñïåöèôèêàöèþ F1 â ýòîì æå
ÿçûêå, êîòîðàÿ ýêâèâàëåíòíà èñõîäíîé ñïåöèôèêàöèè îòíîñèòåëüíî åå ñèãíàòó-
ðû � è ñïåöèôèöèðóåò àâòîìàò A1 ñ êîíå÷íîé ïàìÿòüþ. Ïðîåêöèÿ àâòîìàòà A1 íà
ñèãíàòóðó � [8] ñîâïàäàåò ñ àâòîìàòîì A, ñïåöèôèöèðóåìûì ôîðìóëîé F ,
êîòîðûé, âîîáùå ãîâîðÿ, íå îáëàäàåò êîíå÷íîé ïàìÿòüþ. Ïðè ðåàëèçàöèè àâ-
òîìàòà A1 åãî ïðîåêöèÿ íà � ïîëó÷àåòñÿ òðèâèàëüíî, ïîýòîìó îí ñèíòåçèðóåòñÿ
âìåñòî àâòîìàòà A. Ïîñêîëüêó àâòîìàò A1 îáëàäàåò êîíå÷íîé ïàìÿòüþ, îí ìîæåò
áûòü ñïåöèôèöèðîâàí â ÿçûêå L. Òàêèì îáðàçîì, çàäà÷ó ïîñòðîåíèÿ àâòîìàòà A1
ìîæíî ðåøàòü, èñïîëüçóÿ îäèí èç äâóõ ïîäõîäîâ.
1. Ïî ñïåöèôèêàöèè F1 ñòðîèòñÿ ñïåöèôèêàöèÿ â ÿçûêå L, ñïåöèôèöèðóþùàÿ
àâòîìàò A1, êîòîðûé çàòåì ñèíòåçèðóåòñÿ ïðîöåäóðîé ñèíòåçà. Çàìåòèì, ÷òî ñïå-
öèôèêàöèÿ àâòîìàòà A1 â ÿçûêå L ëîãè÷åñêè íå ýêâèâàëåíòíà ñïåöèôèêàöèè F1
â ÿçûêå L*, õîòÿ îíè ñïåöèôèöèðóþò îäèí è òîò æå àâòîìàò.
2. Ïî ñïåöèôèêàöèè F ñòðîèòñÿ ñïåöèôèêàöèÿ â ÿçûêå L, ñïåöèôèöèðóþùàÿ
àâòîìàò A2 , ñîäåðæàùèé A1 â êà÷åñòâå ïîäàâòîìàòà. Çàòåì íà óðîâíå ïðîöå-
äóðíîãî ïðåäñòàâëåíèÿ àâòîìàòîâ èç ñèíòåçèðîâàííîãî àâòîìàòà âûäåëÿåòñÿ àâòî-
ìàò A1 ïóòåì óäàëåíèÿ âñåõ íå ïðèíàäëåæàùèõ åìó ñîñòîÿíèé.
Ïåðâûé ïîäõîä ðàññìîòðåí â [6]; â íàñòîÿùåé ðàáîòå, êàê è â [4, 5], ðàññìîò-
ðåí âòîðîé ïîäõîä. Îäíàêî ïðåäëîæåííûé çäåñü ìåòîä àíàëèçà ôèêòèâíîñòè ñî-
ñòîÿíèé ñóùåñòâåííî ïðîùå ìåòîäà, îïèñàííîãî â [5], ïîñêîëüêó ïðîâåðêà ôèê-
òèâíîñòè ñîñòîÿíèé îñíîâàíà íà ïðîñòûõ îïåðàöèÿõ ïðîïîçèöèîíàëüíîé ëîãèêè.
ÑÏÈÑÎÊ ËÈÒÅÐÀÒÓÐÛ
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. × å á î ò à ð å â À . Í . Ïðåîáðàçîâàíèå ñïåöèôèêàöèè àâòîìàòà â ÿçûêå L* â àâòîìàòíî
ýêâèâàëåíòíóþ ñïåöèôèêàöèþ â ÿçûêå L // Òàì æå. — 2010. — ¹ 4. — Ñ. 60–69.
7. × å á î ò à ð å â À . Í . Î êëàññå ôîðìóë ÿçûêà L*, ñïåöèôèöèðóþùèõ àâòîìàòû ñ êîíå÷íîé ïàìÿòüþ //
Òàì æå. — 2010. — ¹ 1. — Ñ. 3–9.
8. × å á î ò à ð å â À . Í . , Ê ó ð è â ÷ à ê Î . È . Äîïóñòèìûå ïðåîáðàçîâàíèÿ àâòîìàòà, âçàèìîäåéñò-
âóþùåãî ñî ñðåäîé // Óïðàâëÿþùèå ñèñòåìû è ìàøèíû. — 2010. — ¹ 1. — C. 38–44.
Ïîñòóïèëà 16.08.2011
10 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 1
|
| id | nasplib_isofts_kiev_ua-123456789-86159 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 0023-1274 |
| language | Russian |
| last_indexed | 2025-12-07T13:31:32Z |
| publishDate | 2013 |
| publisher | Інститут кібернетики ім. В.М. Глушкова НАН України |
| record_format | dspace |
| spelling | Чеботарев, А.Н. 2015-09-08T17:57:37Z 2015-09-08T17:57:37Z 2013 Анализ фиктивности состояний автомата, синтезированного по спецификации, преобразованной из языка L* в язык L / А.Н. Чеботарев // Кибернетика и системный анализ. — 2013. — Т. 49, № 1. — С. 3-10. — Бібліогр.: 8 назв. — рос. 0023-1274 https://nasplib.isofts.kiev.ua/handle/123456789/86159 519.713.1 Розглянуто метод синтезу скінченного автомата, специфікованого логічною мовою L*. Цей метод базується на трансляції специфікації у менш виразну мову L і застосуванні існуючого методу синтезу автомата за специфікацією у цій мові. Автомат, що синтезується у такий спосіб, може мати зайві (фіктивні) стани, які мають бути вилученими. Запропоновано простий метод перевірки станів на фіктивність. A method for synthesizing an FSM specified in the logical language L* is considered. The method is based on translating the specification into the less expressive language L and applying the available method for synthesizing an FSM from the specification in this language. The resulting FSM may contain extra states called fictitious that have to be deleted. A simple method for checking the states for fictitiousness is proposed. ru Інститут кібернетики ім. В.М. Глушкова НАН України Кибернетика и системный анализ Кибернетика Анализ фиктивности состояний автомата, синтезированного по спецификации, преобразованной из языка L* в язык L Аналіз фіктивності станів автомата, синтезованого за специфікацією, що перетворена із мови L* у мову L Fictitiousness analysis of the states of a finite state machine synthesized from the specification, which is transformed from language L* to language L Article published earlier |
| spellingShingle | Анализ фиктивности состояний автомата, синтезированного по спецификации, преобразованной из языка L* в язык L Чеботарев, А.Н. Кибернетика |
| title | Анализ фиктивности состояний автомата, синтезированного по спецификации, преобразованной из языка L* в язык L |
| title_alt | Аналіз фіктивності станів автомата, синтезованого за специфікацією, що перетворена із мови L* у мову L Fictitiousness analysis of the states of a finite state machine synthesized from the specification, which is transformed from language L* to language L |
| title_full | Анализ фиктивности состояний автомата, синтезированного по спецификации, преобразованной из языка L* в язык L |
| title_fullStr | Анализ фиктивности состояний автомата, синтезированного по спецификации, преобразованной из языка L* в язык L |
| title_full_unstemmed | Анализ фиктивности состояний автомата, синтезированного по спецификации, преобразованной из языка L* в язык L |
| title_short | Анализ фиктивности состояний автомата, синтезированного по спецификации, преобразованной из языка L* в язык L |
| title_sort | анализ фиктивности состояний автомата, синтезированного по спецификации, преобразованной из языка l* в язык l |
| topic | Кибернетика |
| topic_facet | Кибернетика |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/86159 |
| work_keys_str_mv | AT čebotarevan analizfiktivnostisostoâniiavtomatasintezirovannogopospecifikaciipreobrazovannoiizâzykalvâzykl AT čebotarevan analízfíktivnostístanívavtomatasintezovanogozaspecifíkacíêûŝoperetvorenaízmovilumovul AT čebotarevan fictitiousnessanalysisofthestatesofafinitestatemachinesynthesizedfromthespecificationwhichistransformedfromlanguageltolanguagel |