Композиционный подход к проектированию реактивных алгоритмов
Запропоновано метод проектування складних автоматів за їх композиційною специфікацією мовою L. Композиційна специфікація складається із специфікацій автоматних модулів та зв’язків між ними. Автомат, що синтезується, одержується шляхом з’єднання графів переходів модулів, синтезованих за їх специфікац...
Saved in:
| Published in: | Кибернетика и системный анализ |
|---|---|
| Date: | 2013 |
| Main Author: | |
| Format: | Article |
| Language: | Russian |
| Published: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2013
|
| Subjects: | |
| Online Access: | https://nasplib.isofts.kiev.ua/handle/123456789/86267 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Cite this: | Композиционный подход к проектированию реактивных алгоритмов / А.Н. Чеботарев // Кибернетика и системный анализ. — 2013. — Т. 49, № 5. — С. 14-27. — Бібліогр.: 15 назв. — рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1859788426668146688 |
|---|---|
| author | Чеботарев, А.Н. |
| author_facet | Чеботарев, А.Н. |
| citation_txt | Композиционный подход к проектированию реактивных алгоритмов / А.Н. Чеботарев // Кибернетика и системный анализ. — 2013. — Т. 49, № 5. — С. 14-27. — Бібліогр.: 15 назв. — рос. |
| collection | DSpace DC |
| container_title | Кибернетика и системный анализ |
| description | Запропоновано метод проектування складних автоматів за їх композиційною специфікацією мовою L. Композиційна специфікація складається із специфікацій автоматних модулів та зв’язків між ними. Автомат, що синтезується, одержується шляхом з’єднання графів переходів модулів, синтезованих за їх специфікаціями.
A method for the development of complex finite state machines (FSMs) from their compositional specifications in the logical language L is proposed. A compositional specification consists of specifications of automata modules and interconnections between them. The FSM being synthesized is obtained by connecting the state transition graphs of modules synthesized from their specifications.
|
| first_indexed | 2025-12-02T11:24:41Z |
| format | Article |
| fulltext |
ÓÄÊ 519.713.1
À.Í. ×ÅÁÎÒÀÐÅÂ
ÊÎÌÏÎÇÈÖÈÎÍÍÛÉ ÏÎÄÕÎÄ Ê ÏÐÎÅÊÒÈÐÎÂÀÍÈÞ
ÐÅÀÊÒÈÂÍÛÕ ÀËÃÎÐÈÒÌÎÂ
Êëþ÷åâûå ñëîâà: ìîäóëü àëãîðèòìà, êîìïîçèöèîííàÿ ñïåöèôèêàöèÿ, ÿçûê L,
�-àâòîìàò, ñâåðõñëîâî, îïåðàöèè ñîåäèíåíèÿ ìîäóëåé, âûäåëåíèå ñîñòîÿíèÿ.
ÂÂÅÄÅÍÈÅ
Ðàññìàòðèâàåìûé ïðîöåññ ïðîåêòèðîâàíèÿ ðåàêòèâíîãî àëãîðèòìà ñîñòîèò
â ïîñòðîåíèè ôîðìàëüíîé ñïåöèôèêàöèè òðåáîâàíèé ê åãî ïîâåäåíèþ è àâòî-
ìàòè÷åñêîì ïåðåõîäå îò òàêîé (êàê ïðàâèëî, äåêëàðàòèâíîé) ñïåöèôèêàöèè
ê èìïåðàòèâíîìó (ïðîöåäóðíîìó) ïðåäñòàâëåíèþ àëãîðèòìà. Ñïåöèôèêàöèÿ
òðåáîâàíèé ê ôóíêöèîíèðîâàíèþ àëãîðèòìà ïðåäñòàâëÿåò ñîáîé ìíîæåñòâî
óòâåðæäåíèé, çàïèñàííûõ íà ôîðìàëüíîì ÿçûêå, êîòîðûå äîëæíû áûòü ñïðà-
âåäëèâû â êàæäûé ìîìåíò ðàáîòû àëãîðèòìà. Â èñïîëüçóåìîì ïîäõîäå ê ïðî-
åêòèðîâàíèþ òàêàÿ ñïåöèôèêàöèÿ ñîñòîèò èç äâóõ ÷àñòåé: ñïåöèôèêàöèè
óïðàâëÿþùåé ÷àñòè àëãîðèòìà è ñïåöèôèêàöèè îïåðàöèîííîé ÷àñòè. Îïåðàöè-
îííàÿ ÷àñòü àëãîðèòìà ðåàëèçóåòñÿ â âèäå äîñòàòî÷íî ðåãóëÿðíîé ñòðóêòóðû
(ïðîãðàììíîé èëè àïïàðàòóðíîé), ïîýòîìó çàäà÷è ñïåöèôèêàöèè è ðåàëèçàöèè
ýòîé ÷àñòè ñóùåñòâåííî ïðîùå àíàëîãè÷íûõ çàäà÷ äëÿ óïðàâëÿþùåé ÷àñòè,
êîòîðûì è ïîñâÿùåíà íàñòîÿùàÿ ðàáîòà. Ïîñêîëüêó ïðîåêòèðîâàíèå óïðàâëÿ-
þùåé ÷àñòè àëãîðèòìà îñóùåñòâëÿåòñÿ ñ ó÷åòîì îãðàíè÷åíèé, îïðåäåëÿåìûõ
åãî îïåðàöèîííîé ÷àñòüþ è ñðåäîé, äëÿ îïòèìèçàöèè óïðàâëÿþùåé ÷àñòè ýòè
îãðàíè÷åíèÿ íåîáõîäèìî òàêæå ñïåöèôèöèðîâàòü.
Àëãîðèòìû ôóíêöèîíèðîâàíèÿ íåáîëüøèõ ñèñòåì, èìåþùèõ äîñòàòî÷íî
ïðîñòîå óïðàâëåíèå, ìîãóò áûòü ñïåöèôèöèðîâàíû îäíèì íàáîðîì òðåáîâàíèé,
ò.å. íàáîðîì èíâàðèàíòîâ, êîòîðûå äîëæíû áûòü èñòèííûìè â ëþáîé ìîìåíò ðà-
áîòû ñèñòåìû. Îäíàêî ïîâåäåíèå ñëîæíûõ ñèñòåì, â îñîáåííîñòè òàêèõ, ôóíêöè-
îíèðîâàíèå êîòîðûõ ñî âðåìåíåì ìîæåò ñóùåñòâåííî èçìåíÿòüñÿ, ñïåöèôèöèðî-
âàòü îäíèì íàáîðîì òðåáîâàíèé íåñðàâíèìî ñëîæíåå. Ñ ðîñòîì ñëîæíîñòè ñïå-
öèôèöèðóåìîãî àëãîðèòìà óâåëè÷èâàåòñÿ êîëè÷åñòâî èíâàðèàíòîâ è ñëîæíîñòü
ôîðìóë, èõ âûðàæàþùèõ, ÷òî ïðèâîäèò ê íåëèíåéíîìó ðîñòó ñëîæíîñòè ñïåöè-
ôèêàöèè â çàâèñèìîñòè îò ñëîæíîñòè àëãîðèòìà. Î÷åâèäíî, ÷òî âåðîÿòíîñòü ïî-
ÿâëåíèÿ îøèáêè â òàêîé ñïåöèôèêàöèè òàêæå çíà÷èòåëüíî âîçðàñòàåò, êðîìå
òîãî, ìîæåò íåäîïóñòèìî óâåëè÷èòüñÿ âðåìÿ ñèíòåçà àëãîðèòìà, ýêñïîíåíöèàëü-
íî çàâèñÿùåå îò ðàçìåðà ñïåöèôèêàöèè. Ïîýòîìó ñïåöèôèêàöèþ öåëåñîîáðàçíî
ðàçáèòü íà íåñêîëüêî ôðàãìåíòîâ, ñïåöèôèöèðóþùèõ îòäåëüíûå ÷àñòè àëãîðèò-
ìà ôóíêöèîíèðîâàíèÿ ñèñòåìû, íàçûâàåìûå ìîäóëÿìè è ñîåäèíÿåìûå â îäèí àë-
ãîðèòì íà óðîâíå ãðàôîâ ïåðåõîäîâ àâòîìàòîâ, ïîëó÷åííûõ ïóòåì ñèíòåçà
óïðàâëÿþùèõ ÷àñòåé ìîäóëåé. Ïîñòðîåííóþ òàêèì îáðàçîì ñïåöèôèêàöèþ
íàçîâåì êîìïîçèöèîííîé. Êîìïîçèöèîííàÿ ñïåöèôèêàöèÿ ñîñòîèò èç
ñïåöèôèêàöèè ìîäóëåé è ñïåöèôèêàöèè ñâÿçåé ìåæäó íèìè.
Êîìïîçèöèîííûå ìåòîäû ÿâëÿþòñÿ îäíèì èç ñïîñîáîâ áîðüáû ñî ñëîæíîñ-
òüþ ðåøåíèÿ çàäà÷ ïðîåêòèðîâàíèÿ. Ýòî îòíîñèòñÿ êàê ê çàäà÷àì âåðèôèêàöèè,
òàê è ê çàäà÷àì ñèíòåçà, ÷åìó ïîñâÿùåíî ìíîãî ïóáëèêàöèé.  çàäà÷àõ ñèíòåçà
äëÿ ïîâåäåí÷åñêîãî îïèñàíèÿ ðåàêòèâíûõ àëãîðèòìîâ íà íà÷àëüíûõ ýòàïàõ ïðî-
14 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 5
© À.Í. ×åáîòàðåâ, 2013
åêòèðîâàíèÿ íàèáîëüøåå ðàñïðîñòðàíåíèå ïîëó÷èëè àâòîìàòíûå ìîäåëè, òàêèå
êàê äèàãðàììû ñîñòîÿíèé (Statecharts) [1–3], êîìïîçèöèè ðåàêòèâíûõ ìîäó-
ëåé [4, 5] èëè ðàñøèðåííûõ àâòîìàòîâ (EFSM, CEFSM è äð.) [6, 7]. Êàæäàÿ òàêàÿ
ìîäåëü ïðåäñòàâëÿåò ñîáîé ðàçâèòèå òðàäèöèîííîé ìîäåëè êîíå÷íîãî àâòîìàòà
(Finite State Machine), äîïóñêàþùåå åå ñòðóêòóðíîå èåðàðõè÷åñêîå îïèñàíèå.
Ðàñøèðåíèå ïîíÿòèÿ àâòîìàòà â òàêèõ ìîäåëÿõ, êàê ðåàêòèâíûé ìîäóëü, EFSM è
äðóãèå, ñâÿçàíî ñ ââåäåíèåì â ìîäåëü òèïèçèðîâàííûõ ïåðåìåííûõ, îïðåäåëÿþ-
ùèõ ñîñòîÿíèÿ ìîäåëè, îïèñàíèé äåéñòâèé, èçìåíÿþùèõ çíà÷åíèÿ ïåðåìåííûõ,
è ïðåäèêàòîâ, îïðåäåëåííûõ íà ñîñòîÿíèÿõ ìîäåëè. Â íàñòîÿùåé ðàáîòå ýòîìó
ñîîòâåòñòâóåò ïðåäñòàâëåíèå ìîäóëÿ è âñåãî àëãîðèòìà â âèäå êîìïîçèöèè
óïðàâëÿþùåãî è îïåðàöèîííîãî àâòîìàòîâ. Òàêîå ðàçäåëåíèå íà äâà êîìïîíåíòà
è èñïîëüçîâàíèå êîíå÷íî-àâòîìàòíîé ìîäåëè äëÿ ïðåäñòàâëåíèÿ èíôîðìàöèè
î ïîâåäåíèè îïåðàöèîííîãî àâòîìàòà ïîçâîëÿåò îïòèìèçèðîâàòü óïðàâëÿþùèé
àâòîìàò â ïðîöåññå åãî ñèíòåçà.
Íåäîñòàòêîì äèàãðàìì ñîñòîÿíèé ÿâëÿåòñÿ íåâîçìîæíîñòü âåðèôèêàöèè
ñâîéñòâ òàêîãî ïîâåäåí÷åñêîãî îïèñàíèÿ, ïîýòîìó â ðàáîòàõ [8–10] ïðåäëàãàåòñÿ
äîïîëíÿòü îïèñàíèå óòâåðæäåíèÿìè êàêîé-ëèáî òåìïîðàëüíîé ëîãèêè. Ïðåäïî÷òå-
íèå çäåñü îòäàåòñÿ ëîãèêàì ñ òåìïîðàëüíûìè îïåðàòîðàìè ïðîøëîãî âðåìåíè.
Îäíàêî îñíîâíîé íåäîñòàòîê ïåðå÷èñëåííûõ ïîäõîäîâ ñîñòîèò â íåîáõîäèìîñòè
íåôîðìàëèçîâàííîé ðàçðàáîòêè ïðîöåäóðíîãî (àâòîìàòíîãî) ïðåäñòàâëåíèÿ ñïå-
öèôèêàöèè àëãîðèòìà íà âåðõíåì óðîâíå åãî ïðîåêòèðîâàíèÿ.
Ïðåäëàãàåìûé â íàñòîÿùåé ðàáîòå ïîäõîä ê ïðîåêòèðîâàíèþ ðåàêòèâíîãî
àëãîðèòìà ñóùåñòâåííî îòëè÷àåòñÿ îò óïîìÿíóòûõ ïîäõîäîâ, à èìåííî: óðîâíåì
èñõîäíîé ñïåöèôèêàöèè, ïðåäñòàâëÿþùåé ñîáîé ëîãè÷åñêóþ ñïåöèôèêàöèþ òðå-
áîâàíèé ê ôóíêöèîíèðîâàíèþ ïðîåêòèðóåìîãî àëãîðèòìà; èñïîëüçîâàíèåì ïðî-
öåäóðû ñèíòåçà [11], äàþùåé ïðîöåäóðíîå îïèñàíèå àëãîðèòìà, ãàðàíòèðîâàííî
óäîâëåòâîðÿþùåå âñåì òðåáîâàíèÿì ñïåöèôèêàöèè; êîìïîçèöèîííûì ïîäõîäîì
êàê ê ïîñòðîåíèþ ëîãè÷åñêîé ñïåöèôèêàöèè òðåáîâàíèé ê ôóíêöèîíèðîâàíèþ
àëãîðèòìà, òàê è ê åãî ñèíòåçó. Â îñíîâå òàêîãî ïðîåêòèðîâàíèÿ ëåæèò ñèíòåç àâ-
òîìàòîâ, ñîîòâåòñòâóþùèõ ìîäóëÿì, è ñîåäèíåíèå èõ ãðàôîâ ïåðåõîäîâ, îïðåäå-
ëÿåìîå ñïåöèôèêàöèåé ñâÿçåé ìåæäó ìîäóëÿìè. Ñîåäèíåíèå àâòîìàòíûõ ìîäå-
ëåé íà óðîâíå èõ ãðàôîâ ïåðåõîäîâ ðàññìàòðèâàëîñü è â [12], ãäå ñîñòîÿíèÿ
îòîæäåñòâëÿþòñÿ â íåêîòîðûõ ïðîñòûõ ñòðóêòóðàõ ãðàôîâ. Â íàñòîÿùåé ðàáîòå
ïðåäëîæåíû ðàçâèòûå îïåðàöèè ñîåäèíåíèÿ ìîäóëåé, îïðåäåëåííûå êàê íà óðîâ-
íå èõ ñïåöèôèêàöèè, òàê è íà óðîâíå ãðàôîâ ïåðåõîäîâ ñîîòâåòñòâóþùèõ àâòî-
ìàòîâ, ÷òî ïîçâîëÿåò ïîëó÷àòü ëþáûå ñòðóêòóðû èç ñîåäèíÿåìûõ êîìïîíåíòîâ.
Òàêîé ïîäõîä óïðîùàåò ïðîöåññ íàïèñàíèÿ ñïåöèôèêàöèè, ÷òî ñíèæàåò âåðîÿò-
íîñòü äîïóùåíèÿ â íåé îøèáîê, à òàêæå ñóùåñòâåííî óìåíüøàåò âðåìÿ ñèíòåçà
ïðîöåäóðíîãî ïðåäñòàâëåíèÿ àëãîðèòìà.
ÑÈÍÒÀÊÑÈÑ È ÑÅÌÀÍÒÈÊÀ ßÇÛÊÀ ÑÏÅÖÈÔÈÊÀÖÈÈ
Äëÿ ñïåöèôèêàöèè ìîäóëåé è ñâÿçåé ìåæäó íèìè èñïîëüçóåòñÿ ëîãè÷åñêèé
ÿçûê L [13]. ßçûê L ÿâëÿåòñÿ ôðàãìåíòîì ëîãèêè ïðåäèêàòîâ ïåðâîãî ïîðÿäêà
ñ îäíîìåñòíûìè ïðåäèêàòàìè è ôèêñèðîâàííîé îáëàñòüþ èíòåðïðåòàöèè, â êà-
÷åñòâå êîòîðîé âûñòóïàåò ìíîæåñòâî Z öåëûõ ÷èñåë. Ñïåöèôèêàöèÿ â ÿçûêå L
èìååò âèä ôîðìóëû �t F t( ) . Ôîðìóëà F t( ) ñòðîèòñÿ ñ ïîìîùüþ ëîãè÷åñêèõ
ñâÿçîê èç àòîìàðíûõ ôîðìóë (àòîìîâ) âèäà p t k( )� , ãäå p — îäíîìåñòíûé
ïðåäèêàòíûé ñèìâîë, t — ïåðåìåííàÿ, ïðèíèìàþùàÿ çíà÷åíèÿ èç ìíîæåñòâà Z ,
ðàññìàòðèâàåìîãî êàê ìíîæåñòâî ìîìåíòîâ äèñêðåòíîãî âðåìåíè, k — öåëîå
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 5 15
÷èñëî, íàçûâàåìîå ðàíãîì àòîìà. Ðàçíîñòü ìåæäó ìàêñèìàëüíûì è ìèíèìàëü-
íûì çíà÷åíèÿìè ðàíãîâ àòîìîâ â ôîðìóëå íàçûâàåòñÿ åå ãëóáèíîé.
Ïðè îïðåäåëåíèè àâòîìàòíîé ñåìàíòèêè ÿçûêîâ ñïåöèôèêàöèè ýòè ÿçûêè è
àâòîìàòû ðàññìàòðèâàþòñÿ êàê ôîðìàëèçìû äëÿ çàäàíèÿ ìíîæåñòâ ñâåðõñëîâ
(áåñêîíå÷íûõ ñëîâ) â àëôàâèòå � �( ) , ãäå � � { , , )p pm1 � — íàáîð ïðåäèêàòíûõ
ñèìâîëîâ ñïåöèôèêàöèè. Ñèìâîëû àëôàâèòà � �( ) ïðåäñòàâëÿþò ñîáîé äâîè÷íûå
âåêòîðû äëèíû m .
Îïðåäåëèì íåîáõîäèìûå ïîíÿòèÿ, ñâÿçàííûå ñî ñâåðõñëîâàìè è àâòoìàòàìè.
Ïóñòü � — êîíå÷íûé àëôàâèò, 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 . Äëÿ n � �N ñëîâî g n g( ) ( )1 0 � íà-
çûâàåòñÿ n-ñóôôèêñîì îáðàòíîãî ñâåðõñëîâà g .
Îïðåäåëåíèå 1. Êîíå÷íûé íåèíèöèàëüíûé X Y -àâòîìàò A — ýòî ÷åòâåðêà
�X Y Q A, , , � , ãäå X Y Q, , — êîíå÷íûå ìíîæåñòâà ñîîòâåòñòâåííî âõîäíûõ ñèì-
âîëîâ, âûõîäíûõ ñèìâîëîâ è ñîñòîÿíèé, à �A
QQ X Y: � � � 2 — ôóíêöèÿ ïåðå-
õîäîâ àâòîìàòà.
X Y -àâòîìàò A íàçûâàåòñÿ êâàçèäåòåðìèíèðîâàííûì, åñëè äëÿ ëþáûõ
q Q x X� �, , y Y� | ( , , )|�A q x y
1 . Êâàçèäåòåðìèíèðîâàííûå X Y -àâòîìàòû
óäîáíî ðàññìàòðèâàòü êàê äåòåðìèíèðîâàííûå ÷àñòè÷íûå àâòîìàòû áåç âûõîäà,
ñ âõîäíûì àëôàâèòîì � � �X Y . Òàêîé àâòîìàò A Q A�
��, , � , ãäå
�A Q Q: � �� — ÷àñòè÷íàÿ ôóíêöèÿ, áóäåì íàçûâàòü �-àâòîìàòîì.
Îïðåäåëåíèå 2. �-àâòîìàò A Q A�
��, , � íàçûâàåòñÿ öèêëè÷åñêèì, åñëè äëÿ
êàæäîãî q Q� ñóùåñòâóþò òàêèå � �1 2, �� è q q Q1 2, � , ÷òî q qA1 1� � �( , ) è
q qA� � �( , )2 2 .
 äàëüíåéøåì ïîä àâòîìàòîì áóäåì ïîíèìàòü öèêëè÷åñêèé �-àâòîìàò
