Синтез автомата, специфицированного в языке L*, путем перехода к спецификации в языке L
Рассматривается метод синтеза конечного автомата, специфицированного в логическом языке L*. Метод основан на трансляции спецификации в язык L и синтезе автомата по спецификации в этом языке. Розглядається метод синтезу скінченного автомата, специфікованого логічною мовою L*. Метод базується на транс...
Збережено в:
| Опубліковано в: : | Комп’ютерні засоби, мережі та системи |
|---|---|
| Дата: | 2011 |
| Автори: | , |
| Формат: | Стаття |
| Мова: | Російська |
| Опубліковано: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2011
|
| Онлайн доступ: | https://nasplib.isofts.kiev.ua/handle/123456789/46448 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Цитувати: | Синтез автомата, специфицированного в языке L*, путем перехода к спецификации в языке L / А.Н. Чеботарев, А.К. Богаченко // Комп’ютерні засоби, мережі та системи. — 2011. — № 10. — С. 13-21. — Бібліогр.: 7 назв. — рос. |
Репозитарії
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1859604487974420480 |
|---|---|
| author | Чеботарев, А.Н. Богаченко, А.К. |
| author_facet | Чеботарев, А.Н. Богаченко, А.К. |
| citation_txt | Синтез автомата, специфицированного в языке L*, путем перехода к спецификации в языке L / А.Н. Чеботарев, А.К. Богаченко // Комп’ютерні засоби, мережі та системи. — 2011. — № 10. — С. 13-21. — Бібліогр.: 7 назв. — рос. |
| collection | DSpace DC |
| container_title | Комп’ютерні засоби, мережі та системи |
| description | Рассматривается метод синтеза конечного автомата, специфицированного в логическом языке L*. Метод основан на трансляции спецификации в язык L и синтезе автомата по спецификации в этом языке.
Розглядається метод синтезу скінченного автомата, специфікованого логічною мовою 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 language L and synthesizing an FSM from the specification in this language.
|
| first_indexed | 2025-11-28T03:02:56Z |
| format | Article |
| fulltext |
Комп’ютерні засоби, мережі та системи. 2011, № 10 13
A.N. Chebotarev, A.K. Bogachenko
SYNTHESIS OF AN FSM
SPECIFIED IN THE LANGUAGE
L* BY PASSING
TO THE SPECIFICATION
IN THE LANGUAGE 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 language L and synthesizing an
FSM from the specification in this
language.
Key words: reactive algorithms, lan-
guage L, method of synthesis, FSM.
Розглядається метод синтезу
скінченного автомата, специфі-
кованого логічною мовою L*. Ме-
тод базується на трансляції спе-
цифікації у мову L і синтезі авто-
мата за специфікацією у цій мові.
Ключові слова: реактивні алгори-
тми, мова L, метод синтезу, скін-
ченний автомат.
Рассматривается метод синтеза
конечного автомата, специфици-
рованного в логическом языке L*.
Метод основан на трансляции
спецификации в язык L и синтезе
автомата по спецификации в
этом языке.
Ключевые слова: реактивные ал-
горитмы, язык L, метод синтеза,
конечный автомат.
А.Н. Чеботарев, А.К. Богаченко,
2011
УДК 519.713.1
А.Н. ЧЕБОТАРЕВ, А.К. БОГАЧЕНКО
СИНТЕЗ АВТОМАТА,
СПЕЦИФИЦИРОВАННОГО
В ЯЗЫКЕ L*, ПУТЕМ ПЕРЕХОДА
К СПЕЦИФИКАЦИИ В ЯЗЫКЕ L
Введение. В основе доказательного проекти-
рованию реактивных алгоритмов лежит спе-
цификация функциональных требований
к алгоритму в языке логики первого порядка
с одноместными предикатами и формальный
переход от спецификации к процедурному
представлению алгоритма. Одна из основ-
ных проблем, связанных со спецификацией
свойств алгоритма, состоит в разработке
подходящего языка спецификации. При этом
приходится искать компромисс между выра-
зительными возможностями языка и сложно-
стью алгоритмов проектирования. Для раз-
решения этого противоречия используются
два уровня языка: язык исходной специфи-
кации L* [1], обладающий достаточными для
практических нужд выразительными воз-
можностями и обеспечивающий удобство
записи функциональных требований к алго-
ритму и язык L [2], обладающий сравнитель-
но ограниченными выразительными возмож-
ностями, но эффективно обрабатываемый
процедурами синтеза.
Автоматный подход к проектированию ре-
активного алгоритма характеризуется тем,
что в качестве модели алгоритма использует-
ся сеть взаимодействующих автоматов. Та-
ким образом, основные задачи проектирова-
ния связаны со спецификацией и синтезом
конечных автоматов. Выразительные воз-
можности языка L ограничены автоматами с
конечной памятью [3], что позволило разра-
ботать для спецификаций в этом языке эф-
фективные алгоритмы синтеза, проверки не-
противоречивости спецификации и вери-
А.Н. ЧЕБОТАРЕВ, А.К. БОГАЧЕНКО
Комп’ютерні засоби, мережі та системи. 2011, № 10 14
фикации темпоральных свойств, а также методы проектирования открытых сис-
тем, к которым относятся реактивные алгоритмы. Поэтому язык L* используется
(когда это необходимо) для начальной спецификации автоматов.
В основе рассматриваемого метода синтеза автомата по спецификации в
языке L* лежит переход от этой спецификации к спецификации в языке L [4].
Такой переход дает спецификацию, не эквивалентную исходной, однако, как
показано в [4], автомат, синтезированный по полученной спецификации, содер-
жит подавтомат, совпадающий с автоматом, специфицированным в языке L*.
Состояния, не принадлежащие этому подавтомату, называются фиктивными.
Задача состоит в удалении из синтезированного автомата всех фиктивных со-
стояний. В работе [5] предложен метод определения фиктивности состояний на
основе проверки выполнимости формул языка L* в анализируемом состоянии. В
настоящей работе на основе результатов, полученных в [6], предлагается фик-
тивность состояния определять путем проверки выполнимости в состоянии дос-
таточно простой формулы языка L, что существенно уменьшает сложность про-
цедуры определения фиктивности состояния.
Языки спецификации L и L
*
.
Языки L* и L построены на основе соответствующих фрагментов логики
предикатов первого порядка с одноместными предикатами, определенными на
множестве моментов дискретного времени, в качестве которого выступает мно-
жество Z целых чисел. Спецификация в обоих языках имеет вид формулы
)(ttF , где )(tF – формула с одной свободной переменной t . В языке L
формула )(tF строится с помощью логических связок из атомов вида )( ktp ,
где p – одноместный предикатный символ, t – переменная, принимающая
значения из множества , а k – целочисленная константа (сдвиг во времени).
Язык L* отличается от языка L тем, что при построении формулы )(tF
наряду с атомарными формулами используются формулы вида
))()((&)(&)( 23211 jjijiii tFkttktttFkttt ,
где 321 ,, kkk Z ; )(2 jtF – формула языка L; )(1 itF – формула языка L*.
Такие формулы будем называть -формулами. Для эквивалентного преобразо-
вания формул )(tF такого вида часто используется равносильность [4]
)()(&)1()( tgthtFtF , (1)
где )1( tF обозначает формулу, полученную из )(tF путем замены t на 1t ,
)()( 32 ktFth , а )1()()( 32111 kktFktFtg , если 213 kkk ,
или )(&&)(&)( 2123211 kktFktFktF , если 213 kkk . Правую часть
равносильности (1) назовем 1-разверткой -формулы )(tF .
Для формулы )(tF языка L* следующим образом определим понятие ранга
(обозначается ))((# tF :
СИНТЕЗ АВТОМАТА, СПЕЦИФИЦИРОВАННОГО В ЯЗІКЕ L*, ПУТЕМ ПЕРЕХОДА…
Комп’ютерні засоби, мережі та системи. 2011, № 10 15
1) ( kktp ))((# (ранг атома);
2) если ))()((&)(&)()( 23211 jjijiii tFkttktttFkttttF , то
),max())((# 3211 krkrtF , где ))((# 111 tFr , ))((# 222 tFr ;
3) если )(tF построена из )(tFi , mi ,...,1 с помощью логических связок, то
)))((#,)),((max(#))((# 1 tFtFtF m .
Объектом спецификации и синтеза является частичный, неинициальный, де-
терминированный автомат без выходов AQA ,, , где – конечный вход-
ной алфавит, Q – конечное множество состояний, QQA : – частичная
функция переходов. Такой автомат назовем -автоматом. Автоматная семантика
языков описывается в терминах циклических -автоматов [4].
-автомат AQA ,, называется циклическим, если для каждого Qq
существуют такие 21, и Qqq 21, , что ),( 11 qq A и ),( 22 qq A .
Поведение циклического -автомата удобно описывать в терминах мно-
жеств сверхслов ( -слов) в алфавите , поэтому приведем связанные с ними
определения.
Пусть – конечный алфавит, Z – множество целых чисел,
}0|{ zZzN и }0|{ zZzN . Отображения NlZu :,: и
Ng : называются соответственно двусторонним сверхсловом (обознача-
ется )2()1()0()1()2( uuuuu ), сверхсловом (обозначается )2()1( ll ) и об-
ратным сверхсловом (обозначается )0()1()2(... ggg ) в алфавите . Отрезок
)()...1()( kuuu двустороннего сверхслова u обозначается ),( ku .
Бесконечные отрезки ),( ku и ),1( ku будем называть соответственно
k-префиксом и k-суффиксом двустороннего сверхслова u . Если значение k не
существенно, то будем говорить об -префиксе и -суффиксе. Отрезок )()...1( kll
назовем k-префиксом сверхслова )...2()1( lll .
Сверхслово ..., 21 l в алфавите допустимо в состоянии q -ав-
томата A , если существует такое сверхслово состояний 210 qqq , где qq 0 ,
что для любого 0,1,2,i , 11),( iiiA qq . Множество всех сверхслов,
допустимых в состоянии q , обозначим )(qW .
Обратное сверхслово 01... в алфавите представимо состоянием q
-автомата A, если существует такое обратное сверхслово состояний
012 qqq , где qq 0 , что для любого 1, 2,...i 11),( iiiA qq . Таким
образом, с каждым состоянием q циклического -автомата ассоциируются два
множества сверхслов: множество )(qW всех сверхслов, допустимых в состоянии
q , и множество )(qP всех обратных сверхслов, представимых состоянием q .
А.Н. ЧЕБОТАРЕВ, А.К. БОГАЧЕНКО
Комп’ютерні засоби, мережі та системи. 2011, № 10 16
Поведение автомата A с множеством состояний },,{ 1 nA qqQ представ-
ляет собой семейство множеств сверхслов ),,()( 1 nWWAS , где )( ii qWW ,
),...,1( ni .
Пусть },,{ 1 mpp – множество всех предикатных символов, встречаю-
щихся в формуле F (сигнатура формулы). Интерпретация формулы F – это упо-
рядоченный набор определенных на Z одноместных предикатов m ,...,1 , соот-
ветствующих предикатным символам из . Интерпретацию mI ,...,1
можно представить в виде двустороннего сверхслова в алфавите )( , который
представляет собой множество всех двоичных векторов длины m . Символы ал-
фавита )( иногда удобно рассматривать как отображения вида }1,0{: .
Пусть 1 , проекцией символа )( на 1 будем называть ограничение
отображения на 1 . Понятие проекции символа на 1 естественным образом
распространяется на слова и сверхслова, так что проекция сверхслова в алфавите
)( на 1 есть сверхслово в алфавите )( 1 . В дальнейшем не будем разли-
чать интерпретации и соответствующие им двусторонние сверхслова, поэтому
можно говорить об истинностном значении формулы F на двустороннем
сверхслове u и значении формулы )(tF в некоторой позиции двустороннего
сверхслова u .
Каждой замкнутой формуле F ставится в соответствие множество )(FM
моделей для этой формулы, т. е. множество таких интерпретаций, на которых
F истинна.
Обозначим )(FW множество 0-суффиксов всех моделей из )(FM , а )(FP –
множество 0-префиксов этих моделей.
Двустороннее сверхслово u называется k-сдвигом ( k ) двустороннего
сверхслова u , если для всех i )()( kiuiu . Если u – модель для F , то и
любой ее k-сдвиг принадлежит )(FM . Отсюда следует, что любой -суффикс
модели для F принадлежит )(FW и любой ее -префикс принадлежит )(FP .
Пусть )(FPg , обозначим )(gS множество всех тех сверхслов, конкатена-
ция каждого из которых с 0-префиксом g соответствует модели для F . Такие
сверхслова назовем допустимыми продолжениями 0-префикса g , а k-префиксы
сверхслов из )(gS – допустимыми k-продолжениями g .
Формула F однозначно определяет конечную совокупность множеств
сверхслов },,,{)( 21 mSSSFS [4], такую, что для каждого )(FPg
)()( FSgS и, наоборот, для каждого )(FSSi существует )(FPg , для ко-
торого iSgS )( .
Так -префиксы 21, gg моделей для F эквивалентны, если )()( 21 gSgS .
Пусть mPPP ,...,, 21 – классы эквивалентности -префиксов из )(FP , соответст-
СИНТЕЗ АВТОМАТА, СПЕЦИФИЦИРОВАННОГО В ЯЗІКЕ L*, ПУТЕМ ПЕРЕХОДА…
Комп’ютерні засоби, мережі та системи. 2011, № 10 17
вующие mSSS ,...,, 21 , тогда
m
i
ii FMSP
1
)(
.
Формуле F поставим в соответствие приведенный автомат )(FA , состояния
mqq ,...,1 которого соответствуют классам mPPP ,...,, 21 , а функция переходов
определяется следующим образом. Пусть g – произвольный 0-префикс из iP
и iki ,...,1 – все допустимые 1-продолжения g , тогда ijiji qq ),(
),,1( kj , где ijq таково, что -префикс ijg принадлежит ijP . Для всех
символов алфавита )( , отличных от iki ,...,1 , переход из iq не определен.
Очевидно, что для каждого iq ),...,1( mi существует, по крайней мере, один
символ, для которого значение функции переходов определено и состояние jq ,
из которого имеется переход в iq . Следовательно, автомат )(FA циклический.
Определение 1. Формула F специфицирует автомат А с поведением
),...,,()( 21 nWWWAS тогда и только тогда, когда существует такое разбиение
( nPPP ,,, 21 ) множества )(FP , что )(
1
FMWP
n
i
ii
.
Легко видеть, что любые два -префикса из iP ),...,1( ni эквивалентны.
Доказательство. Допустим противное, т. е. iPgg 21 не эквивалентны. Это
значит, что для одного из этих -префиксов, скажем g2, существует допустимое
продолжение l , не принадлежащее iW (любое сверхслово из iW допустимое
продолжение как для 1g , так и для 2g ) и не принадлежащее )( 1gS . Тогда l
принадлежит некоторому ij WW , но поскольку ji PP , то 2g l , не явля-
ется моделью для F , а значит, и допустимым продолжением для 2g . Таким об-
разом, приходим к противоречию.
Отсюда также следует, что каждое iW ),...,1( ni принадлежит )(FS . Та-
ким образом, все автоматы, специфицируемые формулой F , строго эквивалент-
ны автомату )(FA .
Пусть замкнутые формулы 1F и 2F имеют соответственно сигнатуры 1 и
2 , а – непустое подмножество множества 21 . Формулы 1F и 2F на-
зовем эквивалентными относительно сигнатуры , если множества проекций
всех моделей (двусторонних сверхслов) из )( 1FM и )( 2FM на совпадают.
Переход от языка L
*
к языку L.
Преобразование исходной спецификации в спецификацию в языке L осуще-
ствляется в два этапа. На первом этапе спецификация )(ttFF в языке L* пре-
образуется в такую эквивалентную относительно ее сигнатуры формулу
А.Н. ЧЕБОТАРЕВ, А.К. БОГАЧЕНКО
Комп’ютерні засоби, мережі та системи. 2011, № 10 18
)(11 ttFF в языке L*, которая специфицирует автомат с конечной памятью.
Преобразование )(tF в )(1 tF осуществляется путем введения дополнительных
предикатных символов для предикатов, удовлетворяющих -подформулам ис-
ходной спецификации.
Пусть )(ti максимальная -подформула формулы )(tF , т. е. подформула,
не содержащаяся ни в какой другой -подформуле. Каждая такая -подформула
заменяется атомом вида )( ii rtz , где ir – ранг заменяемой -подформулы, а iz
– предикатный символ, отсутствующий в формуле )(tF , и в спецификацию до-
бавляется эквивалентность )()( iii rttz . Если -формулы в правых частях
эквивалентностей содержат отличные от них -подформулы, то с ними посту-
пают так как и с -подформулами исходной формулы. Они заменяются соответ-
ствующими обозначениями новых предикатов и добавляются эквивалентности
вида )()( ttz jj . Так поступают до тех пор, пока ни одна из -формул )(tj
не будет содержать вхождений -подформул, отличных от нее. В результате бу-
дет получена спецификация )(11 ttFF . Как показано в [7] эта спецификация
эквивалентна исходной спецификации относительно ее сигнатуры и специфици-
рует автомат с конечной памятью. На втором этапе в каждой эквивалентности
)()( iii rttz -формула )( ii rt заменяется правой частью равносиль-
ности (1), где обозначение формулы )1( ii rt заменяется на )1( tzi .
Таким образом, рассматриваемые эквивалентности приобретают вид
))()(&)1(()( tgthtztz iiii , где )(thi и )(tgi -
развертками соответствующих формул )(ti . Это дает спецификацию
)(2 ttfF z в языке L. Второй этап представляет собой неэквивалентное преоб-
разование, поскольку полученная формула 2F языка L имеет дополнительные
по сравнению с формулой 1F модели, а синтезированный по ней автомат может
иметь дополнительные состояния.
Фиктивные состояния.
Каждая модель из )( 2FM , не принадлежащая )( 1FM , имеет 0-префикс, не
принадлежащий )( 1FP [6]. Таким образом, любая модель для 2F , имеющая
0-префикс, принадлежащий )( 1FP , принадлежит )( 1FM . Отсюда следует, что
)()( 21 FSFS , т. е. любой автомат, специфицируемый формулой 2F , имеет по-
давтомат, строго эквивалентный автомату )( 1FA . Все состояния, не принадле-
жащие этому подавтомату, должны быть удалены. Это осуществляется путем
удаления так называемых фиктивных состояний.
Определение 2. Фиктивное состояние автомата, специфицируемого фор-
мулой 2F – это такое состояние, что все представимые им обратные сверхслова
не являются 0-префиксами из )( 1FP .
СИНТЕЗ АВТОМАТА, СПЕЦИФИЦИРОВАННОГО В ЯЗІКЕ L*, ПУТЕМ ПЕРЕХОДА…
Комп’ютерні засоби, мережі та системи. 2011, № 10 19
Несложно убедиться в справедливости следующих утверждений.
Утверждение 1. Если 0-префикс g модели для 2F принадлежит )( 1FP , то
и любое обратное сверхслово gr , где r – допустимое k-продолжение g
)( Nk , также принадлежит )( 1FP .
Утверждение 2. Если 0-префикс g модели для 2F не принадлежит )( 1FP ,
то и все его -префиксы не принадлежат )( 1FP .
Отсюда следует:
1) если состояние не фиктивно, то все достижимые из него состояния также
не фиктивны;
2) если состояние фиктивно, то и все состояния, из которых оно достижимо,
также фиктивны.
Это позволяет при анализе фиктивности состояний ограничиться только со-
стояниями начальных сильно связных подавтоматов (НССП), т. е. таких сильно
связных подавтоматов, состояния которых не достижимы из остальных состоя-
ний автомата. Очевидно, что либо все состояния НССП фиктивны, либо все они
не фиктивны. Если автомат имеет фиктивные состояния, то имеется НССП, все
состояния которого фиктивны. Все фиктивные состояния – это состояния, кото-
рые достижимы только из состояний таких НССП.
Пусть u – модель для формулы F, специфицирующей автомат A с поведени-
ем ),,,( 21 nWWW , которому соответствует разбиение ),,,( 21 nPPP множества
)(FP .
Утверждение 3. 0-префикс двустороннего сверхслова u представим со-
стоянием автомата A.
Доказательство. Пусть u имеет 0-префикс из iP . Для каждого 0k
k-префикс u(–, k) принадлежит некоторому классу из },...,,{ 21 nPPP . Таким
образом, модель u определяет бесконечную последовательность классов из
},...,,{ 21 nPPP , которым принадлежат k-префиксы двустороннего сверхслова
u для всех 0k , а следовательно, и соответствующее обратное сверхслово со-
стояний. Пусть для произвольного 0k lPku ),( , а ),()1,( kuku
и принадлежит mP . Тогда согласно определению специфицируемого автомата
A mqq ),( 1 . Отсюда следует, что 0-префикс )0,(u представим состо-
янием iq .
Пусть 2A – автомат, специфицируемый формулой 2F . Тогда все -пре-
фиксы из )( 2FP представимы состояниями автомата A2 и для всякого состояния
q , которым представим -префикс из )( 1FP , )()( 1FSqW . Если состояния
НССП автомата A2 фиктивны, то удаление их сохраняет наличие в полученном
автомате подавтомата, строго эквивалентного автомату )( 1FA .
А.Н. ЧЕБОТАРЕВ, А.К. БОГАЧЕНКО
Комп’ютерні засоби, мережі та системи. 2011, № 10 20
Рассмотрим способ нахождения фиктивных состояний в автомате 2A .
С каждой формулой вида ))()(&)1(()( tgthtztz iiii в спецификации
2F ассоциируется условие )()()()( tzthtgtc iiii . Пусть в спецификации 2F
имеется k таких эквивалентностей. Как показано в [6] )()( 21 FMFM , причем
все модели для 2F , имеющие -префикс, в каждой позиции которого истинна
одна из формул вида )()()( tzthtg iii , и только такие модели, не являются моде-
лями для 1F .
Утверждение 4. Состояние q НССП фиктивно тогда и только тогда, когда
все представимые им обратные сверхслова удовлетворяют одной и той же фор-
муле ))()(( 111 tcttt i , т. е. во всех позициях таких обратных сверхслов ис-
тинна формула )(tci .
Достаточность непосредственно следует из определения фиктивности со-
стояния. Для доказательства необходимости покажем, что если все обратные
сверхслова, представимые состоянием q не принадлежат )( 1FP , то во всех по-
зициях каждого такого сверхслова истинна одна и та же формула )(tci . Допус-
тим противное, т. е. для каждого )(tci , )(qP содержит обратное сверхслово,
в некоторой позиции которого эта формула ложна. Поскольку q принадлежит
сильно связному подавтомату, то существуют такие слова ir ),,1( ki , пере-
водящие состояние q в себя, что в некоторой позиции слова ir ложна формула
)(tci . Обратное сверхслово )( ki rr , принадлежащее )(qP , не имеет -пре-
фикса, в каждой позиции которого истинна одна из формул )(tci . Таким обра-
зом, оно не принадлежит )(\)( 12 FPFP , т. е. принадлежит )( 1FP . Из этого
следует, что состояние q не фиктивно. Полученное противоречие доказывает
необходимость.
Проверка фиктивности состояний НССП основывается на следующем. Если
формулы )(tci ),,1( ki содержат атомы только ранга 0, то состояния НССП
фиктивны, если отметки всех дуг этого НССП имплицируют одну и ту же
формулу )(tci . Если )(tci имеет вид )(&&)( 0 tcstc iis , где формула
)( jtc ji построена из атомов ранга j , то она преобразуется в формулу
)(&&)()( 0 tctctc iisi . Действительно, такая формула )(tci может быть ис-
тинна во всех позициях обратного сверхслова только в том случае, если )(tci
истинна во всех его позициях. Будем говорить, что формула ))()(( 111 tcttt i
выполняется на НССП, если отметки всех его дуг имплицируют формулу )(tci .
Таким образом, проверка фиктивности состояний НССП состоит в проверке
выполнимости на нем каждой из формул )(tci ),,1( ki . Фиктивные состоя-
ния удаляются из автомата. При удалении состояний какого-либо из НССП
СИНТЕЗ АВТОМАТА, СПЕЦИФИЦИРОВАННОГО В ЯЗІКЕ L*, ПУТЕМ ПЕРЕХОДА…
Комп’ютерні засоби, мережі та системи. 2011, № 10 21
и всех состояний, не принадлежащих циклическому подавтомату, могут поя-
виться новые НССП, для которых выполняется аналогичная проверка. В резуль-
тате удаления всех фиктивных состояний будет получен автомат, строго эквива-
лентный автомату )( 1FA . Если будут удалены все состояния, то исходная спе-
цификация F противоречива.
Выводы. Предложенный метод анализа фиктивности состояний и основан-
ный на нем метод синтеза автомата, специфицированного в языке L* , сущест-
венно проще метода, рассмотренного в [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.
Получено 01.09.2011
|
| id | nasplib_isofts_kiev_ua-123456789-46448 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 1817-9908 |
| language | Russian |
| last_indexed | 2025-11-28T03:02:56Z |
| publishDate | 2011 |
| publisher | Інститут кібернетики ім. В.М. Глушкова НАН України |
| record_format | dspace |
| spelling | Чеботарев, А.Н. Богаченко, А.К. 2013-06-30T06:34:32Z 2013-06-30T06:34:32Z 2011 Синтез автомата, специфицированного в языке L*, путем перехода к спецификации в языке L / А.Н. Чеботарев, А.К. Богаченко // Комп’ютерні засоби, мережі та системи. — 2011. — № 10. — С. 13-21. — Бібліогр.: 7 назв. — рос. 1817-9908 https://nasplib.isofts.kiev.ua/handle/123456789/46448 519.713.1 Рассматривается метод синтеза конечного автомата, специфицированного в логическом языке L*. Метод основан на трансляции спецификации в язык L и синтезе автомата по спецификации в этом языке. Розглядається метод синтезу скінченного автомата, специфікованого логічною мовою 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 language L and synthesizing an FSM from the specification in this language. ru Інститут кібернетики ім. В.М. Глушкова НАН України Комп’ютерні засоби, мережі та системи Синтез автомата, специфицированного в языке L*, путем перехода к спецификации в языке L Synthesis of an FSM specified in the language L* by passing to the specification in the language L Article published earlier |
| spellingShingle | Синтез автомата, специфицированного в языке L*, путем перехода к спецификации в языке L Чеботарев, А.Н. Богаченко, А.К. |
| title | Синтез автомата, специфицированного в языке L*, путем перехода к спецификации в языке L |
| title_alt | Synthesis of an FSM specified in the language L* by passing to the specification in the language L |
| title_full | Синтез автомата, специфицированного в языке L*, путем перехода к спецификации в языке L |
| title_fullStr | Синтез автомата, специфицированного в языке L*, путем перехода к спецификации в языке L |
| title_full_unstemmed | Синтез автомата, специфицированного в языке L*, путем перехода к спецификации в языке L |
| title_short | Синтез автомата, специфицированного в языке L*, путем перехода к спецификации в языке L |
| title_sort | синтез автомата, специфицированного в языке l*, путем перехода к спецификации в языке l |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/46448 |
| work_keys_str_mv | AT čebotarevan sintezavtomataspecificirovannogovâzykelputemperehodakspecifikaciivâzykel AT bogačenkoak sintezavtomataspecificirovannogovâzykelputemperehodakspecifikaciivâzykel AT čebotarevan synthesisofanfsmspecifiedinthelanguagelbypassingtothespecificationinthelanguagel AT bogačenkoak synthesisofanfsmspecifiedinthelanguagelbypassingtothespecificationinthelanguagel |