Усовершенствованный метод синтеза автомата по его спецификации в языке L

Запропоновано модифікацію алгоритму синтезу автомата за його логічною специфікацією. В основі цього алгоритму лежить процедура розщеплення компонентів диз’юнктивної форми. Удосконалення методу спрямовані на зменшення кількості найбільш складних процедур, що використовуються в процесі синтезу, та на...

Повний опис

Збережено в:
Бібліографічні деталі
Опубліковано в: :Кибернетика и системный анализ
Дата:2011
Автори: Тимофеев, В.Г., Чеботарев, А.Н.
Формат: Стаття
Мова:Російська
Опубліковано: Інститут кібернетики ім. В.М. Глушкова НАН України 2011
Теми:
Онлайн доступ:https://nasplib.isofts.kiev.ua/handle/123456789/84197
Теги: Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
Назва журналу:Digital Library of Periodicals of National Academy of Sciences of Ukraine
Цитувати:Усовершенствованный метод синтеза автомата по его спецификации в языке L / В.Г. Тимофеев, А.Н. Чеботарев // Кибернетика и системный анализ. — 2011. — Т. 47, № 3. — С. 3-14. — Бібліогр.: 4 назв. — рос.

Репозитарії

Digital Library of Periodicals of National Academy of Sciences of Ukraine
_version_ 1859708713061842944
author Тимофеев, В.Г.
Чеботарев, А.Н.
author_facet Тимофеев, В.Г.
Чеботарев, А.Н.
citation_txt Усовершенствованный метод синтеза автомата по его спецификации в языке L / В.Г. Тимофеев, А.Н. Чеботарев // Кибернетика и системный анализ. — 2011. — Т. 47, № 3. — С. 3-14. — Бібліогр.: 4 назв. — рос.
collection DSpace DC
container_title Кибернетика и системный анализ
description Запропоновано модифікацію алгоритму синтезу автомата за його логічною специфікацією. В основі цього алгоритму лежить процедура розщеплення компонентів диз’юнктивної форми. Удосконалення методу спрямовані на зменшення кількості найбільш складних процедур, що використовуються в процесі синтезу, та на спрощення формул, до яких ці процедури застосовуються. Крім того, модифікації алгоритму пов’язані зі збільшенням його природного паралелізму. A modification of an algorithm for automaton synthesis from a logical specification is proposed. This algorithm is based on the procedure of splitting components of disjunctive form. Improvements are aimed at decreasing the number of most complex procedures used in the synthesis and reducing the complexity of formulas processed by the procedures. Moreover, the modification enhances the natural parallelism of the algorithm.
first_indexed 2025-12-01T03:59:08Z
format Article
fulltext Â.Ã. ÒÈÌÎÔÅÅÂ, À.Í. ×ÅÁÎÒÀÐÅ ÓÄÊ 519.713.1 ÓÑÎÂÅÐØÅÍÑÒÂÎÂÀÍÍÛÉ ÌÅÒÎÄ ÑÈÍÒÅÇÀ ÀÂÒÎÌÀÒÀ ÏÎ ÅÃÎ ÑÏÅÖÈÔÈÊÀÖÈÈ Â ßÇÛÊÅ L Êëþ÷åâûå ñëîâà: ÿçûê L, ñèíòåç àâòîìàòà, äèçúþíêòèâíàÿ ôîðìà, íîðìàëüíàÿ ôîðìà, îðòîãîíàëèçàöèÿ äèçúþíêòèâíîé ôîðìû, ìíîæèòåëè ðàñùåïëåíèÿ. ÂÂÅÄÅÍÈÅ Äàííàÿ ðàáîòà âûïîëíåíà â ðàìêàõ ìåòîäîëîãèè ïðîåêòèðîâàíèÿ ðåàêòèâíûõ ñèñòåì [1], â îñíîâå êîòîðîé ëåæèò ñèíòåç àâòîìàòíûõ ìîäåëåé ñèñòåì ïî ñïå- öèôèêàöèè òðåáîâàíèé ê èõ ôóíêöèîíèðîâàíèþ.  êà÷åñòâå ÿçûêà ñïåöèôèêà- öèè ðàññìàòðèâàåòñÿ ëîãè÷åñêèé ÿçûê L [2]. Ââèäó ñëîæíîñòè ïðàêòè÷åñêèõ çà- äà÷ ïðîåêòèðîâàíèÿ áîëüøîå çíà÷åíèå èìååò ýôôåêòèâíîñòü àëãîðèòìîâ ñèíòåçà.  íàñòîÿùåé ñòàòüå ïðåäëàãàåòñÿ óñîâåðøåíñòâîâàíèå ìåòîäà ñèíòåçà àâòîìàòà, îñíîâàííîãî íà ðàñùåïëåíèè ïîäôîðìóë ñïåöèôèêàöèè [3]. Ñîîòâåòñòâóþùèé àëãîðèòì èñïîëüçóåò ïðåäñòàâëåíèå ñïåöèôèêàöèè â äèçúþíêòèâíîé ôîðìå. Íàèáîëåå ñëîæíîé ïðîöåäóðîé òàêîãî ñèíòåçà ÿâëÿåòñÿ îðòîãîíàëèçàöèÿ ìíîæå- ñòâà êîìïîíåíòîâ äèçúþíêòèâíîé ôîðìû. Ïîýòîìó óñîâåðøåíñòâîâàíèå ìåòîäà íàïðàâëåíî íà óìåíüøåíèå êîëè÷åñòâà îðòîãîíàëèçèðóåìûõ ìíîæåñòâ êîìïî- íåíòîâ è óïðîùåíèå ôîðìóë, ê êîòîðûì ïðèìåíÿåòñÿ îïåðàöèÿ îðòîãîíàëèçà- öèè. Êðîìå òîãî, ðàññìàòðèâàåìûå ìîäèôèêàöèè ñâÿçàíû ñ ïîâûøåíèåì ðåãó- ëÿðíîñòè àëãîðèòìà ñèíòåçà, ÷òî óâåëè÷èâàåò âîçìîæíîñòü åãî ðàñïàðàëëåëè- âàíèÿ ïðè ðåàëèçàöèè íà ïàðàëëåëüíûõ âû÷èñëèòåëüíûõ ñèñòåìàõ. Ñòàòüÿ îðãàíèçîâàíà ñëåäóþùèì îáðàçîì.  ðàçä. 1 îïèñàíû ñèíòàêñèñ è ñå- ìàíòèêà ÿçûêà L.  ðàçä. 2 ïðåäñòàâëåí èñõîäíûé àëãîðèòì ñèíòåçà. Ïðåäëàãàå- ìûå ìîäèôèêàöèè ýòîãî àëãîðèòìà è èõ îáîñíîâàíèÿ ïðèâåäåíû â ðàçä. 3, 4. Ðà- áîòà âñåõ ðàññìîòðåííûõ âàðèàíòîâ àëãîðèòìà ñèíòåçà äåìîíñòðèðóåòñÿ íà îä- íîé è òîé æå ôîðìóëå ñïåöèôèêàöèè.  çàêëþ÷åíèè ñðàâíèâàþòñÿ îöåíêè âðåìåííîé ñëîæíîñòè ïðèìåíåíèÿ èñõîäíîãî è ìîäèôèöèðîâàííîãî àëãîðèòìîâ ê ôîðìóëå, èñïîëüçóåìîé â ïðèìåðàõ. 1. ßÇÛÊ ÑÏÅÖÈÔÈÊÀÖÈÈ L ßçûê L [2] ÿâëÿåòñÿ ôðàãìåíòîì ëîãèêè ïðåäèêàòîâ ïåðâîãî ïîðÿäêà ñ îäíî- ìåñòíûìè ïðåäèêàòàìè è ôèêñèðîâàííîé îáëàñòüþ èíòåðïðåòàöèè, â êà÷åñòâå êîòîðîé âûñòóïàåò ìíîæåñòâî Z öåëûõ ÷èñåë. Ñïåöèôèêàöèÿ â ÿçûêå L èìååò âèä ôîðìóëû �tF t( ) , èíòåðïðåòèðóåìîé íà ìíîæåñòâå Z . Ôîðìóëà F t( ) ñòðî- èòñÿ ñ ïîìîùüþ ëîãè÷åñêèõ ñâÿçîê èç àòîìàðíûõ ôîðìóë (àòîìîâ) âèäà p t k( )� , ãäå p — îäíîìåñòíûé ïðåäèêàòíûé ñèìâîë, t — ïåðåìåííàÿ, ïðèíè- ìàþùàÿ çíà÷åíèÿ èç ìíîæåñòâà öåëûõ ÷èñåë, ðàññìàòðèâàåìîãî êàê ìíîæåñò- âî ìîìåíòîâ äèñêðåòíîãî âðåìåíè, k — öåëî÷èñëåííàÿ êîíñòàíòà, íàçûâàåìàÿ ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 3 3 © Â.Ã. Òèìîôååâ, À.Í. ×åáîòàðåâ, 2011 ðàíãîì àòîìà. Ðàçíîñòü ìåæäó ìàêñèìàëüíûì è ìèíèìàëüíûì çíà÷åíèÿìè ðàíãîâ àòîìîâ, âñòðå÷àþùèõñÿ â ôîðìóëå, íàçûâàåòñÿ åå ãëóáèíîé. Ïîñêîëüêó ôîðìóëà F t( ) èíòåðïðåòèðóåòñÿ íà ìíîæåñòâå öåëûõ ÷èñåë, äëÿ ïðîèçâîëüíî- ãî öåëîãî k èìååò ìåñòî ýêâèâàëåíòíîñòü � � � �tF t tF t k( ) ( ), ãäå � �tF t k( ) îáîçíà÷àåò ôîðìóëó, ïîëó÷åííóþ èç F t( ) ïðèáàâëåíèåì k ê ðàíãàì âñåõ åå àòîìîâ. Òàêèì îáðàçîì, ìîæíî îãðàíè÷èòüñÿ ôîðìóëàìè F t( ), ó êîòîðûõ ìàê- ñèìàëüíûé ðàíã àòîìîâ ðàâåí 0. Ïðè îïðåäåëåíèè àâòîìàòíîé ñåìàíòèêè ÿçûêîâ ñïåöèôèêàöèè ýòè ÿçûêè è àâòîìàòû ðàññìàòðèâàþòñÿ êàê ôîðìàëèçìû äëÿ çàäàíèÿ ìíîæåñòâ ñâåðõñëîâ â àëôàâèòå äâîè÷íûõ âåêòîðîâ, äëèíà êîòîðûõ ðàâíà êîëè÷åñòâó ðàçëè÷íûõ ïðåäèêàòíûõ ñèìâîëîâ ÿçûêà. Ñåìàíòèêà ôîðìóëû F ÿçûêà L îïðåäåëÿåòñÿ êàê àâ- òîìàò, ñ êîòîðûì àññîöèèðóåòñÿ òî æå ìíîæåñòâî ñâåðõñëîâ, ÷òî è ñ ôîðìóëîé F . Ïóñòü � — êîíå÷íûé àëôàâèò, Z — ìíîæåñòâî öåëûõ ÷èñåë, N Z� � �{z | z � 0} è N Z � � { }z z| 0 . Îòîáðàæåíèÿ u: Z � � è l: N� � � íàçûâàþòñÿ ñîîò- âåòñòâåííî äâóñòîðîííèì ñâåðõñëîâîì (îáîçíà÷àåòñÿ � u u u u u( ) ( ) ( ) ( ) ( )...2 1 0 1 2 ) è ñâåðõñëîâîì (îáîçíà÷àåòñÿ l l( ) ( )...1 2 ). Äëÿ äâóñòîðîííåãî ñâåðõñëîâà u è n �Z îïðåäåëèì n-ñóôôèêñ êàê ñâåðõñëîâî u n u n( ) ( )...� �1 2 Ïóñòü � { }p p pq1 2, , , —� ìíîæåñòâî âñåõ ïðåäèêàòíûõ ñèìâîëîâ, âñòðå÷àþùèõñÿ â ôîðìóëå �tF t( ) (ñèã- íàòóðà ôîðìóëû). Èíòåðïðåòàöèÿ ôîðìóëû �tF t( ) — ýòî íàáîð � � �1 2, ,� ... , � q � îïðåäåëåííûõ íà Z îäíîìåñòíûõ ïðåäèêàòîâ, êîòîðûå ñîîòâåòñòâóþò âñåì ïðåäèêàòíûì ñèìâîëàì èç ìíîæåñòâà . Êàæäûé ïðåäèêàò � i ìîæíî ðàñ- ñìàòðèâàòü êàê äâóñòîðîííåå ñâåðõñëîâî íàä àëôàâèòîì {0, 1}, à íàáîð q òàêèõ ïðåäèêàòîâ — êàê äâóñòîðîííåå ñâåðõñëîâî íàä àëôàâèòîì � � { }0 1, q . Èíòåðïðå- òàöèÿ, ïðè êîòîðîé ôîðìóëà �tF t( ) èñòèííà, íàçûâàåòñÿ ìîäåëüþ äëÿ ýòîé ôîð- ìóëû. Ñ ôîðìóëîé F tF t� � ( ) àññîöèèðóåòñÿ ìíîæåñòâî M F( ) âñåõ ìîäåëåé äëÿ íåå, ò.å. ìíîæåñòâî äâóñòîðîííèõ ñâåðõñëîâ. Êàæäàÿ ôîðìóëà F tF t� � ( ) çàäàåò ìíîæåñòâî ñâåðõñëîâ íàä � , à èìåííî ìíîæåñòâî 0-ñóôôèêñîâ âñåõ äâóñòîðîí- íèõ ñâåðõñëîâ èç M F( ), êîòîðîå îáîçíà÷èì W F( ) . Ðàññìîòðèì òåïåðü àâòîìàòû êàê ñðåäñòâî çàäàíèÿ ìíîæåñòâ ñâåðõñëîâ. Êîíå÷íûì X Y -àâòîìàòîì A íàçûâàåòñÿ ÷åòâåðêà � �X Y Q, , , � , ãäå X è Y — ñîîòâåòñòâåííî âõîäíîé è âûõîäíîé àëôàâèòû, Q — êîíå÷íîå ìíîæåñòâî ñîñòîÿ- íèé, �: Q X Y Q � � � 2 — ôóíêöèÿ ïåðåõîäîâ. X Y -àâòîìàò A X Y Q�� �, , , � íàçûâàåòñÿ êâàçèäåòåðìèíèðîâàííûì, åñëè äëÿ ëþáûõ q Q� , x X� è y Y� èìååì | ( , , )|� q x y 1 . Êâàçèäåòåðìèíèðîâàííûé X Y -àâòîìàò óäîáíî ðàññìàòðèâàòü êàê äåòåð- ìèíèðîâàííûé ÷àñòè÷íûé àâòîìàò áåç âûõîäîâ ñ âõîäíûì àëôàâèòîì � � �X Y . Òàêîé àâòîìàò A Q�� ��, , � , ãäå �:Q Q� �� — ÷àñòè÷íàÿ ôóíêöèÿ ïåðåõîäîâ, íàçîâåì �-àâòîìàòîì A.  êà÷åñòâå àâòîìàòíûõ ìîäåëåé ðåàêòèâíûõ àëãîðèòìîâ èñïîëüçóþòñÿ öèê- ëè÷åñêèå �-àâòîìàòû. �-àâòîìàò A Q�� ��, , � íàçûâàåòñÿ öèêëè÷åñêèì, åñëè äëÿ êàæäîãî q Q� ñóùåñòâóþò òàêèå q q Q1 2, � è � �1 2, �� , ÷òî q q1 1� � �( , ) è q q� � �( , )2 2 . Öèêëè÷åñêèé àâòîìàò ìîæåò áûòü îõàðàêòåðèçîâàí â òåðìèíàõ äî- ïóñòèìûõ ñâåðõñëîâ. Âõîäíîå ñâåðõñëîâî l � � �1 2� äîïóñòèìî â ñîñòîÿíèè q �-àâòîìàòà A, åñëè ñóùåñòâóåò òàêîå ñâåðõñëîâî ñîñòîÿíèé q q q0 1 2� , ãäå q q0 � , ÷òî äëÿ ëþáîãî i � �0 1 2, , , � �( , )q qi i i� ��1 1. Ñâåðõñëîâî l äîïóñòèìî äëÿ àâòîìàòà A, åñëè îíî äîïóñòèìî õîòÿ áû â îäíîì èç åãî ñîñòîÿíèé. Ìíîæåñòâî âñåõ ñâåðõñëîâ, äîïóñòèìûõ â ñîñòîÿíèè q, îáîçíà÷èì W q( ). Ñîñòîÿíèÿ q1 è q2 íàçûâàþòñÿ ýêâèâàëåíòíûìè, åñëè W q W q( ) ( )1 2� . Ìíîæåñ- òâî âñåõ ñâåðõñëîâ, äîïóñòèìûõ äëÿ àâòîìàòà A, îáîçíà÷èì W A( ). Àâòîìàòíóþ ñåìàíòèêó ÿçûêà L îïðåäåëÿåò ñëåäóþùàÿ òåîðåìà. 4 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 3 Òåîðåìà 1 [2]. Äëÿ êàæäîé íåïðîòèâîðå÷èâîé ôîðìóëû F âèäà �tF t( ) ñó- ùåñòâóåò â îáùåì ñëó÷àå íåäåòåðìèíèðîâàííûé íåèíèöèàëüíûé öèêëè÷åñêèé �-àâòîìàò A, äëÿ êîòîðîãî W A W F( ) ( )� . 2. ÑÈÍÒÅÇ ÀÂÒÎÌÀÒÀ ÌÅÒÎÄÎÌ ÐÀÑÙÅÏËÅÍÈÉ Â îñíîâå ñèíòåçà àâòîìàòà ïî ôîðìóëå �tF t( ) ìåòîäîì ðàñùåïëåíèé [3] ëåæèò ïî- íÿòèå íîðìàëüíîé ôîðìû äëÿ ôîðìóëû F t( ) . Çäåñü è äàëåå ôîðìóëó F t( ) ãëóáè- íû r, ñ ñèãíàòóðîé � { }p p pq1 2, , ,� , áóäåì ðàññìàòðèâàòü êàê ïðîïîçèöèî- íàëüíóþ ôîðìóëó ñ ïðîïîçèöèîíàëüíûìè ïåðåìåííûìè p t p tq1 ( ), , ( ),� p t1 1( ), ... , p t p t rq ( ), , ( ) 1 1� , …, p t rq ( ) . Ïóñòü ôîðìóëà F t( ) ïðåäñòàâëåíà â âèäå � � i n i iF t f t 1 1( )& ( ) , (1) ãäå F ti ( ) 1 — ôîðìóëà, ìàêñèìàëüíûé ðàíã àòîìîâ â êîòîðîé íå ïðåâûøàåò –1, f ti ( ) — ôîðìóëà, ïîñòðîåííàÿ èç àòîìîâ ðàíãà 0. Òàêîå ïðåäñòàâëåíèå F t( ) íàçûâàåòñÿ äèçúþíêòèâíîé ôîðìîé, à êîíúþíêöèÿ âèäà F t f ti i( )& ( ) 1 — êîìïîíåíòîì òàêîãî ïðåäñòàâëåíèÿ ñ ëåâîé ÷àñòüþ F ti ( ) 1 è ïðàâîé ÷àñòüþ f ti ( ) . Äèçúþíêòèâíàÿ ôîðìà (1) óäîâëåòâîðÿåò óñëîâèþ îðòîãîíàëüíîñòè, åñëè äëÿ i j� ( , , , )i j n�{ }1 � èìååì F t F ti j( )& ( ) �1 1 0. Òàêàÿ äèçúþíêòèâ- íàÿ ôîðìà F t( ) íàçûâàåòñÿ íîðìàëüíîé ôîðìîé, åñëè äëÿ ëþáûõ i j n, , ,�1 � êîíúþíêöèÿ F t f t F ti i j( )& ( )& ( ) 1 èëè òîæäåñòâåííî ðàâíà íóëþ, èëè ðàâíà F t f ti ij( )& ( ) 1 , ãäå f tij ( ) — îòëè÷íàÿ îò íóëÿ ôîðìóëà, ïîñòðîåííàÿ èç àòî- ìîâ íóëåâîãî ðàíãà. Ïóñòü � { }p pq1, ,� — ñèãíàòóðà ôîðìóëû F t( ), à � ( ) — ìíîæåñòâî âñåõ äâîè÷íûõ âåêòîðîâ äëèíû q. Çàôèêñèðîâàâ íåêîòîðîå óïîðÿäî÷åíèå ìíî- æåñòâà , êàæäîìó ñèìâîëó � �� ( ) ìîæíî ïîñòàâèòü â ñîîòâåòñòâèå ýëåìåí- òàðíóþ êîíúþíêöèþ ~( )� t âèäà ~ ( )& & ~ ( )p t p tq1 � , ãäå ~ ( ) ( ), ( )p t p t p tj j j�{ }, êî- òîðàÿ ïðèíèìàåò çíà÷åíèå 1 íà âåêòîðå �. Ñïåöèôèêàöèè F tF t� � ( ), ãäå F t( ) — ôîðìóëà ñèãíàòóðû , ïðåäñòàâëÿþ- ùàÿ ñîáîé íîðìàëüíóþ ôîðìó � � i n i iF t f t 1 1( )& ( ), îäíîçíà÷íî ñòàâèòñÿ â ñîîòâåò- ñòâèå �-àâòîìàò A F� ( ) ñ âõîäíûì àëôàâèòîì � ( ), ñîñòîÿíèÿìè q qn1, ,� , ãäå q i ni ( , , , )�1 2 � ñîîòâåòñòâóåò ôîðìóëå F ti ( ) 1 , è ôóíêöèåé ïåðåõîäîâ ��, êîòî- ðàÿ îïðåäåëÿåòñÿ ñëåäóþùèì îáðàçîì. Äëÿ � �� ( ) è q q q qi j n, , ,�{ }1 � çíà÷å- íèå � �� ( , )qi ðàâíî q j òîãäà è òîëüêî òîãäà, êîãäà F t f ti i( )& ( )& 1 ~( )&� t & ( ) ( )& ~( )F t F t tj i� 1 � . Åñëè äëÿ qi , � íå ñóùåñòâóåò òàêîãî j n�{ }1 2, , ,� , ïðè êîòîðîì âûïîëíÿåòñÿ ïîñëåäíåå ðàâåíñòâî, çíà÷åíèå � �� ( , )qi íå îïðåäåëåíî. Àâòîìàò A F( ), ñïåöèôèöèðóåìûé ôîðìóëîé F tF t� � ( ), ïðåäñòàâëÿåò ñîáîé ìàê- ñèìàëüíûé öèêëè÷åñêèé ïîäàâòîìàò àâòîìàòà A F� ( ). Òàêèì îáðàçîì, ÷òîáû ïîëó- ÷èòü àâòîìàò A F( ), íåîáõîäèìî äëÿ ôîðìóëû F t( ) ïîñòðîèòü ñîîòâåòñòâóþùóþ åé íîðìàëüíóþ ôîðìó. Ïîñòðîåíèå òàêîé íîðìàëüíîé ôîðìû ñîñòîèò èç äâóõ ýòàïîâ: 1) ýêâèâàëåíòíîå ïðåîáðàçîâàíèå ôîðìóëû F t( ) â äèçúþíêòèâíóþ ôîðìó, óäîâëåòâîðÿþùóþ óñëîâèþ îðòîãîíàëüíîñòè; 2) ïðåîáðàçîâàíèå ýòîé äèçúþíêòèâíîé ôîðìû â íîðìàëüíóþ ôîðìó ïóòåì ðàñùåïëåíèÿ åå êîìïîíåíòîâ. Íà ïåðâîì ýòàïå äèçúþíêòèâíàÿ ôîðìà F t( ) ïðåîáðàçóåòñÿ ïóòåì ïîñëåäî- âàòåëüíîãî ïðèìåíåíèÿ ê ïàðàì åå êîìïîíåíòîâ, íå óäîâëåòâîðÿþùèì óñëîâèþ îðòîãîíàëüíîñòè, ñëåäóþùåãî ñîîòíîøåíèÿ: ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 3 5 ( ( )& ( ) ( )& ( ))F t f t F t f ti i j j � �1 1 � � �( ( )& ( )& ( ) ( )& ( )& ( )F t F t f t F t F t f ti j i i j j1 1 1 1 � �F t F t f t f ti j i j( )& ( )& ( ( ) ( ))).1 1 (2) Òàêîå ïðåîáðàçîâàíèå äèçúþíêòèâíîé ôîðìû F t( ) íàçîâåì åå îðòîãîíàëèçàöèåé. Ïóñòü äèçúþíêòèâíàÿ ôîðìà, ïîëó÷åííàÿ â ðåçóëüòàòå îðòîãîíàëèçàöèè ôîðìóëû F t( ), èìååò âèä � � i n i iF t f t 1 1( )& ( ) . Íà âòîðîì ýòàïå îñóùåñòâëÿåòñÿ ðàñùåïëåíèå êîìïîíåíòîâ F t f ti i( )& ( ) 1 (i n�1, ..., ) ïóòåì óìíîæåíèÿ êàæäîãî èç íèõ ïîñëåäîâàòåëüíî íà ôîðìóëû F t F t F tn1 2( ), ( ), , ( )� . Ðåçóëüòàòîì ðàñ- ùåïëåíèÿ êîìïîíåíòà ÿâëÿåòñÿ äèçúþíêöèÿ ïîëó÷åííûõ ïðîèçâåäåíèé, ïðåä- ñòàâëåííàÿ â äèçúþíêòèâíîé ôîðìå, óäîâëåòâîðÿþùåé óñëîâèþ îðòîãîíàëüíîñ- òè. Ðàñùåïëåíèå êîìïîíåíòà F t f ti i( )& ( ) 1 ïðîèñõîäèò, åñëè ýòà äèçúþíêòèâ- íàÿ ôîðìà ñîñòîèò áîëåå ÷åì èç îäíîãî êîìïîíåíòà, ñêàæåì, F ti1 1( )& & ( ), , ( )& ( )f t F t f ti ik ik1 1� . Î÷åâèäíî, ÷òî äèçúþíêòèâíàÿ ôîðìà, íè îäèí èç êîìïîíåíòîâ êîòîðîé íå ðàñùåïëÿåòñÿ, ïðåäñòàâëÿåò ñîáîé íîðìàëüíóþ ôîðìó. Åñëè ïðîèñõîäèò ðàñùåïëåíèå õîòÿ áû îäíîãî êîìïîíåíòà, òî âûïîëíÿåòñÿ î÷å- ðåäíîé öèêë ðàñùåïëåíèÿ êîìïîíåíòîâ ïîëó÷åííîé äèçúþíêòèâíîé ôîðìû. Ïðè ýòîì ðàñùåïëÿåìûå êîìïîíåíòû óìíîæàþòñÿ òîëüêî íà òå F tij ( ), êîòîðûå ïîëó- ÷åíû â ðåçóëüòàòå ðàñùåïëåíèÿ êîìïîíåíòîâ â ïðåäûäóùåì öèêëå. Âòîðîé ýòàï çàêàí÷èâàåòñÿ, êîãäà â î÷åðåäíîì öèêëå íå ïðîèñõîäèò ðàñùåïëåíèÿ íè îäíîãî êîìïîíåíòà. Èçâåñòíî, ÷òî êîëè÷åñòâî òàêèõ öèêëîâ ðàñùåïëåíèÿ íå ïðåâûøàåò r 1 , ãäå r — ãëóáèíà èñõîäíîé ôîðìóëû. Ïðèìåð 1. Ïðîäåìîíñòðèðóåì ðàáîòó îïèñàííîãî àëãîðèòìà. Äëÿ óïðîùå- íèÿ çàïèñè ñèìâîëû êîíúþíêöèè â ôîðìóëàõ ÷àñòî îïóñêàþòñÿ. Ïóñòü ôîðìóëà F t( ) â ñïåöèôèêàöèè �tF t( ) èìååò ñëåäóþùèé âèä: F t x t y t u t w t y t w t( ) ( ) ( )( ( ) ( )) ( ) ( )� � �3 2 1 1 � � ( ( ) ( ) ( ) ( ) ( ) ( ) ( ) (x t y t u t w t y t u t u t w t3 3 2 1 3 2 1 1))& ( ( ) ( ))y t u t� . Ýòà ôîðìóëà ïðåäñòàâëåíà â ôîðìå (1), ñîñòîèò èç äâóõ êîìïîíåíòîâ è óäîâ- ëåòâîðÿåò óñëîâèþ îðòîãîíàëüíîñòè. Ëåâûå ÷àñòè êîìïîíåíòîâ èìåþò âèä F t x t y t u t w t1 1 3 2 1 1( ) ( ) ( )( ( ) ( )), � � F t x t y t u t w t y t u t u t2 1 3 3 2 1 3 2 1( ) ( ) ( ) ( ) ( ) ( ) ( ) ( � � ) ( ).w t 1  ïåðâîì öèêëå ðàñùåïëåíèé êàæäûé êîìïîíåíò äèçúþíêòèâíîé ôîðìû F t( ) óìíîæàåòñÿ íà ôîðìóëû F t F t1 2( ), ( ) è îðòîãîíàëèçèðóåòñÿ äèçúþíêöèÿ ïî- ëó÷åííûõ ïðîèçâåäåíèé, ïðåäñòàâëåííàÿ â âèäå äèçúþíêòèâíîé ôîðìû. Óìíîæèâ ïåðâûé êîìïîíåíò F t f t1 11( )& ( ) íà F t1 ( ) è F t2 ( ), ïîëó÷èì F t f t F t1 1 11( ) ( )& ( ) � � � x t y t u t w t y t w t x t y t( ) ( )( ( ) ( )) ( ) ( )& ( ) ( )(3 2 1 1 2 1 u t w t( ) ( ))� � � � x t x t y t y t u t w t y t w t( ) ( ) ( ) ( )( ( ) ( )) ( ) ( ),3 2 2 1 1 1 F t f t F t1 1 21( ) ( )& ( ) � � � x t y t u t w t y t w t x t y t( ) ( )( ( ) ( )) ( ) ( )& ( ( ) ( )3 2 1 1 2 2 u t w t( ) ( ) �1 � � y t u t u t w t x t x t y t u t y t( ) ( ) ( ) ( )) ( ) ( ) ( ) ( ) (2 1 3 2 2 1 ) ( ).w t Äèçúþíêöèÿ ïîëó÷åííûõ ïðîèçâåäåíèé èìååò âèä x t x t y t y t u t w t y t w t( ) ( ) ( ) ( )( ( ) ( )) ( ) ( ) � �3 2 2 1 1 1 � x t x t y t u t y t w t( ) ( ) ( ) ( ) ( ) ( )3 2 2 1 , 6 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 3 óäîâëåòâîðÿþùèé óñëîâèþ îðòîãîíàëüíîñòè, è îïðåäåëÿåò ðàñùåïëåíèå ïåð- âîãî êîìïîíåíòà íà äâà êîìïîíåíòà, êîòîðûå îáîçíà÷èì F t f t11 111( )& ( ) è F t f t12 121( )& ( ) . Ïîñëå óìíîæåíèÿ âòîðîãî êîìïîíåíòà íà F t1 ( ) è F t2 ( ) èìååì F t f t F t2 2 11( ) ( )& ( ) � � � ( ( ) ( ) ( ) ( ) ( ) ( ) ( ) (x t y t u t w t y t u t u t w t3 3 2 1 3 2 1 1))( ( ) ( ))&y t u t� & ( ) ( )( ( ) ( )) ( ( ) ( ) ( ) ( )x t y t u t w t x t y t x t u t � � 2 1 3 3 2 2 y t w t( ) ( ) �1 1 � �y t x t u t y t u t w t y t u t y( ) ( ) ( ) ( ) ( ) ( ))( ( ) ( ) (3 2 2 1 1 1 t w t u t w t) ( ) ( ) ( )),� F t f t F t2 2 21( ) ( )& ( ) � � � ( ( ) ( ) ( ) ( ) ( ) ( ) ( ) (x t y t u t w t y t u t u t w t3 3 2 1 3 2 1 1))( ( ) ( ))&y t u t� & ( ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ))x t y t u t w t y t u t u t w t � �2 2 1 2 1 � x t y t x t y t u t u t w t y t w( ) ( ) ( ) ( ) ( ) ( ) ( )( ( ) (3 3 2 2 2 1 1 t u t w t) ( ) ( ))� � � x t y t y t u t u t w t u t w t( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ).3 3 2 2 1 1 Îðòîãîíàëèçàöèÿ äèçúþíêòèâíîé ôîðìû, ñîîòâåòñòâóþùåé äèçúþíêöèè ïî- ëó÷åííûõ ïðîèçâåäåíèé, äàåò ñëåäóþùèå ÷åòûðå êîìïîíåíòà: ( ( ) ( ) ( ) ( ) ( ) ( ) ( )x t y t x t y t u t y t w t �3 3 2 2 2 1 1 � �x t y t x t u t y t u t w t( ) ( ) ( ) ( ) ( ) ( ) ( )3 3 2 2 1 1 1 � �y t x t u t y t u t w t y t u t y( ) ( ) ( ) ( ) ( ) ( ))( ( ) ( ) (3 2 2 1 1 1 t w t u t w t) ( ) ( ) ( )),� x t y t x t y t u t y t u t w t y( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )( 3 3 2 2 2 1 1 1 ( ) ( )),t u t� x t y t x t y t u t u t y t w t u( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( 3 3 2 2 2 1 1 1 t w t) ( ), x t y t x t y t u t u t w t u t y( ) ( ) ( ) ( ) ( ) ( ) ( )( ( ) ( �3 3 2 2 2 1 1 t w t) ( )). Êîìïîíåíòû, íà êîòîðûå ðàñùåïèëñÿ êîìïîíåíò F t f t2 21( )& ( ) , îáîçíà- ÷èì ñîîòâåòñòâåííî F t f t F t f t21 21 24 241 1( )& ( ), , ( )& ( ) � . Âî âòîðîì öèêëå êàæäûé èç ïîëó÷åííûõ øåñòè êîìïîíåíòîâ óìíîæàåòñÿ íà øåñòü ìíîæèòåëåé: F t F t F t11 12 21( ), ( ), ( ) è ò.ä. Îðòîãîíàëèçàöèÿ ñîîòâåòñòâóþ- ùèõ äèçúþíêòèâíûõ ôîðì äàåò ñëåäóþùèé ðåçóëüòàò: êàæäàÿ èç ôîðìóë F t f t11 111( )& ( ) , F t f t21 211( )& ( ) , F t f t22 221( )& ( ) ðàñùåïëÿåòñÿ íà äâà êîì- ïîíåíòà, ôîðìóëû F t f t12 121( )& ( ) è F t f t24 241( )& ( ) — íà òðè, êîìïîíåíò F t f t23 231( )& ( ) íå ðàñùåïëÿåòñÿ, à ïðåîáðàçóåòñÿ â ôîðìóëó F t f t F t23 23 211( )& ( )& ( ) � � x t y t x t y t u t u t y t w t u( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )3 3 2 2 2 1 1 1 ( ) ( )& ( )t w t F t21 � � x t y t x t y t u t u t x t y t w( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )3 3 2 2 2 1 1 1 ( ) ( ) ( ) ( )t y t u t w t 1 .  ñèëó òîãî ÷òî ãëóáèíà èñõîäíîé ôîðìóëû F t( ) ðàâíà òðåì, â ñëåäóþùåì öèêëå íå ðàñùåïèòñÿ íè îäèí èç êîìïîíåíòîâ, ïîýòîìó ïðîöåññ ðàñùåïëåíèÿ çàâåðøàåòñÿ. Ïîëó÷åííàÿ â ðåçóëüòàòå íîðìàëüíàÿ ôîðìà äëÿ ôîðìóëû F t( ) ñîñòîèò èç 13 êîìïîíåíòîâ: 1) x t x t y t x t y t u t w t y t w( ) ( ) ( ) ( ) ( )( ( ) ( )) ( ) � 3 2 2 1 1 1 1 ( )t , 2) x t x t y t x t y t u t w t y t u( ) ( ) ( ) ( ) ( )( ( ) ( )) ( ) � 3 2 2 1 1 1 1 ( ) ( )t w t , 3) x t x t y t x t y t u t y t w t( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) 3 2 2 1 1 1 , 4) x t x t y t x t y t u t y t u t w t( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) 3 2 2 1 1 1 , 5) x t x t y t x t y t u t y t w t( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) 3 2 2 1 1 1 , ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 3 7 6) ( ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )x t y t x t y t u t x t y t w t �3 3 2 2 2 1 1 1 � �x t y t x t u t x t y t u t w t( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )3 3 2 2 1 1 1 1 � y t x t u t x t y t u t w t y t w( ) ( ) ( ) ( ) ( ) ( ) ( )) ( ) (3 2 2 1 1 1 1 t u t) ( ) , 7) ( ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )x t y t x t y t u t x t y t w t �3 3 2 2 2 1 1 1 � �x t y t x t u t x t y t u t w t( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )3 3 2 2 1 1 1 1 � y t x t u t x t y t u t w t y t u( ) ( ) ( ) ( ) ( ) ( ) ( )) ( ) (3 2 2 1 1 1 1 t) , 8) x t y t x t y t u t x t y t u t w( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( 3 3 2 2 2 1 1 1 t y t u t 1) ( ) ( ) , 9) x t y t x t y t u t x t y t u t w( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( 3 3 2 2 2 1 1 1 t y t u t 1) ( ) ( ) , 10) x t y t x t y t u t x t y t u t w( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( 3 3 2 2 2 1 1 1 t y t u t w t 1) ( ) ( ) ( ) , 11) x t y t x t y t u t x t y t u t w( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( 3 3 2 2 2 1 1 1 t y t u t w t 1) ( ) ( ) ( ) , 12) x t y t x t y t u t x t y t u t w( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( 3 3 2 2 2 1 1 1 t y t u t �1)( ( ) ( ) � y t u t w t( ) ( ) ( )) , 13) x t y t x t y t u t x t y t u t w( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( 3 3 2 2 2 1 1 1 t y t u t 1) ( ) ( ) . Ýòîé íîðìàëüíîé ôîðìå ñîîòâåòñòâóåò �-àâòîìàò A F� ( ) , ôóíêöèÿ ïåðåõî- äîâ êîòîðîãî èìååò ñëåäóþùèé âèä: 1: xyw � 1, 2: xyuw � 4, 3: xyw � 6, 4: xyuw � 11, xyw � 2. xyuw � 5. xyw � 7. xyuw � 12. 5: xyuw � 6, 6: xyuw � 1, 7: xyu � 3. 8: xyu � 3. xyuw � 7, xyuw � 2. xyuw � 8, xyuw � 9. 9: xyuw � 1, 10: xyuw � 6, 11: xyuw � 13. 12: xyu � 6, 13: xyu � 6, xyuw � 2, xyuw � 7. xyu � 7, xyu � 7. xyuw � 6, xyuw � 10. xyuw � 7. Ëåãêî çàìåòèòü, ÷òî ïîëó÷åííûé àâòîìàò öèêëè÷åñêèé è åãî ñîñòîÿíèÿ 7 è 8 ýêâèâàëåíòíû. 3. ÌÎÄÈÔÈÊÀÖÈß ÌÅÒÎÄÀ ÐÀÑÙÅÏËÅÍÈÉ Îñíîâíàÿ èäåÿ ïðåäëàãàåìîé ìîäèôèêàöèè ìåòîäà ðàñùåïëåíèé ñîñòîèò â òîì, ÷òîáû ìíîæåñòâî ôîðìóë, íà êîòîðûå ïðè ðàñùåïëåíèè óìíîæàþòñÿ êîìïîíåíòû äèçúþíêòèâíîãî ïðåäñòàâëåíèÿ ñïåöèôèêàöèè, îðòîãîíàëèçèðî- âàòü äî âûïîëíåíèÿ ðàñùåïëåíèÿ. Ïðè ýòîì äèçúþíêòèâíàÿ ôîðìà, ïîëó÷åí- íàÿ â ðåçóëüòàòå òàêèõ óìíîæåíèé, áóäåò óäîâëåòâîðÿòü óñëîâèþ îðòîãîíàëü- íîñòè. Áîëåå òîãî, ïðåäëàãàåòñÿ ïîñòðîèòü íàáîð îðòîãîíàëüíûõ ìíîæèòåëåé (ìíîæèòåëè ðàñùåïëåíèÿ), ïðîèçâåäåíèå êîòîðûõ íà äèçúþíêòèâíóþ ôîðìó èñõîäíîé ôîðìóëû F t( ), óäîâëåòâîðÿþùåé óñëîâèþ îðòîãîíàëüíîñòè, äàåò ñî- îòâåòñòâóþùóþ åé íîðìàëüíóþ ôîðìó. Ýòî ïîçâîëÿåò óïðîñòèòü íàèáîëåå ñëîæíóþ èç èñïîëüçóåìûõ îïåðàöèé, à èìåííî îïåðàöèþ îðòîãîíàëèçàöèè, ïîñêîëüêó îíà ïðèìåíÿåòñÿ ê áîëåå ïðîñòûì ôîðìóëàì ïî ñðàâíåíèþ ñ ìåòî- äîì, îïèñàííûì â [3]. Ïóñòü G t0 ( ) � � � i n i iG t g t 1 0 0 0 1( ) ( ) — äèçúþíêòèâíàÿ ôîðìà, èìåþùàÿ ãëóáèíó r è óäîâëåòâîðÿþùàÿ óñëîâèþ îðòîãîíàëüíîñòè. Íàçîâåì åå äèçúþíêòèâíîé ôîð- ìîé íóëåâîãî óðîâíÿ. Ìíîæèòåëè ðàñùåïëåíèÿ äëÿ ïîñòðîåíèÿ ñîîòâåòñòâóþ- ùåé íîðìàëüíîé ôîðìû ñòðîÿòñÿ êàê âñåâîçìîæíûå ïðîèçâåäåíèÿ ìíîæèòåëåé óðîâíåé îò 1 äî r 1, âçÿòûõ ïî îäíîìó èç êàæäîãî óðîâíÿ. Ìíîæèòåëü j-ãî óðîâ- íÿ ( j r� 1 1, ,� ) ïðåäñòàâëÿåò ñîáîé êîìïîíåíò äèçúþíêòèâíîé ôîðìû ñîîòâåò- ñòâóþùåãî óðîâíÿ, êîòîðàÿ èìååò âèä G t G t g tj i n i j i j j ( ) ( ) ( )� � �1 1 . 8 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 3 Äèçúþíêòèâíàÿ ôîðìà j-ãî óðîâíÿ G tj ( ) ( j r� 1 1, ,� ) ïîëó÷àåòñÿ èç äèçúþíêòèâíîé ôîðìû j 1-ãî óðîâíÿ G t G t g tj i n i j i j j � � � 1 1 1 1 1 1( ) ( ) ( ) êàê ðåçóëü- òàò îðòîãîíàëèçàöèè äèçúþíêòèâíîé ôîðìû, ñîîòâåòñòâóþùåé ôîðìóëå � � i n i j j G t 1 1 1 ( ). Òàêèì îáðàçîì, íà êàæäîì ñëåäóþùåì óðîâíå ãëóáèíà îðòîãîíàëè- çèðóåìîé ôîðìóëû óìåíüøàåòñÿ íà 1. Íîðìàëüíàÿ ôîðìà H t( ) äëÿ ôîðìóëû G t0 ( ) èìååò âèä H t G t i r i( ) ( )&� � 0 1 . Äëÿ äîêàçàòåëüñòâà êîððåêòíîñòè îïèñàííîãî àëãîðèòìà äîñòàòî÷íî ïîêà- çàòü ñïðàâåäëèâîñòü ñëåäóþùèõ äâóõ óòâåðæäåíèé. Óòâåðæäåíèå 1. Ôîðìóëà �tH t( ) èìååò òî æå ñàìîå ìíîæåñòâî ìîäåëåé, ÷òî è ôîðìóëà �tG t0 ( ). Óòâåðæäåíèå 2. Ïîëó÷åííîå äèçúþíêòèâíîå ïðåäñòàâëåíèå H t( ) ÿâëÿåòñÿ íîðìàëüíîé ôîðìîé. Ñïðàâåäëèâîñòü óòâåðæäåíèÿ 1 íåïîñðåäñòâåííî âûòåêàåò èç ñëåäóþùåé ëåììû, äîêàçàííîé â [4]. Ëåììà. Ïóñòü F t( ) — äèçúþíêòèâíàÿ ôîðìà âèäà � � i n i iF t f t 1 1( )& ( ). Òîãäà ìíîæåñòâî ìîäåëåé äëÿ ôîðìóëû � � � t F t i n i 1 ( ) ñîäåðæèò â ñåáå ìíîæåñòâî ìîäå- ëåé äëÿ ôîðìóëû �tF t( ) . Äëÿ äîêàçàòåëüñòâà óòâåðæäåíèÿ 2 èñïîëüçóåòñÿ ñëåäóþùåå î÷åâèäíîå ñâîé- ñòâî îïåðàöèè îðòîãîíàëèçàöèè. Óòâåðæäåíèå 3. Ïóñòü äèçúþíêòèâíàÿ ôîðìà � � i n i iG t g t 1 1( )& ( ) — ðåçóëü- òàò îðòîãîíàëèçàöèè äèçúþíêòèâíîé ôîðìû � � i m i iF t f t 1 1( )& ( ), òîãäà äëÿ ëþáûõ i m�{ }1, ..., è j n�{ }1, ..., ïðîèçâåäåíèå G tj ( ) 1 íà F ti ( ) 1 ëèáî òîæäåñòâåííî ðàâíî 0, ëèáî ñîâïàäàåò ñ G tj ( ) 1 . Ïóñòü G t G t G t g t g i i i r r i i0 0 1 1 1 1 0 0 1 11 1 1( )& ( )& & ( )& ( )& ( ) � ( )& & ( ) ( ) t g t i r r � 1 1 è G t G t G t g t g j j j r r j j0 0 1 1 1 1 0 0 1 11 1 1( )& ( )& & ( )& ( )& ( ) � ( )& & ( ) ( ) t g t j r r � 1 1 — äâà ïðîèçâîëüíûõ êîìïîíåíòà ôîðìóëû H t( ). Ïîêàæåì, ÷òî ïðîèçâåäåíèå ïåðâî- ãî èç íèõ íà ôîðìóëó G t G t G t j j j r r 0 0 1 1 1 1( )& ( )& & ( ) ( ) � ëèáî òîæäåñòâåííî ðàâ- íî 0, ëèáî ñîâïàäàåò ñ G t G t G t g t i i i r r i0 0 1 1 1 11 1 1( )& ( )& & ( )& ( ) ( ) � , ãäå g ti ( ) — ôîðìóëà, ïîñòðîåííàÿ èç àòîìîâ íóëåâîãî ðàíãà. Äëÿ ïðîèçâîëüíîãî k r� { }1 1, ..., ðàññìîòðèì ïðîèçâåäåíèå G t ik k ( ) 1 íà G t j k k ( ) ( ) 1 1 . Êîìïîíåíò äèçúþí- êòèâíîé ôîðìû k-ãî óðîâíÿ G t g t ik k ik k( )& ( ) 1 ïîëó÷àåòñÿ â ðåçóëüòàòå îðòîãîíà- ëèçàöèè äèçúþíêòèâíîé ôîðìû, ñîîòâåòñòâóþùåé ôîðìóëå � � i n i k k G t 1 1 1 ( ) . Çàìå- òèì, ÷òî ïðè ïðåäñòàâëåíèè ôîðìóëû � � i n i k k G t 1 1 1 ( ) â âèäå äèçúþíêòèâíîé ôîðìû êàæäàÿ ôîðìóëà G ti k 1 ( ) ðàâíà äèçúþíêöèè íåêîòîðûõ êîìïîíåíòîâ ýòîé ôîð- ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 3 9 ìû. Ïóñòü ôîðìóëà G t j k k ( ) ( ) 1 1 ðàâíà äèçúþíêöèè l � 1 òàêèõ êîìïîíåíòîâ. Êàê ñëå- äóåò èç óòâåðæäåíèÿ 3, ïðîèçâåäåíèå G t ik k ( ) 1 íà ëåâóþ ÷àñòü êàæäîãî èç l ýòèõ êîìïîíåíòîâ ëèáî òîæäåñòâåííî ðàâíî íóëþ, ëèáî ðàâíî G t ik k ( ) 1 . Îòñþäà ñëå- äóåò, ÷òî ïðîèçâåäåíèå G t ik k ( ) 1 íà G t j k k ( ) ( ) 1 1 ëèáî òîæäåñòâåííî ðàâíî íóëþ, ëèáî ðàâíî G t g t ik k ( )& ( ) 1 , ãäå g t( ) — ôîðìóëà íóëåâîé ãëóáèíû. Ïîñêîëüêó ýòî ñïðàâåä- ëèâî äëÿ ëþáîãî k r� 1 1, ,� è ãëóáèíà ôîðìóëû G t j r r ( ) ( ) 1 1 ðàâíà 0, ïðîèçâåäå- íèå G t G t G t g t g i i i r r i i0 0 1 1 1 1 0 0 1 11 1 1( )& ( )& & ( )& ( )& ( ) � ( )& & ( ) ( ) t g t i r r � 1 1 íà G t G t G t j j j r r 0 0 1 1 1 1( )& ( )& & ( ) ( ) � òàêæå ëèáî òîæäåñòâåííî ðàâíî 0, ëèáî ñîâïàäà- åò ñ G t G t G t g t i i i r r i0 0 1 1 1 11 1 1( )& ( )& & ( )& ( ) ( ) � . Òàêèì îáðàçîì, ôîðìóëà H t( ) ÿâëÿåòñÿ íîðìàëüíîé ôîðìîé. Ïðèìåð 2. Ïðîäåìîíñòðèðóåì ðàáîòó àëãîðèòìà íà ôîðìóëå èç ïðåäûäóùå- ãî ïðèìåðà. Èòàê, F t x t y t u t( ) ( ) ( )( ( )� �3 2 1 w t y t w t( )) ( ) ( ) �1 � � ( ( ) ( ) ( ) ( ) ( ) ( ) ( ) (x t y t u t w t y t u t u t w t3 3 2 1 3 2 1 1))& ( ( ) ( )).y t u t� Ýòà äèçúþíêòèâíàÿ ôîðìà óäîâëåòâîðÿåò óñëîâèþ îðòîãîíàëüíîñòè. Òàêèì îáðàçîì, F t G t( ) ( )� � 0 � � i i iG t g t 1 2 0 01( ) ( ), ãäå G t x t y t u t w t 1 0 1 3 2 1 1( ) ( ) ( )( ( ) ( )) � � , G t x t 2 0 1 3( ) ( ) � y t u t( ) ( )& 3 2 & ( ) ( ) ( ) ( ) ( ).w t y t u t u t w t � 1 3 2 1 1 Ïîñòðîèì ìíîæèòåëè ïåðâîãî óðîâíÿ, ïðåäñòàâèâ ôîðìóëó � �i iG t 1 2 0 ( ) â âèäå äèçúþíêòèâíîé ôîðìû � � � i i iF t f t 1 3 1 11( ) ( ) � � � �x t y t u t w t x t y t u t w t y( ) ( )( ( ) ( )) ( ) ( ) ( ) ( ) (2 1 2 2 1 t u t u t w t 2 1) ( ) ( ) ( ). Ïîñëå îðòîãîíàëèçàöèè ýòîé ôîðìóëû ïîëó÷èì G t G t g t x t y t y t i i i 1 1 4 1 11 2 2 1( ) ( ) ( ) ( ( ) ( ) ( )� � �� � � � �x t y t u t u t w t( ) ( ) ( ))( ( ) ( ))2 1 1 x t y t y t u t u t w t( ) ( ) ( ) ( ) ( ) ( ) �2 2 1 1 � � �x t y t y t u t x t y t u t w t( ) ( ) ( ) ( ) ( ) ( ) ( )( ( )2 2 1 1 2 2 1 u t( )). Ïîñòðîèì ìíîæèòåëè âòîðîãî óðîâíÿ. Äèçúþíêòèâíàÿ ôîðìà ôîðìóëû � �i iG t 1 4 1 ( ) èìååò âèä � � � � i i iF t f t x t y t y t x t y t u t 1 5 2 21 1 1 1( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )� �x t y t y t u t1 1 � � x t y t y t u t x t y t u t( ) ( ) ( ) ( ) ( ) ( ) ( ).1 1 1 1  ðåçóëüòàòå îðòîãîíàëèçàöèè ýòîé ôîðìóëû ïîëó÷àåì G t G t g t i i i 2 1 3 2 21( ) ( ) ( )� �� � � � � � x t y t y t x t y t y t u t x t y( ) ( ) ( ) ( ) ( )( ( ) ( )) ( ) (1 1 1 1 1 t u t 1) ( ) . 10 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 3 Ïåðåìíîæèâ ïîïàðíî ìíîæèòåëè 1-ãî óðîâíÿ íà ìíîæèòåëè 2-ãî óðîâíÿ, ïî- ëó÷èì ìíîæèòåëè ðàñùåïëåíèÿ: M x t y t x t y t x t x t y t u t� � {( ( ) ( ) ( ) ( ) ( ) ( ) ( ) (2 2 1 1 2 1 1 �1))( ( ) ( ) ( )),u t y t w t ( ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )x t y t x t y t x t x t y t u t � 2 2 1 1 2 1 1 1 ) ( ),u t x t y t x t y t u t y t u t w t( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ), 2 2 1 1 1 x t y t x t y t u t y t u t( ) ( ) ( ) ( ) ( )( ( ) ( )), �2 2 1 1 1 x t y t x t y t u t u t( ) ( ) ( ) ( ) ( ) ( ), 2 2 1 1 1 x t y t x t y t u t u t w t y t( ) ( ) ( ) ( ) ( )( ( ) ( )) ( ), �2 2 1 1 1 x t y t x t y t u t y t w t y t u t u( ) ( ) ( ) ( ) ( )( ( ) ( ) ( ) ( ) � �2 2 1 1 1 ( ) ( )),t w t x t y t x t y t u t u t w t( ) ( ) ( ) ( ) ( ) ( ) ( ) . 2 2 1 1 1 } Óìíîæèâ èñõîäíóþ ôîðìóëó G t0 ( ) � � � i i iG t g t 1 2 0 01( ) ( ) íà ìíîæèòåëè èç M , ïîëó÷èì ðåçóëüòàò ðàñùåïëåíèÿ, ò.å. íîðìàëüíóþ ôîðìó äëÿ ôîðìóëû F t( ): H t x t x t y t x t y t u t w t y t( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) (� 3 2 2 1 1 1 1 ) ( )w t � � x t x t y t x t y t u t w t y t u t( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) (3 2 2 1 1 1 1 ) ( )w t � � �x t x t y t x t y t u t y t w t( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )3 2 2 1 1 1 � �x t x t y t x t y t u t y t u t w t( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )3 2 2 1 1 1 � �x t x t y t x t y t u t y t w t( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )3 2 2 1 1 1 � �x t x t y t x t y t u t y t w t( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )3 2 2 1 1 1 � �x t x t y t x t y t u t y t u t w t( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )3 2 2 1 1 1 � ( ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )x t y t x t y t u t x t y t w t3 3 2 2 2 1 1 1 � � �x t y t x t u t x t y t u t w t( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )3 3 2 2 1 1 1 1 � y t x t u t x t y t u t w t y t u( ) ( ) ( ) ( ) ( ) ( ) ( ))( ( )3 2 2 1 1 1 1 ( ) ( ) ( ) ( ))t y t u t w t� � � ( ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )x t y t x t y t u t x t y t w t3 3 2 2 2 1 1 1 � � �x t y t x t u t x t y t u t w t( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )3 3 2 2 1 1 1 1 � y t x t u t x t y t u t w t y t u( ) ( ) ( ) ( ) ( ) ( ) ( )) ( ) (3 2 2 1 1 1 1 t)� � x t y t x t y t u t x t( ) ( ) ( ) ( ) ( ) ( )&3 3 2 2 2 1 & ( ) ( ) ( )( ( ) ( ) ( ) ( ))y t u t w t y t u t y t u t � �1 1 1 � x t y t x t y t u t x t y t u t w( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )3 3 2 2 2 1 1 1 ( ) ( ) ( )t y t u t �1 � x t y t x t y t u t x t y t u t w( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )3 3 2 2 2 1 1 1 ( ) ( ) ( ) ( )t y t u t w t �1 � x t y t x t y t u t x t y t u t w( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )3 3 2 2 2 1 1 1 ( ) ( ) ( )t y t u t �1 � x t y t x t y t u t x t y t u t w( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )3 3 2 2 2 1 1 1 ( )&t 1 & ( ( ) ( ) ( ) ( ) ( ))y t u t y t u t w t� � � x t y t x t y t u t x t y t u t w( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )3 3 2 2 2 1 1 1 ( ) ( ) ( ) ( ).t y t u t w t 1 Ýòîé íîðìàëüíîé ôîðìå ñîîòâåòñòâóåò àâòîìàò ñ 15 ñîñòîÿíèÿìè, êîòîðûé, êàê ñëåäóåò èç ðåçóëüòàòà ïðåäûäóùåãî ïðèìåðà, ñîäåðæèò òðè ïàðû ýêâèâàëåíòíûõ ñîñòîÿíèé. ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 3 11 4. ÂÀÐÈÀÍÒ ÏÎÑÒÐÎÅÍÈß ÌÍÎÆÈÒÅËÅÉ ÐÀÑÙÅÏËÅÍÈß Â ðàññìîòðåííîì àëãîðèòìå ìíîæèòåëÿìè ðàñùåïëåíèÿ j-ãî óðîâíÿ ÿâëÿþòñÿ êîìïîíåíòû äèçúþíêòèâíîé ôîðìû � i n i j i j j G t g t( ) ( )1 . Ïðàâûå ÷àñòè êîìïîíåí- òîâ íå âëèÿþò íè íà êîëè÷åñòâî ìíîæèòåëåé ðàñùåïëåíèÿ êàæäîãî óðîâíÿ, íè íà ëåâûå ÷àñòè êîìïîíåíòîâ ïîëó÷àåìîé íîðìàëüíîé ôîðìû. Ñ ó÷åòîì ýòîãî ìîæíî óïðîñòèòü ïðîöåññ ïîñòðîåíèÿ ìíîæèòåëåé ðàñùåïëåíèÿ, íå âêëþ÷àÿ â íèõ àòîìû íóëåâîãî ðàíãà. Ðàññìîòðèì ñïîñîá ïîñòðîåíèÿ òàêèõ ìíîæèòåëåé j-ãî óðîâíÿ. Ïóñòü F t( ) � � � i n i iG t g t 1 0 0 0 1( ) ( ) — äèçúþíêòèâíàÿ ôîðìà, èìåþùàÿ ãëóáèíó r è óäîâëåòâîðÿþùàÿ óñëîâèþ îðòîãîíàëüíîñòè. Êàæäûé ìíîæèòåëü j-ãî óðîâíÿ ( , ...,j r� 1 1) ïðåäñòàâëÿåò ñîáîé êîìïîíåíò äèçúþíêòèâíîé ôîðìû ñîîòâåòñòâó- þùåãî óðîâíÿ, èìåþùåé âèä G tj ( ) �1 � � i n i j j G t 1 1( ). Ïðàâûå ÷àñòè âñåõ êîìïî- íåíòîâ òàêîé ôîðìû òîæäåñòâåííî ðàâíû åäèíèöå. Äèçúþíêòèâíóþ ôîðìó íóëå- âîãî óðîâíÿ G t0 1( ) ïîëîæèì ðàâíîé � � i n iG t 1 0 0 1( ). Äèçúþíêòèâíàÿ ôîðìà j-ãî óðîâíÿ ( j r� 1 1, ..., ) ïîëó÷àåòñÿ èç äèçúþíêòèâíîé ôîðìû ( j 1)-ãî óðîâíÿ G tj � 1 1( ) � � i n i j j G t 1 1 1 1( ) ñëåäóþùèì îáðàçîì. Ïóñòü F tj ( ) � � � � i n i j j G t 1 1 1 ( ) � � �i m i j i j j F t f t 1 1( )& ( ) , òîãäà G tj ( ) �1 � � i n i j j G t 1 1( ) ïðåäñòàâëÿåò ñîáîé ðåçóëüòàò îðòîãîíàëèçàöèè ôîðìóëû � � i m i j j F t 1 1( ). Íîðìàëüíàÿ ôîðìà H t( ) äëÿ ôîðìóëû F t( ) èìååò âèä H t( ) � F t G t i r i( )& ( )& � 1 1 . Äîêàçàòåëüñòâî òîãî, ÷òî H t( ) ÿâëÿåòñÿ íîðìàëüíîé ôîðìîé ôîðìóëû F t( ), îñóùåñòâëÿåòñÿ òàê æå, êàê â ïðåäûäóùåì ðàçäåëå. Çàìåòèì òîëüêî, ÷òî èç ýêâè- âàëåíòíîñòè ôîðìóë �tF t( ) è � � � tF t G t g t i n i i( )& ( ) ( ) 1 1 ñëåäóåò ýêâèâàëåíòíîñòü ôîðìóë �tF t( ) è � � � tF t G t i n i( )& ( ) 1 1 . Ïðèìåð 3. Ïðîèëëþñòðèðóåì ðàññìîòðåííûé âàðèàíò ïîñòðîåíèÿ ìíîæèòå- ëåé äëÿ ôîðìóëû F t( ) èç ïðåäûäóùèõ ïðèìåðîâ. Èòàê, F t x t y t u t w t y t w t( ) ( ) ( )( ( ) ( )) ( ) ( )� � �3 2 1 1 � � ( ( ) ( ) ( ) ( ) ( ) ( ) ( ) (x t y t u t w t y t u t u t w t3 3 2 1 3 2 1 1))& ( ( ) ( )).y t u t� Ýòà äèçúþíêòèâíàÿ ôîðìà óäîâëåòâîðÿåò óñëîâèþ îðòîãîíàëüíîñòè. Òàêèì îáðàçîì, G t0 ( ) � � �i 1 2 G ti 0 1( ) , ãäå G t x t y t u t w t 1 0 1 3 2 1 1( ) ( ) ( )( ( ) ( )), � � G t x t y t u t w t y t u t u t 2 0 1 3 3 2 1 3 2( ) ( ) ( ) ( ) ( ) ( ) ( ) ( � � 1 1) ( ).w t 12 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 3 Ïîñòðîèì ìíîæèòåëè ïåðâîãî óðîâíÿ G t1 1( ) . Ïðåäñòàâèì ôîðìóëó F t G t i i 1 1 2 0( ) ( )� � � â âèäå F t F t f t i m i i 1 1 1 1 1 1( ) ( ) ( )� �� � � � � �x t y t u t w t x t y t u t w t y( ) ( )( ( ) ( )) ( ) ( ) ( ) ( ) (2 1 2 2 1 t u t u t w t 2 1) ( ) ( ) ( ). Îòñþäà èìååì � � � � � i iF t x t y t x t y t u t y t 1 3 1 1 2 1 2 2 1( ) ( ) ( ) ( ) ( ) ( ) ( 2 1) ( ).u t Ïîñëå îðòîãîíàëèçàöèè ïîëó÷èì G t G t i n i 1 1 11 1 1 ( ) ( ) � �� � � � �( ( ) ( ) ( ) ( ) ( ) ( ))x t y t y t x t y t u t2 2 1 2 1 1 x t y t y t u t( ) ( ) ( ) ( ) �2 2 1 1 � �x t y t y t u t( ) ( ) ( ) ( )2 2 1 1 x t y t u t( ) ( ) ( ). 2 2 1 Ïîñòðîèì ìíîæèòåëè âòîðîãî óðîâíÿ G t2 1( ) . Ïðåäñòàâèì ôîðìóëó F t G t i i 2 1 4 1( ) ( )� � � â âèäå � � � � i m i iF t f t x t y t y t x t y t u 1 2 2 2 1 1 1 1( ) ( ) ( ) ( ) ( ) ( ) ( ) (t x t y t y t u t) ( ) ( ) ( ) ( )� �1 1 � � x t y t y t u t x t y t u t( ) ( ) ( ) ( ) ( ) ( ) ( ).1 1 1 1 Òàêèì îáðàçîì, � � � � � � i iF t x t y t x t x t y t x t 1 5 2 1 1 1 1 1 1( ) ( ) ( ) ( ) ( ) ( ) ( 1 1) ( ).y t Ïîñëå îðòîãîíàëèçàöèè ïîñëåäíåé ôîðìóëû ïîëó÷èì G t G t x t y t x t y t x i n i 2 1 21 1 1 1 1 1 2 ( ) ( ) ( ) ( ) ( ) ( ) � � � �� � ( ) ( ).t y t 1 1 Òåïåðü ìîæíî âû÷èñëèòü ìíîæèòåëè ðàñùåïëåíèÿ, óìíîæèâ ïîïàðíî âñå ìíîæèòåëè 1-ãî óðîâíÿ íà ìíîæèòåëè 2-ãî óðîâíÿ. Èòàê, M x t y t x t y t x t x t y t u t� � {( ( ) ( ) ( ) ( ) ( ) ( ) ( ) (2 2 1 1 2 1 1 1)), ( ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )x t y t x t y t x t x t y t u t � 2 2 1 1 2 1 1 1 ), x t y t x t y t u t( ) ( ) ( ) ( ) ( ), 2 2 1 1 1 x t y t x t y t u t( ) ( ) ( ) ( ) ( ), 2 2 1 1 1 x t y t x t y t u t( ) ( ) ( ) ( ) ( ), 2 2 1 1 1 x t y t x t y t u t( ) ( ) ( ) ( ) ( ), 2 2 1 1 1 x t y t x t y t u t( ) ( ) ( ) ( ) ( ), 2 2 1 1 1 x t y t x t y t u t( ) ( ) ( ) ( ) ( ) . 2 2 1 1 1 } Äëÿ ïîëó÷åíèÿ íîðìàëüíîé ôîðìû äëÿ ôîðìóëû F t( ), ïðåäñòàâëåííîé â âèäå (1) è óäîâëåòâîðÿþùåé óñëîâèþ îðòîãîíàëüíîñòè, åå ñëåäóåò óìíîæèòü íà äèçúþíêöèþ âñåõ ìíîæèòåëåé èç M . ÇÀÊËÞ×ÅÍÈÅ Â íàñòîÿùåé ðàáîòå ïðåäëîæåíà ìîäèôèêàöèÿ àëãîðèòìà ñèíòåçà àâòîìàòà ïî åãî ñïåöèôèêàöèè â ÿçûêå L, ïðåäñòàâëåííîé â äèçúþíêòèâíîé ôîðìå. Ðàññìàò- ðèâàåìûé àëãîðèòì îñíîâàí íà ïðîöåäóðå ðàñùåïëåíèÿ êîìïîíåíòîâ äèçúþí- êòèâíîé ôîðìû. Èòåðàòèâíîå ïðèìåíåíèå ýòîé ïðîöåäóðû ïðåîáðàçóåò èñõîä- íóþ ôîðìóëó ñïåöèôèêàöèè â íîðìàëüíóþ ôîðìó, îäíîçíà÷íî îïðåäåëÿþùóþ ñèíòåçèðóåìûé àâòîìàò. Íàèáîëåå ñëîæíîé îïåðàöèåé ïðîöåäóðû ðàñùåïëåíèÿ ÿâëÿåòñÿ îðòîãîíàëèçàöèÿ ôîðìóëû, ïðåäñòàâëåííîé â äèçúþíêòèâíîé ôîðìå. ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 3 13 Ïîýòîìó ìîäèôèêàöèÿ àëãîðèòìà íàïðàâëåíà íà óìåíüøåíèå êîëè÷åñòâà òàêèõ îïåðàöèé è óïðîùåíèå äèçúþíêòèâíûõ ôîðì, ê êîòîðûì îíè ïðèìåíÿþòñÿ. Ñðàâíèì ñ ýòîé òî÷êè çðåíèÿ èñõîäíûé è ìîäèôèöèðîâàííûé àëãîðèòìû. Ïóñòü èñõîäíàÿ äèçúþíêòèâíàÿ ôîðìà ñïåöèôèêàöèè èìååò ãëóáèíó r. 1.  èñõîäíîì àëãîðèòìå âñå îðòîãîíàëèçèðóåìûå äèçúþíêòèâíûå ôîðìû èìåþò ãëóáèíó r.  ìîäèôèöèðîâàííîì àëãîðèòìå ãëóáèíà ôîðìóë, îðòîãîíàëèçèðóåìûõ â ïåðâîì öèêëå ðàñùåïëåíèÿ, ðàâíà r 1 è â êàæäîì ïîñëåäóþùåì öèêëå óìåíüøàåòñÿ íà 1. Òàêèì îáðàçîì, â ïîñëåäíåì öèêëå îðòîãîíàëèçèðóþòñÿ ôîðìóëû ãëóáèíû 1. 2.  èñõîäíîì àëãîðèòìå â êàæäîì öèêëå ðàñùåïëåíèÿ îðòîãîíàëèçèðóåòñÿ ãðóï- ïà ôîðìóë, ïîëó÷àþùèõñÿ â ïðîöåññå ðàñùåïëåíèÿ êàæäîãî êîìïîíåíòà äèçúþí- êòèâíîé ôîðìû ïðåäûäóùåãî óðîâíÿ.  ìîäèôèöèðîâàííîì àëãîðèòìå â êàæäîì öèêëå îðòîãîíàëèçèðóåòñÿ îäíà äèçúþíêòèâíàÿ ôîðìà, îäíàêî êîëè÷åñòâî êîìïî- íåíòîâ â íåé, êàê ïðàâèëî, ïðåâûøàåò êîëè÷åñòâî êîìïîíåíòîâ â êàæäîé èç ôîð- ìóë, îðòîãîíàëèçèðóåìûõ â ñîîòâåòñòâóþùåì öèêëå èñõîäíîãî àëãîðèòìà. Ïðèâåäåì áîëåå òî÷íûå îöåíêè ñóììàðíîé âðåìåííîé ñëîæíîñòè ïðîöåäóð îðòîãîíàëèçàöèè äëÿ ïðèìåðîâ 1 è 2. Ñëîæíîñòü îðòîãîíàëèçàöèè äèçúþíêòèâ- íîé ôîðìû ãëóáèíû r, ñîñòîÿùåé èç n êîìïîíåíòîâ, (Ort r n( )) ìîæíî ãðóáî îöå- íèòü êàê Cr n( )2 1 , ãäå Cr — êîýôôèöèåíò, ïðîïîðöèîíàëüíûé ãëóáèíå îðòîãîíàëèçèðóåìîé ôîðìóëû.  ïðèìåðå 1 â ïåðâîì öèêëå âûïîëíÿþòñÿ äâå îïåðàöèè îðòîãîíàëèçàöèè îáùåé ñëîæíîñòüþ Ort Ort3 3( ) ( )2 3� , âî âòîðîì — ïÿòü îïåðàöèé îðòîãîíàëèçà- öèè îáùåé ñëîæíîñòüþ Ort Ort Ort Ort3 3 3 3( ) ( ) ( ) ( )2 4 2 2 3� � � . Èòîãî, ñóììàðíàÿ ñëîæíîñòü ðàâíà C C3 2 4 3 33 2 1 2 1 3 2 1 45( ( ) ( ) ( )) � � � .  ïðèìåðå 2 âûïîëíÿþòñÿ äâå îïåðàöèè îðòîãîíàëèçàöèè îáùåé ñëîæíî- ñòüþ Ort Ort2 1( ) ( ) ( ) ( )3 5 2 1 2 1 7 312 3 1 5 2 1� � � � �C C C C . Ó÷èòûâàÿ, ÷òî C C C1 2 3� � , ëåãêî âèäåòü, ÷òî ñóììàðíàÿ ñëîæíîñòü îïåðàöèé îðòîãîíàëèçàöèè äëÿ ìîäèôèöèðîâàííîãî àëãîðèòìà ìåíüøå, ÷åì äëÿ èñõîäíîãî.  ðàññìîòðåííîì â ðàçä. 4 âàðèàíòå ïîñòðîåíèÿ ìíîæèòåëåé ðàñùåïëåíèÿ íå- ñêîëüêî óïðîùåíà îïåðàöèÿ îðòîãîíàëèçàöèè, ïîñêîëüêó íå íóæíî ó÷èòûâàòü ïðà- âûå ÷àñòè îðòîãîíàëèçèðóåìûõ êîìïîíåíòîâ, â ÷àñòíîñòè ñòðîèòü èõ äèçúþí- êöèþ. Êðîìå òîãî, ìîäèôèêàöèè àëãîðèòìà ñóùåñòâåííî óâåëè÷èâàþò åãî åñòåñ- òâåííûé ïàðàëëåëèçì, ÷òî âàæíî ïðè ðåàëèçàöèè àëãîðèòìà íà ïàðàëëåëüíûõ âû÷èñëèòåëüíûõ ñèñòåìàõ. Íåäîñòàòêîì ìîäèôèêàöèé ÿâëÿåòñÿ òî, ÷òî êîëè÷åñòâî ñîñòîÿíèé â ñèíòå- çèðóåìîì àâòîìàòå ìîæåò óâåëè÷èòüñÿ ïî ñðàâíåíèþ ñ ðåçóëüòàòîì, ïîëó÷àåìûì èñõîäíûì àëãîðèòìîì. ÑÏÈÑÎÊ ËÈÒÅÐÀÒÓÐÛ 1. × å á î ò à ð å â À . Í . , à î ë î â è í ñ ê è é À . Ë . Äîêàçàòåëüíîå ïðîåêòèðîâàíèå àëãîðèòìîâ ôóíêöèîíèðîâàíèÿ ðåàêòèâíûõ ñèñòåì // Èñêóññòâåííûé èíòåëëåêò. — 2008. — ¹ 3. — Ñ. 771–780. 2. × å á î ò à ð å â À . Í . Îá îäíîì ïîäõîäå ê ôóíêöèîíàëüíîé ñïåöèôèêàöèè àâòîìàòíûõ ñèñòåì. I // Êèáåðíåòèêà è ñèñòåìíûé àíàëèç. — 1993. — ¹ 3. — Ñ. 31–42. 3. × å á î ò à ð å â À . Í . Ñèíòåç àëãîðèòìà ïî åãî ëîãè÷åñêîé ñïåöèôèêàöèè // Óïð. ñèñòåìû è ìàøèíû. — 2004. — ¹ 5. — Ñ. 53–60. 4. × å á î ò à ð å â À . Í . Ñèíòåç ïðîöåäóðíîãî ïðåäñòàâëåíèÿ àâòîìàòà, ñïåöèôèöèðîâàííîãî â ëîãè- ÷åñêîì ÿçûêå L*. I // Êèáåðíåòèêà è ñèñòåìíûé àíàëèç. — 1997. — ¹ 4. — Ñ. 60–74. Ïîñòóïèëà 09.07.2010 14 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2011, ¹ 3
id nasplib_isofts_kiev_ua-123456789-84197
institution Digital Library of Periodicals of National Academy of Sciences of Ukraine
issn 0023-1274
language Russian
last_indexed 2025-12-01T03:59:08Z
publishDate 2011
publisher Інститут кібернетики ім. В.М. Глушкова НАН України
record_format dspace
spelling Тимофеев, В.Г.
Чеботарев, А.Н.
2015-07-03T16:15:34Z
2015-07-03T16:15:34Z
2011
Усовершенствованный метод синтеза автомата по его спецификации в языке L / В.Г. Тимофеев, А.Н. Чеботарев // Кибернетика и системный анализ. — 2011. — Т. 47, № 3. — С. 3-14. — Бібліогр.: 4 назв. — рос.
0023-1274
https://nasplib.isofts.kiev.ua/handle/123456789/84197
519.713.1
Запропоновано модифікацію алгоритму синтезу автомата за його логічною специфікацією. В основі цього алгоритму лежить процедура розщеплення компонентів диз’юнктивної форми. Удосконалення методу спрямовані на зменшення кількості найбільш складних процедур, що використовуються в процесі синтезу, та на спрощення формул, до яких ці процедури застосовуються. Крім того, модифікації алгоритму пов’язані зі збільшенням його природного паралелізму.
A modification of an algorithm for automaton synthesis from a logical specification is proposed. This algorithm is based on the procedure of splitting components of disjunctive form. Improvements are aimed at decreasing the number of most complex procedures used in the synthesis and reducing the complexity of formulas processed by the procedures. Moreover, the modification enhances the natural parallelism of the algorithm.
ru
Інститут кібернетики ім. В.М. Глушкова НАН України
Кибернетика и системный анализ
Кибернетика
Усовершенствованный метод синтеза автомата по его спецификации в языке L
Удосконалений метод синтезу автомата за його специфікацією у мові L
Improved method for automaton synthesis from its specification in the language L
Article
published earlier
spellingShingle Усовершенствованный метод синтеза автомата по его спецификации в языке L
Тимофеев, В.Г.
Чеботарев, А.Н.
Кибернетика
title Усовершенствованный метод синтеза автомата по его спецификации в языке L
title_alt Удосконалений метод синтезу автомата за його специфікацією у мові L
Improved method for automaton synthesis from its specification in the language L
title_full Усовершенствованный метод синтеза автомата по его спецификации в языке L
title_fullStr Усовершенствованный метод синтеза автомата по его спецификации в языке L
title_full_unstemmed Усовершенствованный метод синтеза автомата по его спецификации в языке L
title_short Усовершенствованный метод синтеза автомата по его спецификации в языке L
title_sort усовершенствованный метод синтеза автомата по его спецификации в языке l
topic Кибернетика
topic_facet Кибернетика
url https://nasplib.isofts.kiev.ua/handle/123456789/84197
work_keys_str_mv AT timofeevvg usoveršenstvovannyimetodsintezaavtomatapoegospecifikaciivâzykel
AT čebotarevan usoveršenstvovannyimetodsintezaavtomatapoegospecifikaciivâzykel
AT timofeevvg udoskonaleniimetodsintezuavtomatazaiogospecifíkacíêûumovíl
AT čebotarevan udoskonaleniimetodsintezuavtomatazaiogospecifíkacíêûumovíl
AT timofeevvg improvedmethodforautomatonsynthesisfromitsspecificationinthelanguagel
AT čebotarevan improvedmethodforautomatonsynthesisfromitsspecificationinthelanguagel