A Q A�
�� �( ), , � , ãäå � — ìíîæåñòâî äâîè÷íûõ ïåðåìåííûõ, êîäèðóþùèõ
ñèìâîëû åãî àëôàâèòà.
Îïðåäåëåíèå 3. Ñâåðõñëîâî l � � �1 2 � â àëôàâèòå � äîïóñòèìî â ñîñòîÿ-
íèè q àâòîìàòà A , åñëè ñóùåñòâóåò òàêîå ñâåðõñëîâî ñîñòîÿíèé q q q0 1 2 � , ãäå
q q0 � , ÷òî äëÿ ëþáîãî i � 0 1 2, , ,� q qi A i i� ��1 1� �( , ) . Ìíîæåñòâî âñåõ ñâåðõ-
ñëîâ, äîïóñòèìûõ â ñîñòîÿíèè q, îáîçíà÷èì W q( ) . Ñâåðõñëîâî l äîïóñòèìî äëÿ
àâòîìàòà A , åñëè îíî äîïóñòèìî õîòÿ áû â îäíîì èç åãî ñîñòîÿíèé. Ìíîæåñòâî
âñåõ ñâåðõñëîâ, äîïóñòèìûõ äëÿ àâòîìàòà A , îáîçíà÷èì W A( ) .
Îïðåäåëåíèå 4. Îáðàòíîå ñâåðõñëîâî � � � 1 0 â àëôàâèòå � ïðåäñòàâèìî
ñîñòîÿíèåì q àâòîìàòà A , åñëè ñóùåñòâóåò òàêîå îáðàòíîå ñâåðõñëîâî ñîñòîÿíèé
� q q q 2 1 0 , ãäå q0 = q , ÷òî äëÿ ëþáîãî i � 1 2, ,� q qi A i i� ��1 1� �( , ) . Ìíî-
æåñòâî âñåõ îáðàòíûõ ñâåðõñëîâ, ïðåäñòàâèìûõ ñîñòîÿíèåì q , îáîçíà÷èì P q( ) .
Àíàëîãè÷íî äëÿ ïðîèçâîëüíîãî k � �N îïðåäåëèì ìíîæåñòâî W qk
i( ) âñåõ
ñëîâ äëèíû k, äîïóñòèìûõ â ñîñòîÿíèè qi , è ìíîæåñòâî P qk
i( ) âñåõ ñëîâ äëèíû k,
ïðåäñòàâèìûõ ñîñòîÿíèåì qi .
16 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 5
Ïóñòü A Q A�
��, , � è q q Q1 2, � , � �� . Òðîéêó
�q q1 2, ,� , òàêóþ, ÷òî
� �A q q( , )1 2� , íàçîâåì ïåðåõîäîì â àâòîìàòå A èç ñîñòîÿíèÿ q1 â ñîñòîÿíèå q2 ,
à ñèìâîë � — îòìåòêîé ýòîãî ïåðåõîäà. Áóäåì ãîâîðèòü, ÷òî âõîäíîå ñëîâî
r n� � �1 � ïåðåâîäèò ñîñòîÿíèå q� â ñîñòîÿíèå ��q , åñëè ñóùåñòâóåò òàêîå ñëîâî
ñîñòîÿíèé q q qn1 2 1� � , ÷òî äëÿ êàæäîãî i n�1, ,� â àâòîìàòå A èìååòñÿ ïåðåõîä
��q qi i i, ,� 1 è q q� � 1, �� � �q qn 1 .
Îïðåäåëåíèå 5. �-àâòîìàò A íàçûâàåòñÿ àâòîìàòîì ñ êîíå÷íîé ïàìÿòüþ, åñëè
ñóùåñòâóåò òàêîå íàòóðàëüíîå k, ÷òî äëÿ ëþáîãî âõîäíîãî ñëîâà äëèíû k âñå ñî-
ñòîÿíèÿ àâòîìàòà A, â êîòîðûõ îíî äîïóñòèìî, ïåðåâîäÿòñÿ ýòèì ñëîâîì â ýêâèâà-
ëåíòíûå ñîñòîÿíèÿ. Ìèíèìàëüíîå òàêîå k íàçûâàåòñÿ ãëóáèíîé ïàìÿòè àâòîìàòà.
Ðàññìîòðèì òåïåðü ôîðìóëó ÿçûêà L êàê ñïîñîá çàäàíèÿ ìíîæåñòâà ñâåðõñëîâ.
Êàæäîé ôîðìóëå F tF t� � ( ) ñòàâèòñÿ â ñîîòâåòñòâèå ìíîæåñòâî ìîäåëåé
äëÿ ýòîé ôîðìóëû, ò.å. ìíîæåñòâî òàêèõ èíòåðïðåòàöèé, íà êîòîðûõ F èñòèííà.
Ïóñòü � � { , , }p pm1 � — ìíîæåñòâî âñåõ ïðåäèêàòíûõ ñèìâîëîâ, âñòðå÷àþùèõ-
ñÿ â ôîðìóëå F (ñèãíàòóðà ôîðìóëû). Èíòåðïðåòàöèÿ ôîðìóëû F — ýòî óïîðÿ-
äî÷åííûé íàáîð îïðåäåëåííûõ íà Z îäíîìåñòíûõ ïðåäèêàòîâ � �1, ,� m , ñîîòâå-
òñòâóþùèõ ïðåäèêàòíûì ñèìâîëàì èç � . Èíòåðïðåòàöèþ I m�
�� �1, ,� ìîæ-
íî ïðåäñòàâèòü â âèäå äâóñòîðîííåãî ñâåðõñëîâà â àëôàâèòå � �( ) , à ìíîæåñòâî
âñåõ ìîäåëåé äëÿ F — â âèäå ìíîæåñòâà M F( ) äâóñòîðîííèõ ñâåðõñëîâ â ýòîì
àëôàâèòå. Ïîýòîìó ìîæíî ãîâîðèòü îá èñòèííîñòíîì çíà÷åíèè çàìêíóòîé ôîð-
ìóëû, ò.å. ôîðìóëû âèäà �tF t( ) èëè F ( )� , ãäå � �Z , íà äâóñòîðîííåì ñâåðõñëî-
âå. Îáîçíà÷èì W F( ) ìíîæåñòâî 0-ñóôôèêñîâ âñåõ ìîäåëåé èç M F( ) , à P F( ) —
ìíîæåñòâî 0-ïðåôèêñîâ ýòèõ ìîäåëåé. Òàêèì îáðàçîì, ñ êàæäîé ôîðìóëîé
F tF t� � ( ) àññîöèèðóåòñÿ ìíîæåñòâî ñâåðõñëîâ W F( ) è ìíîæåñòâî îáðàòíûõ
ñâåðõñëîâ P F( ) .
Ôîðìóëà F t( ) ñ åäèíñòâåííîé ñâîáîäíîé ïåðåìåííîé t íàçûâàåòñÿ 0-îãðàíè-
÷åííîé, åñëè äëÿ ëþáîãî � �Z çíà÷åíèÿ ôîðìóëû F ( )� íà âñåõ äâóñòîðîííèõ
ñâåðõñëîâàõ, ñ îäèíàêîâûìè �-ïðåôèêñàìè, ñîâïàäàþò. Áóäåì òàêèå ôîðìóëû èñ-
ïîëüçîâàòü äëÿ çàäàíèÿ ìíîæåñòâ îáðàòíûõ ñâåðõñëîâ, à èìåííî, 0-îãðàíè÷åííàÿ
ôîðìóëà F t( ) çàäàåò ìíîæåñòâî R F t( ( )) 0-ïðåôèêñîâ âñåõ òàêèõ äâóñòîðîííèõ
ñâåðõñëîâ, íà êîòîðûõ èñòèííà F ( )0 . Îáîçíà÷èì R F tk ( ( )) ìíîæåñòâî k-ñóôôèê-
ñîâ âñåõ îáðàòíûõ ñâåðõñëîâ èç R F t( ( )) .
Àâòîìàòíóþ ñåìàíòèêó ÿçûêà L îïðåäåëÿåò ñëåäóþùàÿ òåîðåìà.
Òåîðåìà 1 [13]. Äëÿ êàæäîé íåïðîòèâîðå÷èâîé ôîðìóëû F tF t� � ( ) ñèãíà-
òóðû � ñóùåñòâóåò â îáùåì ñëó÷àå íåäåòåðìèíèðîâàííûé íåèíèöèàëüíûé öèê-
ëè÷åñêèé �-àâòîìàò A QA A�
�� �( ), , � ñ êîíå÷íîé ïàìÿòüþ, äëÿ êîòîðîãî
W A W F( ) ( )� .
Òàêîé àâòîìàò íàçîâåì àâòîìàòîì, ñïåöèôèöèðóåìûì ôîðìóëîé F .
Ïðåäïîëàãàåòñÿ, ÷òî ñèìâîëû ñèãíàòóðû � ðàçáèòû íà äâà êëàññà: âõîäíûå
è âûõîäíûå, îïðåäåëÿþùèå âõîäíîé è âûõîäíîé àëôàâèòû ñîîòâåòñòâóþùåãî
X Y -àâòîìàòà.
ÊÎÌÏÎÇÈÖÈß ÀÂÒÎÌÀÒÎÂ ÍÀ ÓÐÎÂÍÅ ÈÕ ÃÐÀÔÎÂ ÏÅÐÅÕÎÄÎÂ
 êà÷åñòâå àâòîìàòíîé ìîäåëè ìîäóëÿ ðàññìàòðèâàåòñÿ äåòåðìèíèðîâàííûé
�-àâòîìàò A Q A�
��, , � . Çíà÷åíèÿ ôóíêöèè ïåðåõîäîâ â ñîñòîÿíèè q áóäåì
çàäàâàòü â âèäå ìíîæåñòâà îáîáùåííûõ ïåðåõîäîâ èç ýòîãî ñîñòîÿíèÿ. Êàæ-
äûé òàêîé ïåðåõîä ñîîòâåòñòâóåò ìíîæåñòâó ïåðåõîäîâ ìåæäó îäíèìè è òåìè
æå ñîñòîÿíèÿìè, ïðè êîòîðûõ ãåíåðèðóåòñÿ îäèí è òîò æå âûõîäíîé ñèìâîë
ñîîòâåòñòâóþùåãî X Y -àâòîìàòà. Îòìåòêà òàêîãî ïåðåõîäà ñîñòîèò èç äâóõ
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 5 17
÷àñòåé: âõîäíîãî óñëîâèÿ, ò.å. áóëåâîé ôóíêöèè îò âõîäíûõ ïåðåìåííûõ, çàäà-
þùåé ìíîæåñòâî ñèìâîëîâ âõîäíîãî àëôàâèòà X Y -àâòîìàòà, è ñèìâîëà âû-
õîäíîãî àëôàâèòà (íàáîðà çíà÷åíèé âûõîäíûõ ïåðåìåííûõ). Âõîäíûå óñëîâèÿ
ïåðåõîäîâ çàäàþòñÿ ôîðìóëàìè ÿçûêà L, ïîëó÷àþùèìèñÿ çàìåíîé ïåðåìåííûõ
ñîîòâåòñòâóþùèìè àòîìàìè ðàíãà 0. Òàêèì îáðàçîì, óñëîâèþ âèäà f x xm( , , )1 �
ñîîòâåòñòâóåò ôîðìóëà f x t x tm( ( ), , ( ))1 � . Áóäåì ãîâîðèòü, ÷òî ïåðåõîä óäîâ-
ëåòâîðÿåò óñëîâèþ f t( ) , åñëè ôîðìóëà ÿçûêà L, ñîîòâåòñòâóþùàÿ âõîäíîìó
óñëîâèþ ýòîãî ïåðåõîäà, èìïëèöèðóåò ôîðìóëó f t( ) . Åñëè ñèìâîë âûõîäíîãî
àëôàâèòà çàäàâàòü êîíñòèòóýíòîé åäèíèöû îò âûõîäíûõ àòîìîâ íóëåâîãî
ðàíãà, òî îáå ÷àñòè îòìåòêè ïåðåõîäà ìîãóò áûòü çàäàíû îäíîé ôîðìóëîé
ÿçûêà L. Ïðè ýòîì ïåðåõîä
�q q1 2, ,� â êâàçèäåòåðìèíèðîâàííîì X Y -àâòî-
ìàòå îïèñûâàåòñÿ ôîðìóëîé F t f t( ) & ( ) 1 , òàêîé, ÷òî R F t P q( ( )) ( )� 1 ,
R F t f t P q( ( )& ( )) ( ) �1 2 , à f t( ) çàäàåò îòìåòêó ïåðåõîäà � .
Óòî÷íèì íåêîòîðûå èñïîëüçóåìûå â äàëüíåéøåì ïîíÿòèÿ.
Ïðåäûñòîðèÿ — ýòî õàðàêòåðèñòèêà òåêóùåãî ìîìåíòà ðàáîòû ñèñòåìû,
ïðåäñòàâëÿþùàÿ ñîáîé ïîñëåäîâàòåëüíîñòü âõîä-âûõîäíûõ ñèìâîëîâ, ïîëó÷åí-
íûõ ñèñòåìîé îò íà÷àëà åå ôóíêöèîíèðîâàíèÿ (äëÿ íåèíèöèàëüíûõ ñèñòåì â áåñ-
êîíå÷íîì ïðîøëîì) äî ðàññìàòðèâàåìîãî ìîìåíòà. Äëÿ ñïåöèôèêàöèè F ìíî-
æåñòâî âñåõ âîçìîæíûõ ïðåäûñòîðèé ôóíêöèîíèðîâàíèÿ ñïåöèôèöèðóåìîé åþ
ñèñòåìû îïðåäåëÿåòñÿ ìíîæåñòâîì îáðàòíûõ ñâåðõñëîâ P F( ) . Åñëè ìàêñèìàëü-
íàÿ ãëóáèíà ôîðìóë ñïåöèôèêàöèè F â ÿçûêå L ðàâíà k1 , òî â êà÷åñòâå ïðåäûñ-
òîðèé, îäíîçíà÷íî õàðàêòåðèçóþùèõ òåêóùåå ñîñòîÿíèå ñèñòåìû, ìîæíî ðàñ-
ñìàòðèâàòü ñëîâà äëèíû k k� 1 , ÿâëÿþùèåñÿ k-ñóôôèêñàìè îáðàòíûõ ñâåðõñëîâ
èç P F( ) . Ìíîæåñòâî âñåõ òàêèõ ñëîâ îáîçíà÷èì P Fk ( ) .
Ñïîñîá (ðåæèì) ôóíêöèîíèðîâàíèÿ ñèñòåìû — ýòî ôóíêöèÿ, êîòîðàÿ êàæ-
äîé äîïóñòèìîé ïðåäûñòîðèè ñòàâèò â ñîîòâåòñòâèå ìíîæåñòâî äîïóñòèìûõ åå
ïðîäîëæåíèé [14]. Ïðè êîìïîçèöèîííîé ñïåöèôèêàöèè ñèñòåìû âîçìîæíûå ðå-
æèìû åå ðàáîòû îïðåäåëÿþòñÿ ñïåöèôèêàöèÿìè èñïîëüçóåìûõ ìîäóëåé. Â ñèí-
òåçèðîâàííîé ïî òàêîé ñïåöèôèêàöèè ñèñòåìå ìíîæåñòâî ðàçëè÷íûõ ðåæèìîâ åå
ðàáîòû îïðåäåëÿåòñÿ ðàçáèåíèåì ìíîæåñòâà ñîñòîÿíèé ñèñòåìû íà êëàññû, ñîîò-
âåòñòâóþùèå ìíîæåñòâàì ñîñòîÿíèé ñîåäèíÿåìûõ ìîäóëåé. Ïåðåõîä îò îäíîãî
ðåæèìà ôóíêöèîíèðîâàíèÿ ê äðóãîìó ñâÿçàí ñ ñîáûòèåì, ïðåäñòàâëÿþùèì ñî-
áîé èçìåíåíèå çíà÷åíèÿ íåêîòîðîãî óñëîâèÿ ñ ëîæíîãî íà èñòèííîå. Íà óðîâíå
ãðàôîâ àâòîìàòîâ, ñîîòâåòñòâóþùèõ ìîäóëÿì, òàêîé ïåðåõîä îïèñûâàåòñÿ
ñîåäèíåíèåì ãðàôîâ, çàäàâàåìûì ñ ïîìîùüþ äâóõ îñíîâíûõ îïåðàöèé:
— ìåæìîäóëüíûé ïåðåõîä (ÌÌÏ);
— îòîæäåñòâëåíèå ñîñòîÿíèé (ÎÒÑ).
Ñïåöèôèêàöèÿ êàæäîãî ìîäóëÿ ñîñòîèò èç ñïåöèôèêàöèè óïðàâëÿþùåãî àâ-
òîìàòà è ñïåöèôèêàöèè ëîêàëüíîé ñðåäû, õàðàêòåðèçóþùåé âçàèìîäåéñòâèå
óïðàâëÿþùåãî àâòîìàòà ñïåöèôèöèðóåìîãî ìîäóëÿ ñ îïåðàöèîííûì àâòîìàòîì
è âíåøíåé ñðåäîé.
Ñïåöèôèêàöèÿ ñîåäèíåíèé ìåæäó ìîäóëÿìè îñóùåñòâëÿåòñÿ â òåðìèíàõ
ñïåöèôèêàöèé èñõîäíûõ ìîäóëåé, ïîýòîìó ðåçóëüòàò ïîñòðîåíèÿ ñïåöèôèöèðî-
âàííîãî àâòîìàòà íå çàâèñèò îò ïîðÿäêà âûïîëíåíèÿ ñîåäèíåíèé ìîäóëåé.
ÑÎÅÄÈÍÅÍÈÅ ÌÎÄÓËÅÉ Ñ ÏÎÌÎÙÜÞ ÌÅÆÌÎÄÓËÜÍÎÃÎ ÏÅÐÅÕÎÄÀ
Ïðè ðåàëèçàöèè ìåæìîäóëüíîãî ïåðåõîäà èç ìîäóëÿ A â íåãî äîáàâëÿþòñÿ ïå-
ðåõîäû, äëÿ êîòîðûõ óêàçûâàþòñÿ ìîäóëü, êóäà îñóùåñòâëÿåòñÿ ïåðåõîä, è ñî-
ñòîÿíèå â ýòîì ìîäóëå. Êàæäûé äîáàâëÿåìûé îáîáùåííûé ïåðåõîä çàäàåòñÿ
18 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 5
äâóìÿ óñëîâèÿìè, îòíîñÿùèìèñÿ ê ðàçëè÷íûì ìîäóëÿì. Îäíî èç íèõ, íàçûâà-
åìîå óñëîâèåì âûõîäà èç ìîäóëÿ, èìååò âèä F t f t( )& ( ) 1 , ãäå F t( ) 1 —
âíóòðåííÿÿ ÷àñòü óñëîâèÿ, òàêàÿ, ÷òî F t( ) âûäåëÿåò îäíî èëè íåñêîëüêî ñîñòî-
ÿíèé â ìîäóëå A , à f t( ) — âíåøíÿÿ ÷àñòü, îïðåäåëÿþùàÿ îòìåòêè äîáàâëÿå-
ìûõ îáîáùåííûõ ïåðåõîäîâ èç ýòèõ ñîñòîÿíèé. Äðóãîå óñëîâèå âèäà F t( ) ,
íàçûâàåìîå óñëîâèåì âõîäà â ìîäóëü, îïðåäåëÿåò ñîñòîÿíèå â ìîäóëå, êóäà
îñóùåñòâëÿåòñÿ ïåðåõîä. Âíóòðåííÿÿ ÷àñòü óñëîâèÿ âûõîäà èç ìîäóëÿ — ýòî
ôîðìóëà, âñå ïðåäèêàòíûå ñèìâîëû êîòîðîé ïðèíàäëåæàò ñèãíàòóðå ñîîòâåò-
ñòâóþùåãî ìîäóëÿ, à ðàíãè åå àòîìîâ íå ïðåâûøàþò – 1. Âíåøíÿÿ ÷àñòü —
ôîðìóëà, ïîñòðîåííàÿ èç àòîìîâ íóëåâîãî ðàíãà, êîòîðàÿ ìîæåò ñîäåðæàòü
ïðåäèêàòíûå ñèìâîëû, íå ïðèíàäëåæàùèå ñèãíàòóðå ìîäóëÿ A . Âñå ïðåäèêàò-
íûå ñèìâîëû â óñëîâèè âõîäà â ìîäóëü ïðèíàäëåæàò ñèãíàòóðå ýòîãî ìîäóëÿ.
Óòî÷íèì ïîíÿòèå âûäåëåíèÿ ñîñòîÿíèÿ óñëîâèåì F t( ) .
Îïðåäåëåíèå 6. Ôîðìóëà F t( ) ñòðîãî âûäåëÿåò âî ìíîæåñòâå Q ñîñòîÿíèå q ,
åñëè P q R F t( ) ( ( ))� è äëÿ ëþáîãî ñîñòîÿíèÿ q Q1 � , íå óäîâëåòâîðÿþùåãî ýòîìó
óñëîâèþ, P q R F t( ) ( ( ))1 � � � .
Åñëè F t( ) 1 — âíóòðåííÿÿ ÷àñòü óñëîâèÿ âûõîäà èç ìîäóëÿ, òî ôîðìóëà
F t( ) âûäåëÿåò ñîñòîÿíèÿ â óêàçàííîì ñìûñëå.
Äëÿ ôîðìóëû F t( ) , çàäàþùåé óñëîâèå âõîäà â ìîäóëü, âûäåëÿåìîå åþ ñî-
ñòîÿíèå q óäîâëåòâîðÿåò óñëîâèþ P q R F t( ) ( ( ))� � � , êîòîðîå íàçîâåì óñëîâè-
åì ñëàáîãî âûäåëåíèÿ ñîñòîÿíèé.
Äàäèì ôîðìàëüíîå îïðåäåëåíèå îïåðàöèè ìåæìîäóëüíîãî ïåðåõîäà.
Ïóñòü �-àâòîìàòû A QA A A�
�� , , � è B QB B B�
�� , , � , ãäå � � �A A� ( ) è
� � �B B� ( ) , ñîåäèíÿþòñÿ ñ ïîìîùüþ ìåæìîäóëüíîãî ïåðåõîäà èç ìîäóëÿ A
â ìîäóëü B, çàäàâàåìîãî óñëîâèåì âûõîäà èç A, ðàâíûì F t f t1 1( )& ( ) , è óñëîâè-
åì âõîäà â B, ðàâíûì F t2 ( ) . Ïóñòü óñëîâèå F t1 ( ) ñòðîãî âûäåëÿåò â ìîäóëå A ñî-
ñòîÿíèå q QA1 � , à óñëîâèå F t2 ( ) ñëàáî âûäåëÿåò â ìîäóëå B ñîñòîÿíèå q QB2 � .
Ðåçóëüòàò îïåðàöèè ÌÌÏ ïðåäñòàâëÿåò ñîáîé àâòîìàò C QC C C�
�� �( ), , � .
Ñèãíàòóðà �C ðàâíà � �A B Z� � , ãäå Z — ìíîæåñòâî âõîäíûõ ïðåäèêàòíûõ
ñèìâîëîâ, ñîäåðæàùèõñÿ â f t( ) è íå ïðèíàäëåæàùèõ � �A B� . Ìíîæåñòâî QC
ðàâíî � � �Q QA B , ãäå � � � � �Q QA B è �QA âçàèìíî îäíîçíà÷íî îòîáðàæàåòñÿ â QA ,
à �QB — â QB . Ñîñòîÿíèå èç QC , ñîîòâåòñòâóþùåå ñîñòîÿíèþ q Q QA B� � ,
îáîçíà÷èì q�. Ôóíêöèÿ ïåðåõîäîâ �C äëÿ âñåõ ñîñòîÿíèé, îòëè÷íûõ îò �q1, ñîâ-
ïàäàåò ñ ôóíêöèåé ïåðåõîäîâ â ñîîòâåòñòâóþùèõ ñîñòîÿíèÿõ àâòîìàòà A èëè B.
 ñîñòîÿíèè �q1 ôóíêöèÿ ïåðåõîäîâ îïðåäåëÿåòñÿ ñëåäóþùèì îáðàçîì. Ê ïåðå-
õîäàì, ñîîòâåòñòâóþùèì ïåðåõîäàì èç ñîñòîÿíèÿ q1, äîáàâëÿþòñÿ ïåðåõîäû èç
�q1 â �q2 ñ îòìåòêàìè, îïðåäåëÿåìûìè ôîðìóëîé f t( ), à âõîäíûå óñëîâèÿ îòìå-
òîê âñåõ ïåðåõîäîâ, ñîîòâåòñòâóþùèõ ïåðåõîäàì èç q1, óìíîæàþòñÿ íà îòðèöà-
íèå äèçúþíêöèè âñåõ âõîäíûõ óñëîâèé îòìåòîê äîáàâëåííûõ ïåðåõîäîâ. Åñëè
óñëîâèå F t1 ( ) âûäåëÿåò íåñêîëüêî ñîñòîÿíèé, òî ôóíêöèÿ ïåðåõîäîâ â ñîîòâåò-
ñòâóþùèõ ñîñòîÿíèÿõ àâòîìàòà C ñîâïàäàåò ñ îïðåäåëåííîé âûøå ôóíêöèåé
ïåðåõîäîâ â ñîñòîÿíèè �q1 .
Äîáàâëÿåìûé ïåðåõîä, âõîäíîå óñëîâèå êîòîðîãî çàâèñèò òîëüêî îò âõîäíûõ
ïåðåìåííûõ ìîäóëÿ A , íàçîâåì âíóòðåííå îáóñëîâëåííûì ïåðåõîäîì, à ïåðå-
õîä, âõîäíîå óñëîâèå êîòîðîãî ñîäåðæèò ïåðåìåííûå, íå ïðèíàäëåæàùèå ñèãíà-
òóðå ìîäóëÿ A, — âíåøíå îáóñëîâëåííûì. Î÷åâèäíî, ÷òî äîáàâëåííûé âíóòðåí-
íå îáóñëîâëåííûé ïåðåõîä èç ñîñòîÿíèÿ �q1 çàìåíÿåò èìåâøèéñÿ ïåðåõîä èç ñî-
ñòîÿíèÿ q1 ñ òàêèì æå âõîäíûì óñëîâèåì. Ïðè äîáàâëåíèè âíåøíå
îáóñëîâëåííîãî ïåðåõîäà âñå ïåðåõîäû, ñîîòâåòñòâóþùèå ïåðåõîäàì èç ñîñòîÿ-
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 5 19
íèÿ q1, ñîõðàíÿþòñÿ, à îðòîãîíàëüíîñòü èõ âõîäíûõ óñëîâèé è âõîäíîãî óñëî-
âèÿ äîáàâëåííîãî ïåðåõîäà îáåñïå÷èâàåòñÿ óìíîæåíèåì ýòèõ óñëîâèé íà îòðèöà-
íèå âõîäíîãî óñëîâèÿ äîáàâëåííîãî ïåðåõîäà.  ñëó÷àå äîáàâëåíèÿ âíóòðåííå
îáóñëîâëåííîãî ïåðåõîäà èç èíèöèàëüíîãî àâòîìàòà A íåêîòîðûå åãî ñîñòîÿíèÿ
ìîãóò ñòàòü íåäîñòèæèìûìè èç íà÷àëüíûõ ñîñòîÿíèé â ðåçóëüòàòå çàìåíû ïåðå-
õîäîâ ìåæäó ñîñòîÿíèÿìè âíóòðè àâòîìàòà ïåðåõîäàìè â äðóãîé ìîäóëü. Ñîîò-
âåòñòâóþùèå èì ñîñòîÿíèÿ â àâòîìàòå C áóäóò óäàëåíû ïîñëå âûïîëíåíèÿ âñåõ
îïåðàöèé ñîåäèíåíèÿ ìîäóëåé êîìïîçèöèîííîé ñïåöèôèêàöèè. Åñëè àâòîìàò A
èíèöèàëüíûé, òî íà÷àëüíîå ñîñòîÿíèå àâòîìàòà C áóäåò ñîîòâåòñòâîâàòü åãî íà-
÷àëüíîìó ñîñòîÿíèþ.
ÑÎÅÄÈÍÅÍÈÅ ÌÎÄÓËÅÉ ÏÓÒÅÌ ÎÒÎÆÄÅÑÒÂËÅÍÈß ÑÎÑÒÎßÍÈÉ
Ýòà îïåðàöèÿ ñîñòîèò â îòîæäåñòâëåíèè ñîñòîÿíèé, ïðèíàäëåæàùèõ äâóì ðàç-
ëè÷íûì ìîäóëÿì. Åå ñïåöèôèêàöèÿ çàêëþ÷àåòñÿ â ñïåöèôèêàöèè äëÿ êàæäîãî
ìîäóëÿ óñëîâèÿ ïåðåõîäà, èìåþùåãî âèä F t f t( )& ( ) 1 , ãäå F t( ) 1 — âíóò-
ðåííÿÿ ÷àñòü óñëîâèÿ, òàêàÿ, ÷òî F t( ) ñòðîãî âûäåëÿåò îòîæäåñòâëÿåìîå ñîñòîÿ-
íèå â ñîîòâåòñòâóþùåì ìîäóëå, à f t( ) — âíåøíÿÿ ÷àñòü, ïîñòðîåííàÿ èç àòî-
ìîâ íóëåâîãî ðàíãà, îáðàçîâàííûõ ñ ïîìîùüþ âõîäíûõ ñèìâîëîâ èç îáúåäèíå-
íèÿ ñèãíàòóð ñîåäèíÿåìûõ ìîäóëåé. Ôîðìóëà f t( ) îïðåäåëÿåò ìíîæåñòâî
ïåðåõîäîâ èç îòîæäåñòâëÿåìîãî ñîñòîÿíèÿ, óäîâëåòâîðÿþùèõ ýòîé ôîðìóëå.
Âíåøíÿÿ ÷àñòü óñëîâèÿ ïåðåõîäà äëÿ îäíîãî ìîäóëÿ ÿâëÿåòñÿ îòðèöàíèåì
âíåøíåé ÷àñòè óñëîâèÿ ïåðåõîäà äëÿ äðóãîãî ìîäóëÿ.
Ïóñòü ïðè ñîåäèíåíèè àâòîìàòîâ A QA A A�
�� �( ), , � è B QB B B�
�� �( ), , �
ñîîòâåòñòâóþùèå óñëîâèÿ ïåðåõîäà èìåþò âèä F t f t1 1( )& ( ) è F t f t2 1( )& ( ) � .
Óñëîâèå F t1 ( ) ñòðîãî âûäåëÿåò â ìîäóëå A îòîæäåñòâëÿåìîå ñîñòîÿíèå q1,
à óñëîâèå F t2 ( ) ñòðîãî âûäåëÿåò â ìîäóëå B îòîæäåñòâëÿåìîå ñîñòîÿíèå q2 . Ïå-
ðåä òåì êàê ýòè ñîñòîÿíèÿ áóäóò îòîæäåñòâëåíû, â ìîäóëå A óäàëÿþòñÿ âñå ïåðå-
õîäû èç ñîñòîÿíèÿ q1, óäîâëåòâîðÿþùèå óñëîâèþ �f t( ), à â ìîäóëå B — âñå ïå-
ðåõîäû èç ñîñòîÿíèÿ q2 , óäîâëåòâîðÿþùèå óñëîâèþ f t( ) . Ïðè ýòîì àâòîìàòû A
è B ðàññìàòðèâàþòñÿ êàê �-àâòîìàòû ñ âõîäíûì àëôàâèòîì � � �( )A B� . Ïîñëå
îòîæäåñòâëåíèÿ ñîñòîÿíèé ïåðåõîäû èç îòîæäåñòâëåííîãî ñîñòîÿíèÿ, óäîâëåòâî-
ðÿþùèå óñëîâèþ f t( ) , îïðåäåëÿþòñÿ àâòîìàòîì A , à ïåðåõîäû, óäîâëåòâîðÿþ-
ùèå óñëîâèþ �f t( ) , — àâòîìàòîì B. Îòñþäà âèäíî, ÷òî ïðè îòîæäåñòâëåíèè ñî-
ñòîÿíèé îáåñïå÷èâàåòñÿ îðòîãîíàëüíîñòü âõîäíûõ óñëîâèé ïåðåõîäîâ èç íèõ, ò.å.
îòîæäåñòâëåíèå íå ïðèâîäèò ê ïîÿâëåíèþ íîâûõ íåäåòåðìèíèðîâàííûõ ïåðåõî-
äîâ. Çàìåòèì, ÷òî çäåñü ðå÷ü èäåò î íåäåòåðìèíèðîâàííîñòè X Y -àâòîìàòîâ.
Ìíîæåñòâî ñîñòîÿíèé àâòîìàòà C, ïîëó÷åííîãî ïóòåì ñîåäèíåíèÿ àâòîìà-
òîâ A è B, ìîæåò ñîäåðæàòü ñîñòîÿíèÿ, íåäîñòèæèìûå èç îòîæäåñòâëåííîãî ñî-
ñòîÿíèÿ. Òàêèå ñîñòîÿíèÿ áóäóò óäàëåíû ïîñëå âûïîëíåíèÿ âñåõ îïåðàöèé ñîå-
äèíåíèÿ ìîäóëåé êîìïîçèöèîííîé ñïåöèôèêàöèè. Åñëè àâòîìàò A èíèöèàëüíûé,
òî åãî íà÷àëüíûå ñîñòîÿíèÿ áóäóò íà÷àëüíûìè ñîñòîÿíèÿìè àâòîìàòà C.
Àâòîìàò C, ïîëó÷åííûé ñ ïîìîùüþ îïåðàöèè ÎÒÑ, ýêâèâàëåíòåí àâòîìàòó,
ïîëó÷åííîìó ïóòåì âûïîëíåíèÿ äâóõ ãðóïï îïåðàöèé ÌÌÏ, îäíà èç êîòîðûõ
îïðåäåëÿåò ïåðåõîäû èç ìîäóëÿ A â B, à äðóãàÿ — èç ìîäóëÿ B â A . Âíóòðåííèå
÷àñòè óñëîâèé âûõîäà â êàæäîé èç ýòèõ ãðóïï ðàâíû ñîîòâåòñòâåííî F t1 1( ) è
F t2 1( ) . Âíåøíèå ÷àñòè óñëîâèé âûõîäà ïåðâîé ãðóïïû ñîîòâåòñòâóþò îòìåò-
êàì îáîáùåííûõ ïåðåõîäîâ èç ñîñòîÿíèÿ q2 , óäîâëåòâîðÿþùèì ôîðìóëå �f t( ) ,
à âíåøíèå ÷àñòè óñëîâèé âûõîäà âòîðîé ãðóïïû — îòìåòêàì îáîáùåííûõ ïåðå-
õîäîâ èç q1, óäîâëåòâîðÿþùèì ôîðìóëå f t( ) . Óñëîâèÿ âõîäà â ìîäóëü B âûäå-
20 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 5
ëÿþò â íåì ñîñòîÿíèÿ, â êîòîðûå îñóùåñòâëÿþòñÿ îáîáùåííûå ïåðåõîäû èç ñî-
ñòîÿíèÿ q2 , ñîîòâåòñòâóþùèå óñëîâèÿì âûõîäà ïåðâîé ãðóïïû, à óñëîâèÿ âõîäà
â ìîäóëü A — ñîñòîÿíèÿ, â êîòîðûå îñóùåñòâëÿþòñÿ îáîáùåííûå ïåðåõîäû èç q1,
ñîîòâåòñòâóþùèå óñëîâèÿì âûõîäà âòîðîé ãðóïïû.
Îïåðàöèÿ ÎÒÑ ìîæåò èñïîëüçîâàòüñÿ äâîÿêî: êàê îïåðàöèÿ ïåðåõîäà îò ìî-
äóëÿ A ê ìîäóëþ B è êàê îïåðàöèÿ äâóñòîðîííåãî ñîåäèíåíèÿ ìîäóëåé, îáåñïå-
÷èâàþùàÿ ïåðåõîä îò ìîäóëÿ A ê ìîäóëþ B è îáðàòíî.  ïåðâîì ñëó÷àå îòîæäå-
ñòâëÿåìîå ñîñòîÿíèå â ìîäóëå B íå äîñòèæèìî èç ñåáÿ ñ ïîìîùüþ ïóòåé, íà÷è-
íàþùèõñÿ ïåðåõîäàìè, óäîâëåòâîðÿþùèìè óñëîâèþ �f t( ) , èëè ñòàíîâèòñÿ
òàêîâûì âñëåäñòâèå ïåðåõîäà èç ìîäóëÿ B ê äðóãîìó ìîäóëþ. Âî âòîðîì ñëó÷àå
â ìîäóëå B ñóùåñòâóþò ïóòè èç îòîæäåñòâëåííîãî ñîñòîÿíèÿ â ñåáÿ, íà÷èíàþ-
ùèåñÿ ïåðåõîäàìè, óäîâëåòâîðÿþùèìè óñëîâèþ �f t( ) . Åñëè ïðè âîçâðàòå
â îòîæäåñòâëåííîå ñîñòîÿíèå çíà÷åíèå óñëîâèÿ f t( ) ñòàíîâèòñÿ èñòèííûì, òî
îñóùåñòâëÿåòñÿ ïåðåõîä ê ìîäóëþ A .
Âîçìîæíî îòîæäåñòâëåíèå íåñêîëüêèõ ñîñòîÿíèé îäíîãî ìîäóëÿ ñ îäíèì è
òåì æå ñîñòîÿíèåì òàêîãî æå êîëè÷åñòâà êîïèé äðóãîãî è îòîæäåñòâëåíèå îäíî-
ãî ñîñòîÿíèÿ ñ íåñêîëüêèìè ñîñòîÿíèÿìè äðóãîãî ìîäóëÿ.
Ñîñòîÿíèÿ q1 è q2 îäíîãî è òîãî æå àâòîìàòà íàçûâàþòñÿ ñîâìåñòèìûìè,
åñëè âñå ïåðåõîäû èç íèõ, èìåþùèå îäèíàêîâûå âõîäíûå óñëîâèÿ, ðàçëè÷àþòñÿ
òîëüêî ýòèìè ñîñòîÿíèÿìè, ò.å. ñòàíîâÿòñÿ îäèíàêîâûìè, åñëè q1 è q2 â íèõ çà-
ìåíèòü îäíèì è òåì æå ñîñòîÿíèåì. Îòîæäåñòâëåíèå ñîâìåñòèìûõ ñîñòîÿíèé ÿâ-
ëÿåòñÿ ýêâèâàëåíòíûì ïðåîáðàçîâàíèåì àâòîìàòà. Îòîæäåñòâëåíèå îäíîãî ñî-
ñòîÿíèÿ ìîäóëÿ A ñ íåñêîëüêèìè ñîñòîÿíèÿìè ìîäóëÿ B äîïóñêàåòñÿ òîëüêî
â òîì ñëó÷àå, êîãäà îòîæäåñòâëÿåìûå ñîñòîÿíèÿ ìîäóëÿ B ñîâìåñòèìû.
Êàê îòìå÷àëîñü, îïåðàöèþ îòîæäåñòâëåíèÿ ñîñòîÿíèé q1 è q2 ìîæíî çàìå-
íèòü íåñêîëüêèìè îïåðàöèÿìè ÌÌÏ, ÷òî ïîçâîëÿåò ïðè ñîåäèíåíèè ìîäóëåé
îãðàíè÷èòüñÿ òîëüêî îïåðàöèåé ÌÌÏ, îäíàêî ýòî ìîæåò óâåëè÷èòü êîëè÷åñòâî
ñîñòîÿíèé â îáúåäèíåííîì àâòîìàòå è íå âñåãäà óäîáíî ïðè ñïåöèôèêàöèè ñîå-
äèíÿåìûõ ìîäóëåé.
ÒÐÅÁÎÂÀÍÈß Ê ÂÈÄÓ ÑÎÅÄÈÍßÅÌÛÕ ÀÂÒÎÌÀÒÎÂ
Åñëè â ñïåöèôèêàöèÿõ ñâÿçåé ìåæäó ìîäóëÿìè ôèãóðèðóåò íåñêîëüêî óñëîâèé
ñòðîãîãî âûäåëåíèÿ ñîñòîÿíèé â îäíîì è òîì æå ìîäóëå, òî ýòîò ìîäóëü äîë-
æåí áûòü ïðåäñòàâëåí â òàêîì âèäå, ÷òîáû äëÿ êàæäîãî èç ýòèõ óñëîâèé îí
èìåë îäíî èëè áîëåå ñîñòîÿíèé, ñòðîãî âûäåëÿåìûõ ýòèì óñëîâèåì. Ïóñòü
F t F tk1 ( ), , ( )� — âñå ðàçëè÷íûå óñëîâèÿ, ñòðîãî âûäåëÿþùèå ñîñòîÿíèÿ â ìî-
äóëå A . Ïðåäïîëàãàåòñÿ, ÷òî ýòè óñëîâèÿ ïîïàðíî îðòîãîíàëüíû. Òîãäà àâòîìàò
A Q A�
��, , � , ñîîòâåòñòâóþùèé ìîäóëþ A , äîëæåí óäîâëåòâîðÿòü òðåáîâà-
íèþ, ÷òîáû äëÿ êàæäîé F ti ( ) (i k�1, ,� ) ôîðìóëà � � � � ��q Q iP q R F t( ( ) ( ( ))
� �P q R F ti( ) ( ( ))) áûëà èñòèííîé. Ýòî òðåáîâàíèå, ïðè íåîáõîäèìîñòè, îáåñ-
ïå÷èâàåòñÿ ýêâèâàëåíòíûì ïðåîáðàçîâàíèåì àâòîìàòà A ïóòåì ðàñùåïëåíèÿ
åãî ñîñòîÿíèé. Àíàëîãè÷íîå òðåáîâàíèå äîëæíî âûïîëíÿòüñÿ è â àâòîìàòå C
äëÿ ìíîæåñòâà ñîñòîÿíèé �QA .
Äëÿ àâòîìàòà ñ êîíå÷íîé ïàìÿòüþ ââåäåì ïîíÿòèå ãëóáèíû ðàçäåëèìîñòè
ñîñòîÿíèé êàê òàêîå íàèìåíüøåå íàòóðàëüíîå k, ÷òî äëÿ ëþáûõ äâóõ åãî ñîñòîÿ-
íèé q1 è q2 P q P qk k( ) ( )1 2� � � . Çàìåòèì, ÷òî ãëóáèíà ðàçäåëèìîñòè ñîñòîÿ-
íèé îòëè÷àåòñÿ îò ãëóáèíû ïàìÿòè àâòîìàòà òîëüêî â òîì ñëó÷àå, åñëè îí èìååò
ýêâèâàëåíòíûå ñîñòîÿíèÿ. Òàêèì îáðàçîì, äëÿ àâòîìàòà ñ ãëóáèíîé ðàçäåëèìîñ-
òè ñîñòîÿíèé, ðàâíîé k, â êà÷åñòâå ïðåäûñòîðèé, îäíîçíà÷íî õàðàêòåðèçóþùèõ
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 5 21
òåêóùåå ñîñòîÿíèå ñèñòåìû, ìîæíî ðàññìàòðèâàòü ñëîâà äëèíû k. Ïóñòü ãëóáèíà
ðàçäåëèìîñòè ñîñòîÿíèé àâòîìàòà A ðàâíà k. Âñëåäñòâèå äîáàâëåíèÿ ïåðåõîäîâ
â íåêîòîðûå ñîñòîÿíèÿ èç �QA àâòîìàòà C ìíîæåñòâà ñëîâ äëèíû k, ïðåäñòàâèìûõ
ñîñòîÿíèÿìè èç �QA , ìîãóò îòëè÷àòüñÿ îò àíàëîãè÷íûõ ìíîæåñòâ äëÿ ñîîòâåòñòâó-
þùèõ ñîñòîÿíèé àâòîìàòà A . Ïîýòîìó óñëîâèå � � � � �� �q Q iA
P q R F t( ( ) ( ( ))
� �P q R F ti( ) ( ( ))) ìîæåò áûòü ëîæíûì, ò.å. äëÿ íåêîòîðûõ ñîñòîÿíèé èç �QA
óñëîâèÿ èõ ñòðîãîãî âûäåëåíèÿ ìîãóò íå âûïîëíÿòüñÿ. Äëÿ èñêëþ÷åíèÿ òàêîé ñè-
òóàöèè ïðåîáðàçîâàíèå ìíîæåñòâà ñîñòîÿíèé �QA îñóùåñòâëÿåòñÿ â ðàìêàõ àâòî-
ìàòà, ïîëó÷åííîãî ïîãðóæåíèåì àâòîìàòà A â êîíòåêñò, îïðåäåëÿåìûé ñâÿçÿìè
ìîäóëÿ A ñ äðóãèìè ìîäóëÿìè. Êîíòåêñò — ýòî ìíîæåñòâî ïîñëåäîâàòåëüíîñòåé
ïåðåõîäîâ, âåäóùèõ â ñîñòîÿíèÿ ðàññìàòðèâàåìîãî ìîäóëÿ. Ìàêñèìàëüíàÿ äëèíà
òàêèõ ïîñëåäîâàòåëüíîñòåé íàçûâàåòñÿ ãëóáèíîé êîíòåêñòà. Îíà îïðåäåëÿåòñÿ
ìàêñèìàëüíîé ãëóáèíîé óñëîâèé, ñòðîãî âûäåëÿþùèõ ñîñòîÿíèÿ â ýòîì ìîäóëå.
Ðàññìîòðèì, êàê ôîðìèðóþòñÿ ÷àñòè êîíòåêñòà ãëóáèíû k, îïðåäåëÿåìûå ñîîò-
âåòñòâåííî îïåðàöèÿìè ÌÌÏ è ÎÒÑ.
Ïóñòü äëÿ ÌÌÏ èç ìîäóëÿ A â ìîäóëü B óñëîâèå âõîäà âûäåëÿåò â àâòîìàòå B
ñîñòîÿíèå q . Ñîîòâåòñòâóþùåå óñëîâèå âûõîäà èç ìîäóëÿ A, ïðåäñòàâëåííîå
â âèäå ìíîæåñòâà ïåðåõîäîâ, âåäóùèõ â ñîñòîÿíèå q, îáðàçóåò ÷àñòü êîíòåêñòà,
îïðåäåëÿåìóþ ýòèì ìåæìîäóëüíûì ïåðåõîäîì.
Ïóñòü îïåðàöèÿ ÎÒÑ çàäàíà óñëîâèÿìè F t f t1 1( )& ( ) è F t f t2 1( )& ( ) � ,
ãäå ïîñëåäíåå óñëîâèå îïðåäåëåíî â ìîäóëå A . Òîãäà ôîðìóëà F t2 ( ) âûäåëÿåò
ñîñòîÿíèå â àâòîìàòå A , à óñëîâèå F t1 ( ) îïðåäåëÿåò ïîñëåäîâàòåëüíîñòü ïåðåõî-
äîâ, âåäóùóþ â ýòî ñîñòîÿíèå è îáðàçóþùóþ ñîîòâåòñòâóþùèé êîíòåêñò.
 öåëÿõ óìåíüøåíèÿ êîëè÷åñòâà ñîñòîÿíèé â ïðåîáðàçîâàííîì àâòîìàòå
óñëîâèå ñòðîãîãî âûäåëåíèÿ ñîñòîÿíèé ìîæíî îñëàáèòü ñëåäóþùèì îáðàçîì.
Ôîðìóëà F t f t( )& ( ) 1 (êàê äëÿ ÌÌÏ, òàê è äëÿ ÎÒÑ) ñòðîãî âûäåëÿåò ñî-
ñòîÿíèå q, åñëè P q R F t( ) ( ( ))� � � è ñóùåñòâóåò òàêàÿ F t1 ( ) , ÷òî P q R F t( ) \ ( ( )) �
� R F t( ( ))1 è F t f t1 1( ) ( ) � � . Äðóãèìè ñëîâàìè, óñëîâèå P q R F t( ) ( ( ))� ìîæåò
íå âûïîëíÿòüñÿ, åñëè âñå ïåðåõîäû â ñîñòîÿíèå q , îïðåäåëÿåìûå îáðàòíûìè
ñâåðõñëîâàìè èç P q R F t( ) \ ( ( )) , ãàðàíòèðóþò ëîæíîñòü ôîðìóëû f t( ) .
ÏÐÈÌÅÐ ÊÎÌÏÎÇÈÖÈÎÍÍÎÃÎ ÏÐÎÅÊÒÈÐÎÂÀÍÈß
Ðàññìîòðèì ïðîöåññ ñïåöèôèêàöèè è ïðîåêòèðîâàíèÿ óïðàâëÿþùåé ÷àñòè ðå-
òðàíñëÿòîðà, ïðèíèìàþùåãî îò ïåðåäàò÷èêà ïîòåíöèàëüíî áåñêîíå÷íóþ ïîñëå-
äîâàòåëüíîñòü äâîè÷íûõ ñëîâ â ïàðàëëåëüíîì êîäå è ïåðåäàþùåãî èõ ïðèåì-
íèêó â ïîñëåäîâàòåëüíîì êîäå. Ïðèåì è ïåðåäà÷à ñëîâ ñèíõðîíèçèðóþòñÿ òàê-
òèðóþùèì ñèãíàëîì, ïîñòóïàþùèì îò ïåðåäàò÷èêà. Ïðè íîðìàëüíîé ðàáîòå
óñòðîéñòâà â êàæäîì òàêòå îñóùåñòâëÿåòñÿ ïðèåì î÷åðåäíîãî ñëîâà îò ïåðå-
äàò÷èêà è ïåðåäà÷à ïðåäûäóùåãî ñëîâà ïðèåìíèêó. Ïðàâèëüíîñòü ïðèåìà ñëîâ
â ðåòðàíñëÿòîðå è ïðèåìíèêå êîíòðîëèðóåòñÿ.  ñëó÷àå íåïðàâèëüíîãî ïðèåìà
ñëîâà â ðåòðàíñëÿòîðå ãåíåðèðóåòñÿ ñèãíàë RW è â ñëåäóþùåì òàêòå îñóùå-
ñòâëÿåòñÿ ïîâòîðíûé ïðèåì ýòîãî æå ñëîâà. Ïðè íåâåðíîì ïðèåìå ñëîâà
â ïðèåìíèêå îí ãåíåðèðóåò ñèãíàë FP, ïîñòóïàþùèé â ðåòðàíñëÿòîð ÷åðåç
îäèí òàêò ïîñëå ïåðåäà÷è ñëîâà, íåâåðíî ïðèíÿòîãî ïðèåìíèêîì.  òå÷åíèå
òàêòà, ïðîøåäøåãî ìåæäó ïåðåäà÷åé ñëîâà è ïîñòóïëåíèåì ñèãíàëà î åãî íå-
âåðíîì ïðèåìå, ìîæåò áûòü ïåðåäàíî î÷åðåäíîå ñëîâî. Ïîýòîìó ïîñëå ïî-
ñòóïëåíèÿ ñèãíàëà FP ðåòðàíñëÿòîð ïîâòîðíî ïåðåäàåò äâà ïîñëåäíèõ ïåðåäàí-
íûõ ñëîâà. Åñëè ñëîâî, íåïîñðåäñòâåííî ñëåäóþùåå çà íåâåðíî ïðèíÿòûì
ïðèåìíèêîì ñëîâîì, íå áûëî ïåðåäàíî, òî ñíà÷àëà îíî äîëæíî áûòü ïåðåäà-
íî, ïîñëå ÷åãî ïîâòîðíî ïåðåäàþòñÿ äâà ïîñëåäíèõ ïåðåäàííûõ ñëîâà. Ñëîâî,
22 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 5
ïåðåäàííîå íåïîñðåäñòâåííî ïîñëå íåâåðíî ïðèíÿòîãî ïðèåìíèêîì ñëîâà,
â ïðèåìíèêå íå êîíòðîëèðóåòñÿ, ïîýòîìó ñèãíàë FP î åãî íåâåðíîì ïðèåìå
ïðèéòè íå ìîæåò. Î÷åâèäíî, ÷òî ðåòðàíñëÿòîð äîëæåí ñîäåðæàòü áóôåð äëÿ
õðàíåíèÿ íå ìåíåå äâóõ ïðèíÿòûõ îò ïåðåäàò÷èêà ñëîâ.
Ôîðìàëèçóåì îïèñàíèå óïðàâëÿþùåé ÷àñòè ðåòðàíñëÿòîðà â âèäå êîìïîçè-
öèîííîé ñïåöèôèêàöèè â ÿçûêå L. Äëÿ ýòîãî îïðåäåëèì äåéñòâèÿ, âûïîëíÿåìûå
ðåòðàíñëÿòîðîì, è ñîîòâåòñòâóþùèå èì óïðàâëÿþùèå ñèãíàëû. Îñíîâíûå äåé-
ñòâèÿ âêëþ÷àþò â ñåáÿ ïðèåì î÷åðåäíîãî ñëîâà, ïîâòîðíûé ïðèåì ñëîâà, ïåðåäà-
÷ó î÷åðåäíîãî ñëîâà è ïîâòîðíóþ ïåðåäà÷ó íåâåðíî ïðèíÿòîãî ïðèåìíèêîì ñëî-
âà. Äëÿ îáîçíà÷åíèÿ ïðèåìà è ïîâòîðíîãî ïðèåìà ñëîâà áóäåì èñïîëüçîâàòü ñî-
îòâåòñòâåííî ñèìâîëû x è y , à äëÿ ïåðåäà÷è è ïîâòîðíîé ïåðåäà÷è —
ñîîòâåòñòâåííî � è w . Ñèãíàë FP çàïîìèíàåòñÿ íà òðèããåðå (â îïåðàöèîííîé ÷àñ-
òè), êîòîðûé óñòàíàâëèâàåòñÿ â 0 ñèãíàëîì w . Ñèãíàë, ïîñòóïàþùèé ñ ýòîãî
òðèããåðà, îáîçíà÷èì TFP. Òàêèì îáðàçîì, ñèãíàòóðà ïðåäèêàòíûõ ñèìâîëîâ ñïå-
öèôèêàöèè èìååò âèä � = {RW, TFP, x , y , � , w}, èç êîòîðûõ RW è TFP — âõîä-
íûå, à x , y , � , w — âûõîäíûå. Êîìïîçèöèîííàÿ ñïåöèôèêàöèÿ ñîñòîèò èç ñïåöè-
ôèêàöèé îñíîâíîãî ìîäóëÿ, âûïîëíÿþùåãî ïðèåì è ïåðåäà÷ó ñëîâ, åñëè ñáîè
â ïðèåìíèêå îòñóòñòâóþò, ìîäóëÿ MFP, âûïîëíÿþùåãî äåéñòâèÿ, ñâÿçàííûå
ñ ïîâòîðíîé ïåðåäà÷åé ñëîâ âñëåäñòâèå ïîñòóïëåíèÿ ñèãíàëà TFP, è ñïåöèôèêà-
öèè ñâÿçåé ìåæäó ýòèìè ìîäóëÿìè.
Ñïåöèôèêàöèÿ îñíîâíîãî ìîäóëÿ
Âõîäíûå: RW.
Âûõîäíûå: x, y , � .
x t RW t( ) ( )� . y t RW t( ) ( )� � . �( ) ( )t RW t� .
Çàìåòèì, ÷òî ñïåöèôèêàöèÿ ïðåäñòàâëÿ-
åò ñîáîé êîíúþíêöèþ ïðèâåäåííûõ ôîðìóë,
ïðåäâàðåííóþ êâàíòîðîì âñåîáùíîñòè �t .
Ýòîé ñïåöèôèêàöèè ñîîòâåòñòâóåò àâòîìàò
ñ îäíèì ñîñòîÿíèåì, ãðàô ïåðåõîäîâ êîòîðîãî
èçîáðàæåí íà ðèñ. 1.
Ñïåöèôèêàöèÿ ìîäóëÿ MFP
Âõîäíûå: RW, TFP.
Âûõîäíûå: x , y , � , w .
y t RW t( ) ( )� � . x t t RW t TFP t( ) ( ( ) ( ) ( ))� � � 1 .
w t t w t TFP t( ) ( ( ) ( ) ( ))� � � 1 1 .
� �( ) ( ( ) ( ) ( ) ( ))t w t t RW t TFP t� � � 1 1 .
w t TFP t( ) ( ) � �1 . ( ( ) ( )) ( )TFP t w t TFP t � �1 1 .
Ïîñëåäíèå äâå ôîðìóëû õàðàêòåðèçóþò ïîâåäåíèå îïåðàöèîííîé ÷àñòè ðå-
òðàíñëÿòîðà è îáóñëîâëèâàþò ÷àñòè÷íîñòü ñèíòåçèðóåìîãî àâòîìàòà. Ãðàô ïåðå-
õîäîâ àâòîìàòà, ñîîòâåòñòâóþùåãî ýòîé ñïåöèôèêàöèè, ïðèâåäåí íà ðèñ. 2.
Ðàññìîòðèì ñíà÷àëà ñîåäèíåíèå ìîäóëåé ñ ïîìîùüþ ìåæìîäóëüíûõ
ïåðåõîäîâ.
Íåîáõîäèìîñòü ïåðåõîäà îò ôóíêöèîíèðîâàíèÿ îñíîâíîãî ìîäóëÿ ê ìîäóëþ
MFP âîçíèêàåò ïðè íàñòóïëåíèè ñîáûòèÿ, ñîîòâåòñòâóþùåãî óñëîâèþ TFP t( ) .
Îäíàêî äàëüíåéøåå ïîâåäåíèå ìîäóëÿ çàâèñèò îò òîãî, áûëî ëè ïåðåäàíî î÷åðåä-
íîå ñëîâî íåïîñðåäñòâåííî ïåðåä ïîñòóïëåíèåì ñèãíàëà TFP, à òàêæå îò çíà÷å-
íèÿ RW â ìîìåíò ïîñòóïëåíèÿ TFP, ÷åìó ñîîòâåòñòâóåò ïåðåõîä â ðàçëè÷íûå ñî-
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 5 23
Ðèñ. 1
ñòîÿíèÿ ìîäóëÿ MFP. Óñëîâèÿ âûõîäà èç îñíîâíîãî ìîäóëÿ, õàðàêòåðèçóþùèå
óêàçàííûå ñèòóàöèè, èìåþò ñëåäóþùèé âèä:
1) RW t t RW t TFP t w t( ) ( ) ( ) ( ) ( ) 1 1� ;
2) RW t t RW t TFP t y t w t( ) ( ) ( ) ( ) ( ) ( ) �1 1� ;
3) � RW t y t RW t TFP t x t t( ) ( ) ( ) ( ) ( ) ( )1 1 � ;
4) � � �RW t y t RW t TFP t y t w t( ) ( ) ( ) ( ) ( ) ( )1 1 .
Ïåðâîìó è âòîðîìó óñëîâèÿì ñîîòâåòñòâóåò óñëîâèå âõîäà â ìîäóëü MFP,
èìåþùåå âèä TFP t w t( ) ( ) è âûäåëÿþùåå ñîñòîÿíèå 3, òðåòüåìó — óñëîâèå âõîäà
RW t TFP t x t t w t( ) ( ) ( ) ( ) ( )� � , âûäåëÿþùåå
ñîñòîÿíèå 2, à ÷åòâåðòîìó — óñëîâèå
� �RW t TFP t y t w t( ) ( ) ( ) ( ) , âûäåëÿþùåå
ñîñòîÿíèå 1. Äëÿ òîãî ÷òîáû âíóòðåííèå
÷àñòè óñëîâèé âûõîäà ñòðîãî âûäåëÿëè
ñîîòâåòñòâóþùèå ñîñòîÿíèÿ â îñíîâíîì
ìîäóëå, îí ïðåîáðàçóåòñÿ ê âèäó,
ïðèâåäåííîìó íà ðèñ. 3.
 ýòîì àâòîìàòå óñëîâèå RW t t( ) ( )� ñòðîãî âûäåëÿåò ñîñòîÿíèå a, à óñëîâèå
�RW t y t( ) ( ) — ñîñòîÿíèå b .
Ïåðåõîä îò ìîäóëÿ MFP ê îñíîâíîìó ìîäóëþ ñïåöèôèöèðóåòñÿ ñëåäóþùè-
ìè óñëîâèÿìè. Óñëîâèÿ âûõîäà èç ìîäóëÿ MFP èìåþò âèä
� �TFP t t RW t TFP t x t t( ) ( ) ( ) ( ) ( ) ( )1 1� � ,
� � �TFP t t RW t TFP t y t( ) ( ) ( ) ( ) ( )1 1� .
Ôîðìóëà �TFP t t( ) ( )� , ñîîòâåòñòâóþùàÿ âíóòðåííåé ÷àñòè îáîèõ óñëîâèé,
ñòðîãî âûäåëÿåò â ìîäóëå MFP ñîñòîÿíèå 4.
Ïåðâîìó èç ýòèõ óñëîâèé ñîîòâåòñòâóåò óñëîâèå âõîäà â îñíîâíîé ìîäóëü
RW t t( ) ( )� , à âòîðîìó — �RW t y t( ) ( ) . Òàêèì îáðàçîì, ñîåäèíåíèå ìîäóëåé îñó-
ùåñòâëÿåòñÿ ñ ïîìîùüþ ÷åòûðåõ îïåðàöèé ÌÌÏ èç îñíîâíîãî ìîäóëÿ â ìîäóëü
MFP è äâóõ îïåðàöèé ÌÌÏ èç ìîäóëÿ MFP â îñíîâíîé ìîäóëü.
Èìåÿ ãðàôû ïåðåõîäîâ àâòîìàòîâ, ñîîòâåòñòâóþùèõ ñïåöèôèêàöèÿì ìîäó-
ëåé, è ñïåöèôèêàöèè ñâÿçåé ìåæäó íèìè, ïîñòðîèì àâòîìàò, çàäàâàåìûé ïðèâå-
24 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 5
Ðèñ. 3
Ðèñ. 2
äåííîé êîìïîçèöèîííîé ñïåöèôèêàöèåé. Ðåçóëüòàòîì ïåðâûõ äâóõ îïåðàöèé
ÿâëÿåòñÿ äîáàâëåíèå äâóõ ïåðåõîäîâ èç ñîñòîÿíèÿ a îñíîâíîãî ìîäóëÿ â ñîñòîÿ-
íèå 3 ìîäóëÿ MFP ñîîòâåòñòâåííî ñ îòìåòêàìè RW � TFP(w) è � RW � TFP( y w, ).
Ïðè ýòîì âõîäíûå óñëîâèÿ îòìåòîê âñåõ èìåâøèõñÿ ïåðåõîäîâ èç ñîñòîÿíèÿ a
óìíîæàþòñÿ íà �TFP. Â ðåçóëüòàòå ñëåäóþùèõ äâóõ îïåðàöèé äîáàâëÿþòñÿ äâà
ïåðåõîäà èç ñîñòîÿíèÿ b îñíîâíîãî ìîäóëÿ â ñîñòîÿíèÿ 2 è 1 ìîäóëÿ TFP ñîîòâåò-
ñòâåííî ñ îòìåòêàìè RW � TFP( , )x � è � RW � TFP( y). Çäåñü òàêæå âõîäíûå óñëîâèÿ
îòìåòîê âñåõ èìåâøèõñÿ ïåðåõîäîâ èç ñîñòîÿíèÿ b óìíîæàþòñÿ íà �TFP.
 ñîîòâåòñòâèè ñ îïåðàöèÿìè ÌÌÏ èç ìîäóëÿ MFP äîáàâëÿþòñÿ äâà ïåðå-
õîäà èç ñîñòîÿíèÿ 4 ýòîãî ìîäóëÿ â ñîñòîÿíèÿ a è b îñíîâíîãî ìîäóëÿ ñîîòâåò-
ñòâåííî ñ îòìåòêàìè RW �� TFP( , )x � è � RW �� TFP( y). Âõîäíûå óñëîâèÿ îòìå-
òîê âñåõ èìåâøèõñÿ ïåðåõîäîâ èç ñîñòîÿíèÿ 4 óìíîæàþòñÿ íà TFP. Òàêèì îáðà-
çîì, ïåðåõîäû èç ýòîãî ñîñòîÿíèÿ â ñîñòîÿíèå 5 óäàëÿþòñÿ è îíî ñòàíîâèòñÿ
íåäîñòèæèìûì èç îñòàëüíûõ ñîñòîÿíèé ìîäóëÿ. Ãðàô àâòîìàòà, ïîëó÷åííûé
â ðåçóëüòàòå âûïîëíåíèÿ âñåõ îïåðàöèé, ñîåäèíÿþùèõ îñíîâíîé ìîäóëü è ìî-
äóëü MFP, ïðèâåäåí íà ðèñ. 4.
Íåñëîæíî çàìåòèòü, ÷òî â ýòîì àâòîìàòå ñîñòîÿíèå 4 ýêâèâàëåíòíî ñîñòîÿíèþ a.
Ñîñòîÿíèÿ 2 è 1 ÷àñòè÷íûå, è ïîñëå ïîäõîäÿùåãî äîîïðåäåëåíèÿ îíè ñòàíîâÿòñÿ
ýêâèâàëåíòíûìè ñîîòâåòñòâåí-
íî ñîñòîÿíèÿì 4 è b. Îòìåòèì,
÷òî ïðîèçâîëüíîå äîîïðåäå-
ëåíèå ýòèõ ñîñòîÿíèé âîçìîæ-
íî, ïîñêîëüêó èõ ÷àñòè÷íîñòü
îáóñëîâëåíà âçàèìîäåéñòâèåì
ñ îïåðàöèîííûì àâòîìàòîì.
Îòîæäåñòâèâ ýêâèâàëåíòíûå
ñîñòîÿíèÿ, ïîëó÷èì àâòîìàò,
èçîáðàæåííûé íà ðèñ. 5.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 5 25
Ðèñ. 4
Ðèñ. 5
Ýòîò æå ðåçóëüòàò ìîæíî ïîëó÷èòü áîëåå ïðîñòûì ïóòåì, èñïîëüçóÿ äâå
îïåðàöèè ÎÒÑ. Ïåðâàÿ îïåðàöèÿ äëÿ îñíîâíîãî ìîäóëÿ èìååò óñëîâèå ïåðåõîäà
RW t x t t TFP t( ) ( ) ( ) ( ) �1 1 1� , à äëÿ ìîäóëÿ MFP — � TFP t t TFP t( ) ( ) ( )1 1� ,
÷òî ñîîòâåòñòâóåò îòîæäåñòâëåíèþ ñîñòîÿíèé a è 4, âûäåëÿåìûõ âíóòðåííèìè
÷àñòÿìè ñîîòâåòñòâóþùèõ óñëîâèé ïåðåõîäà. Âî âòîðîé îïåðàöèè óñëîâèå ïåðå-
õîäà äëÿ îñíîâíîãî ìîäóëÿ èìååò âèä � �RW t y t TFP t( ) ( ) ( )1 1 , à äëÿ ìîäóëÿ
MFP — � � RW t TFP t y t w t TFP t( ) ( ) ( ) ( ) ( )1 1 1 1 , ÷òî ñîîòâåòñòâóåò îòîæäå-
ñòâëåíèþ ñîñòîÿíèé b è 1. Íàïîìíèì, ÷òî ñîåäèíÿåìûå àâòîìàòû ðàññìàòðèâà-
þòñÿ íàä îáúåäèíåííîé ñèãíàòóðîé, ïîýòîìó ïåðåõîäû â îñíîâíîì ìîäóëå ðàñ-
ñìàòðèâàþòñÿ êàê îáîáùåííûå ïåðåõîäû. Òàê, íàïðèìåð, âõîäíîå óñëîâèå RW
îïðåäåëÿåò äâà âõîäíûõ ñèìâîëà: RW�TFP è RW ��TFP. Ïðè îòîæäåñòâëåíèè ñî-
ñòîÿíèé ïåðåõîäû èç ñîñòîÿíèé îñíîâíîãî ìîäóëÿ, óäîâëåòâîðÿþùèå ôîðìóëå
TFP t( ) , óäàëÿþòñÿ. Äëÿ ïîëó÷åíèÿ ïðèâåäåííîãî âûøå àâòîìàòà íåîáõîäèìî
îòîæäåñòâèòü ñîñòîÿíèÿ 2 è 4, ÷òî, âîîáùå ãîâîðÿ, ìîæíî áûëî ñäåëàòü åùå â àâ-
òîìàòå, ñîîòâåòñòâóþùåì ìîäóëþ MFP (ðèñ. 2).
ÇÀÊËÞ×ÅÍÈÅ
 íàñòîÿùåé ðàáîòå ðàññìàòðèâàåòñÿ êîìïîçèöèîííûé ìåòîä ïðîåêòèðîâàíèÿ
ðåàêòèâíûõ àëãîðèòìîâ â ðàìêàõ àâòîìàòíîãî ïîäõîäà ê ïðîåêòèðîâàíèþ [15].
 îñíîâå ýòîãî ìåòîäà ëåæèò ïîíÿòèå êîìïîçèöèîííîé ñïåöèôèêàöèè àâòîìà-
òà è ôîðìàëüíûé ïåðåõîä îò íåå ê åãî ïðîöåäóðíîìó ïðåäñòàâëåíèþ. Êîìïî-
çèöèîííàÿ ñïåöèôèêàöèÿ ñâÿçàíà ñ âûäåëåíèåì ðàçëè÷íûõ ðåæèìîâ ôóíêöèî-
íèðîâàíèÿ ñïåöèôèöèðóåìîãî àëãîðèòìà, êàæäûé èç êîòîðûõ îïðåäåëÿåòñÿ
ñïåöèôèêàöèåé â ÿçûêå L ñîîòâåòñòâóþùåãî àâòîìàòíîãî ìîäóëÿ. Êðîìå òîãî,
òàêàÿ ñïåöèôèêàöèÿ îïðåäåëÿåò ñïîñîáû ïåðåõîäà îò îäíîãî ðåæèìà ôóíê-
öèîíèðîâàíèÿ ê äðóãîìó. Êàæäûé ïåðåõîä ñïåöèôèöèðóåòñÿ ïàðîé ôîðìóë ÿçû-
êà L, îòíîñÿùèõñÿ ê äâóì ðàçëè÷íûì ìîäóëÿì è âûäåëÿþùèõ â ñîîòâåòñòâóþ-
ùèõ àâòîìàòàõ ñîñòîÿíèÿ, èñïîëüçóåìûå äëÿ èõ ñîåäèíåíèÿ. Íà àâòîìàòíîì
(ñåìàíòè÷åñêîì) óðîâíå ïåðåõîäó îò îäíîãî ðåæèìà ê äðóãîìó ñîîòâåòñòâóåò
îïåðàöèÿ ñîåäèíåíèÿ ãðàôîâ ïåðåõîäîâ àâòîìàòîâ.
Ñïåöèôèêàöèÿ ìîäóëÿ ñîñòîèò èç äâóõ ÷àñòåé: ñïåöèôèêàöèè óïðàâëÿþùåãî
êîìïîíåíòà ìîäóëÿ è ëîêàëüíîé ñïåöèôèêàöèè åãî îïåðàöèîííîé ÷àñòè è ñðåäû.
Ëîêàëüíàÿ ñïåöèôèêàöèÿ — ýòî ñïåöèôèêàöèÿ òåõ ñâîéñòâ îïåðàöèîííîé ÷àñòè, êî-
òîðûå íå èçìåíÿþòñÿ â òå÷åíèå ôóíêöèîíèðîâàíèÿ ìîäóëÿ, õîòÿ ìîãóò èçìåíÿòüñÿ
ïðè ïåðåõîäå îò îäíîãî ìîäóëÿ ê äðóãîìó. Èñïîëüçîâàíèå ëîêàëüíîé ñïåöèôèêàöèè
äàåò âîçìîæíîñòü îñóùåñòâëÿòü ëîêàëüíóþ îïòèìèçàöèþ ÷àñòåé ãðàôà ïåðåõîäîâ
àâòîìàòà, ñïåöèôèöèðóåìîãî êîìïîçèöèîííîé ñïåöèôèêàöèåé. Òàêóþ îïòèìèçàöèþ
öåëåñîîáðàçíî îñóùåñòâëÿòü äî ñîåäèíåíèÿ ìîäóëåé â îäèí àâòîìàò, ÷òî óïðîùàåò
ðåøåíèå çàäà÷è îïòèìèçàöèè âñåãî ñïåöèôèöèðóåìîãî àâòîìàòà.
Ðåçóëüòàòîì ñèíòåçà ìîäóëÿ ÿâëÿåòñÿ öèêëè÷åñêèé àâòîìàò. Ïðè ñîåäèíåíèè
ìîäóëåé èñïîëüçóåòñÿ ïîäàâòîìàò ýòîãî àâòîìàòà, âûäåëÿåìûé ñîñòîÿíèÿìè âõî-
äà â ìîäóëü è ñîñòîÿíèÿìè âûõîäà èç íåãî. Áîëåå òîãî, ýòîò àâòîìàò ýêâèâà-
ëåíòíî ïðåîáðàçóåòñÿ ê âèäó, óäîâëåòâîðÿþùåìó òðåáîâàíèÿì, ñâÿçàííûì ñ ïî-
íÿòèåì ñòðîãîãî âûäåëåíèÿ ñîñòîÿíèé. Èìååòñÿ äîñòàòî÷íî ïðîñòàÿ ôîðìàëüíàÿ
ïðîöåäóðà òàêîãî ïðåîáðàçîâàíèÿ, êîòîðàÿ çäåñü íå îïèñàíà.
Ñïåöèôèêàöèÿ îòäåëüíîãî ìîäóëÿ òàêæå ìîæåò áûòü êîìïîçèöèîííîé, ÷òî
ïðèâîäèò ê èåðàðõè÷åñêîé êîìïîçèöèîííîé ñïåöèôèêàöèè. Òàêîå êîìïîçèöèîí-
íîå ïîñòðîåíèå ñïåöèôèêàöèè ñóùåñòâåííî óïðîùàåò åå íàïèñàíèå è, ñëåäîâà-
òåëüíî, óìåíüøàåò âîçìîæíîñòü äîïóùåíèÿ â íåé îøèáîê. Ñèíòåç óïðàâëÿþùåé
÷àñòè àëãîðèòìà ñâîäèòñÿ ê ñèíòåçó áîëåå ïðîñòûõ ÷àñòåé, ÷òî ìîæåò íà íåñêîëü-
26 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 5
êî ïîðÿäêîâ ñîêðàòèòü ñóììàðíîå âðåìÿ ñèíòåçà è çíà÷èòåëüíî ïîâûñèòü êà÷åñ-
òâî ïîëó÷àåìîãî ðåøåíèÿ çà ñ÷åò ëîêàëüíîé îïòèìèçàöèè ñîñòàâëÿþùèõ ÷àñòåé
ñèíòåçèðóåìîãî àâòîìàòà.
ÑÏÈÑÎÊ ËÈÒÅÐÀÒÓÐÛ
1. H a r e l D . Statecharts. A upsilon isual formalism for complex systems // Sci. Comput. Program. —
1987. — 8, N 3. — P. 231–274.
2. H a r e l D . , N a a m a d A . The STATEMATE semantics of statecharts // ACM Trans. Software
Eng. — 1996. — 5. — P. 293–333.
3. Y i - S h e n g H u a n g . Design of traffic light control systems using statecharts // Computer J. —
2006. — 49, N 6. — P. 634–649.
4. A l u r R . , H e n z i n g e r T . Reacti upsilon e modules // Formal Methods in System Design. —
1999. — 15, N 1. — P. 7–48.
5. A l u r R . , G r o s u R . Modular refinement of hierarchic reacti upsilon e machines // Proc. 27th Ann.
ACM Symp. Principles Programming Languages. — New York: ACM Press, 2000. — P. 390–402.
6. P e t r e n k o A . , B o r o d a y S . , G r o z R . Confirming configurations in EFSM testing // IEEE
Trans. Software Eng. — 2004. — 30, N 1. — P. 29–42.
7. B y u n Y . , S a n d e r s B . A . A pattern-based de upsilon elopment methodology for communication
protocols // J. Inform. Sci. and Eng. — 2006. — 22. — P. 315–335.
8. S o w m y a A . , R a m e s h S . Extending statecharts with temporal logic // IEEE Trans. Software
Eng. — 1998. — 24, N 3. — P. 216–231.
9. J e m n i L . , M o s b a h i O . Combining STATEMATE and FNLOG for the specification and the up-
silon erification of complex real time systems // GESTS Intern. Trans. Comput. Sci. and Eng. —
2005. — 20, N 1. — P. 65–76.
10. D r u s i n s k y D . Semantics and runtime monitoring of TL Charts: Statecharts automata with tempo-
ral logic conditional transitions // Electron. Notes Theoret. Comput. Sci. — 2005. — 113, N 3. —
P. 3–21.
11. Ò è ì î ô å å â Â . Ã . , × å á î ò à ð å â À . Í . Óñîâåðøåíñòâîâàííûé ìåòîä ñèíòåçà àâòîìàòà ïî
åãî ñïåöèôèêàöèè â ÿçûêå L // Êèáåðíåòèêà è ñèñòåìíûé àíàëèç. — 2011. — ¹ 3. — Ñ. 3–14.
12. B y u n Y . , S a n d e r s B . A , C h u n g K . A pattern language for communication protocols // Proc.
9th Conf. Pattern Languages Programs (PLoP’02). — Monticello (Ill.): Univ. of Illinois, 2002. —
P. 1–32.
13. × å á î ò à ð å â À . Í . Îá îäíîì ïîäõîäå ê ôóíêöèîíàëüíîé ñïåöèôèêàöèè àâòîìàòíûõ ñèñòåì.
I // Êèáåðíåòèêà è ñèñòåìíûé àíàëèç. — 1993. — ¹ 3. — Ñ. 31–42.
14. × å á î ò à ð å â À . Í . Î êëàññå ôîðìóë ÿçûêà L*, ñïåöèôèöèðóþùèõ àâòîìàòû ñ êîíå÷íîé
ïàìÿòüþ // Òàì æå. — 2010. — ¹ 1. — Ñ. 3–9.
15. × å á î ò à ð å â À . Í . Îá îäíîì ñïîñîáå ñïåöèôèêàöèè ðåàêòèâíûõ àëãîðèòìîâ â ëîãè÷åñêîì
ÿçûêå ïåðâîãî ïîðÿäêà // Ïðîáë. ïðîãðàììèðîâàíèÿ. — 2000. — ¹ 1, 2. — Ñ. 273–279.
Ïîñòóïèëà 16.04.2012
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 5 27
|
| id | nasplib_isofts_kiev_ua-123456789-86267 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 0023-1274 |
| language | Russian |
| last_indexed | 2025-12-02T11:24:41Z |
| publishDate | 2013 |
| publisher | Інститут кібернетики ім. В.М. Глушкова НАН України |
| record_format | dspace |
| spelling | Чеботарев, А.Н. 2015-09-11T19:53:47Z 2015-09-11T19:53:47Z 2013 Композиционный подход к проектированию реактивных алгоритмов / А.Н. Чеботарев // Кибернетика и системный анализ. — 2013. — Т. 49, № 5. — С. 14-27. — Бібліогр.: 15 назв. — рос. 0023-1274 https://nasplib.isofts.kiev.ua/handle/123456789/86267 519.713.1 Запропоновано метод проектування складних автоматів за їх композиційною специфікацією мовою L. Композиційна специфікація складається із специфікацій автоматних модулів та зв’язків між ними. Автомат, що синтезується, одержується шляхом з’єднання графів переходів модулів, синтезованих за їх специфікаціями. A method for the development of complex finite state machines (FSMs) from their compositional specifications in the logical language L is proposed. A compositional specification consists of specifications of automata modules and interconnections between them. The FSM being synthesized is obtained by connecting the state transition graphs of modules synthesized from their specifications. ru Інститут кібернетики ім. В.М. Глушкова НАН України Кибернетика и системный анализ Кибернетика Композиционный подход к проектированию реактивных алгоритмов Композиційний підхід до проектування реактивних алгоритмів Compositional approach to the development of reactive algorithms Article published earlier |
| spellingShingle | Композиционный подход к проектированию реактивных алгоритмов Чеботарев, А.Н. Кибернетика |
| title | Композиционный подход к проектированию реактивных алгоритмов |
| title_alt | Композиційний підхід до проектування реактивних алгоритмів Compositional approach to the development of reactive algorithms |
| title_full | Композиционный подход к проектированию реактивных алгоритмов |
| title_fullStr | Композиционный подход к проектированию реактивных алгоритмов |
| title_full_unstemmed | Композиционный подход к проектированию реактивных алгоритмов |
| title_short | Композиционный подход к проектированию реактивных алгоритмов |
| title_sort | композиционный подход к проектированию реактивных алгоритмов |
| topic | Кибернетика |
| topic_facet | Кибернетика |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/86267 |
| work_keys_str_mv | AT čebotarevan kompozicionnyipodhodkproektirovaniûreaktivnyhalgoritmov AT čebotarevan kompozicíiniipídhíddoproektuvannâreaktivnihalgoritmív AT čebotarevan compositionalapproachtothedevelopmentofreactivealgorithms |