Synthesis of an automaton specified by the set of clauses
An approach to synthesis of an automaton specified by the logical formula in the conjunctive normal form (c.n.f.) is proposed. Although this approach exploits the method for synthesis of an automaton from the specification represented in the disjunctive normal form (d.n.f.), the synthesis is carried...
Gespeichert in:
| Datum: | 2015 |
|---|---|
| 1. Verfasser: | |
| Format: | Artikel |
| Sprache: | Ukrainian |
| Veröffentlicht: |
PROBLEMS IN PROGRAMMING
2015
|
| Schlagworte: | |
| Online Zugang: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/12 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| Назва журналу: | Problems in programming |
| Завантажити файл: |  |
Institution
Problems in programming| id |
pp_isofts_kiev_ua-article-12 |
|---|---|
| record_format |
ojs |
| resource_txt_mv |
ppisoftskievua/d1/e35d8da4ffccfb32c2a21c8f4ecfc7d1.pdf |
| spelling |
pp_isofts_kiev_ua-article-122018-10-02T13:53:04Z Synthesis of an automaton specified by the set of clauses Синтез автомата, специфицированного множеством дизъюнктов Синтез автомата, специфікованого множиною диз’юнктів Chebotarev, A.N. An approach to synthesis of an automaton specified by the logical formula in the conjunctive normal form (c.n.f.) is proposed. Although this approach exploits the method for synthesis of an automaton from the specification represented in the disjunctive normal form (d.n.f.), the synthesis is carried out without transforming c.n.f. into d.n.f. Owing to this fact the proposed method has the same efficiency as the method at which it is based. Предложен подход к синтезу автомата, специфицированного логической формулой в конъюнктивной нормальной форме (к.н.ф.). Хотя при этом используется метод синтеза автомата по формуле, представленной в дизъюнктивной нормальной форме (д.н.ф.), при синтезе не требуется преобразование к.н.ф. в д.н.ф. Благодаря этому предложенный метод имеет ту же эффективность, что и метод, на котором он основан. Запропоновано підхід до синтезу автомата, який специфіковано логічною формулою у кон’юнктивній нормальній формі (к.н.ф.). Хоча при цьому використовується метод синтезу автомата за специфікацією, яку подано у диз’юнктивній нормальній формі (д.н.ф.), синтез виконується без перетворення к.н.ф. у д.н.ф. Завдяки цьому запропонований метод має ту ж саму ефективність, що й метод, на якому він базується. PROBLEMS IN PROGRAMMING ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ ПРОБЛЕМИ ПРОГРАМУВАННЯ 2015-07-01 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/12 PROBLEMS IN PROGRAMMING; No 2 (2003) ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 2 (2003) ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 2 (2003) 1727-4907 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/12/17 Copyright (c) 2015 ПРОБЛЕМИ ПРОГРАМУВАННЯ |
| institution |
Problems in programming |
| baseUrl_str |
https://pp.isofts.kiev.ua/index.php/ojs1/oai |
| datestamp_date |
2018-10-02T13:53:04Z |
| collection |
OJS |
| language |
Ukrainian |
| topic |
|
| spellingShingle |
Chebotarev, A.N. Synthesis of an automaton specified by the set of clauses |
| topic_facet |
|
| format |
Article |
| author |
Chebotarev, A.N. |
| author_facet |
Chebotarev, A.N. |
| author_sort |
Chebotarev, A.N. |
| title |
Synthesis of an automaton specified by the set of clauses |
| title_short |
Synthesis of an automaton specified by the set of clauses |
| title_full |
Synthesis of an automaton specified by the set of clauses |
| title_fullStr |
Synthesis of an automaton specified by the set of clauses |
| title_full_unstemmed |
Synthesis of an automaton specified by the set of clauses |
| title_sort |
synthesis of an automaton specified by the set of clauses |
| title_alt |
Синтез автомата, специфицированного множеством дизъюнктов Синтез автомата, специфікованого множиною диз’юнктів |
| description |
An approach to synthesis of an automaton specified by the logical formula in the conjunctive normal form (c.n.f.) is proposed. Although this approach exploits the method for synthesis of an automaton from the specification represented in the disjunctive normal form (d.n.f.), the synthesis is carried out without transforming c.n.f. into d.n.f. Owing to this fact the proposed method has the same efficiency as the method at which it is based. |
| publisher |
PROBLEMS IN PROGRAMMING |
| publishDate |
2015 |
| url |
https://pp.isofts.kiev.ua/index.php/ojs1/article/view/12 |
| work_keys_str_mv |
AT chebotarevan synthesisofanautomatonspecifiedbythesetofclauses AT chebotarevan sintezavtomataspecificirovannogomnožestvomdizʺûnktov AT chebotarevan sintezavtomataspecifíkovanogomnožinoûdizûnktív |
| first_indexed |
2025-07-17T09:48:44Z |
| last_indexed |
2025-07-17T09:48:44Z |
| _version_ |
1850410474894524416 |
| fulltext |
Формальные методы программирования
© А.Н. Чеботарев, 2003
58 ISSN 1727-4907. Проблемы программирования. 2003. № 2
УДК 519.713.1
А.Н. Чеботарев
СИНТЕЗ АВТОМАТА, СПЕЦИФИЦИРОВАННОГО
МНОЖЕСТВОМ ДИЗЪЮНКТОВ
Предложен подход к синтезу автомата, специфицированного логической фор-
мулой в конъюнктивной нормальной форме (к.н.ф.). Хотя при этом используется
метод синтеза автомата по формуле, представленной в дизъюнктивной нормальной
форме (д.н.ф.), при синтезе не требуется преобразование к.н.ф. в д.н.ф. Благодаря
этому предложенный метод имеет ту же эффективность, что и метод, на котором он
основан.
Введение
При проектировании алгоритма
исходя из декларативной специфика-
ции функциональных требований к
нему центральной задачей перехода от
декларативного представления к импе-
ративному (процедурному) является
построение управляющей части алго-
ритма, например, в виде конечно-
автоматной модели. Рассматриваемая
здесь задача синтеза конечного авто-
мата представляет собой один из эта-
пов проектирования реактивного алго-
ритма, требования к которому заданы
в языке логики предикатов первого
порядка. Под реактивным алгоритмом
понимается алгоритм функционирова-
ния системы, постоянно взаимодейст-
вующей со своим окружением; его на-
значение – выработка реакций на из-
меняющиеся воздействия среды. Су-
щественным параметром описания
функциональных требований к такому
алгоритму является дискретное время,
в качестве которого выступает множе-
ство целых чисел. Предполагается, что
спецификация алгоритма состоит из
двух частей: спецификаций операцион-
ной и управляющей частей алгоритма.
Последняя служит исходной информа-
цией для синтеза процедурного (авто-
матного) представления управляющей
части алгоритма и представляет собой
формулу вида ∀tF(t), где F(t) – не со-
держащая кванторов формула языка
первого порядка с одной переменной t
и одноместными предикатами.
В основе рассматриваемого ме-
тода синтеза лежит представление
формулы F(t) в так называемой нор-
мальной форме. Построение нормаль-
ной формы описано в [1, 2] для случая,
когда F(t) задана в виде дизъюнктив-
ной нормальной формы (д.н.ф.). Син-
тез автомата, т.е. переход от деклара-
тивной спецификации к его процедур-
ному представлению, осуществляется
на заключительном этапе проектиро-
вания управляющей части алгоритма.
На всех предыдущих этапах, таких, как
проверка непротиворечивости специ-
фикации [3], проверка ее согласован-
ности со спецификацией среды [4], де-
терминизация автомата [5], использу-
ется представление F(t) в виде конъ-
юнктивной нормальной формы (мно-
жества дизъюнктов). Поэтому, чтобы
воспользоваться методами синтеза
[1, 2], необходимо к.н.ф. формулы F(t)
преобразовать в д.н.ф. При реализации
методики проектирования на ЭВМ та-
кое преобразование требует значи-
тельных ресурсов памяти, что сущест-
венно ухудшает характеристики реали-
зации и ограничивает размерность
спецификации, для которой возможен
автоматический синтез. Поэтому жела-
тельно иметь такой метод синтеза, ко-
торый бы не требовал преобразования
формулы F(t) из к.н.ф. в д.н.ф.
Основная идея предлагаемого
подхода состоит в том, чтобы сначала
построить нормальную форму для фор-
мулы ¬F(t), дизъюнктивное представле-
ние которой тривиальным образом по-
лучается из конъюнктивного представ-
ления формулы F(t), а затем преобразо-
вать ее в нормальную форму формулы
F(t). Как будет показано ниже, это пре-
образование также осуществляется дос-
Формальные методы программирования
59
таточно просто. При этом построение
нормальной формы формулы ¬F(t)
можно осуществлять не до конца, а на
некотором промежуточном этапе пе-
рейти к дизъюнктивному представле-
нию формулы F(t) и для него продол-
жить построение нормальной формы.
Такой подход позволяет, с одной сторо-
ны, исключить необходимость преобра-
зования конъюнктивного представле-
ния формулы F(t) в дизъюнктивное и, с
другой стороны, использовать имею-
щиеся реализации методов синтеза,
рассчитанных на дизъюнктивное пред-
ставление формулы F(t).
Язык спецификации автоматов и
проблема синтеза
Напомним основные понятия,
связанные со специфицируемыми ав-
томатами и языком, используемым для
их спецификации.
Определение 1. Конечный де-
терминированный Σ-автомат A опреде-
ляется как A = <Σ, Q, δ>, где Σ – конеч-
ный входной алфавит автомата; Q –
конечное множество его состояний; δ:
Q×Σ → Q – частичная функция пере-
ходов.
Определение 2. Σ-автомат A =
= <Σ, Q, δ> называется циклическим, ес-
ли для каждого q ∈ Q существуют такие
σ1, σ2 ∈ Σ и q1, q2 ∈ Q, что q = δ(q1, σ1) и
q2 = δ(q, σ2).
В качестве языка спецификации
используется следующее подмножество
языка первого порядка с одноместны-
ми предикатами, интерпретируемыми
на множестве целых чисел. Пусть
Ω = {p1, …, pm} – множество одномест-
ных предикатных символов, а Φ –
класс формул, построенных с помо-
щью логических связок из атомов вида
p(t + k), где p ∈ Ω; t – переменная, при-
нимающая значения из множества це-
лых чисел; k – целочисленная кон-
станта, называемая рангом атома, а
+ – операция сложения целых чисел.
Формулы языка, используемые в каче-
стве спецификации Σ-автомата (точнее,
класса эквивалентных Σ-автоматов),
имеют вид ∀tF(t), где F(t) ∈ Φ. Как по-
казано в [3], в таких спецификациях
достаточно ограничиться рассмотрени-
ем формул, у которых максимальный
ранг атомов равен 0. В дальнейшем
предполагается, что формула F(t) в
спецификации S = ∀tF(t) удовлетворяет
этому ограничению. Примером специ-
фикации Σ-автомата может служить
формула ∀t((u(t – 1) ∨ ¬w(t – 1)) & ¬w(t) ∨
∨ ¬w(t – 1) & u(t)), где u и w – предикат-
ные символы. Глубиной формулы назы-
вается разность между максимальным
и минимальным рангами входящих в
нее атомов. Таким образом, глубина
приведенной формулы равна 1.
Семантика формулы ∀tF(t), т.е.
описание класса автоматов, задаваемых
этой формулой, определена в [1]. Заме-
тим, что входной алфавит Σ этих авто-
матов представляет собой множество
всех двоичных векторов длиной m, где
m – количество предикатных симво-
лов, встречающихся в формуле F(t).
Рассматривая атомы нулевого ранга,
т.е. вида p(t), как пропозициональные
переменные, произвольное множество
входных символов специфицируемого
автомата зададим формулой f(t) = f(p1(t),
…, pm(t)), а именно f(t) задает множест-
во всех тех двоичных векторов, на ко-
торых она истинна.
Примем следующее соглашение,
касающееся обозначения формул.
Пусть F(t) ∈ Φ, для произвольного цело-
го k F(t + k) обозначает формулу, полу-
ченную из F(t) путем добавления k к
рангам всех ее атомов (сдвиг на k).
В основе методики синтеза авто-
мата, специфицированного формулой
∀tF(t), лежит представление F(t) в так
называемой нормальной форме. Пусть
F(t) представлена в виде
∨
=
n
i 1
Fi(t – 1) & fi(t), (1)
где Fi(t – 1) – формула, максимальный
ранг атомов в которой не превышает
−1, а fi(t) – формула, построенная из
атомов ранга 0. Представление F(t) в
Формальные методы программирования
60
таком виде будем называть дизъюнк-
тивным, а конъюнкцию вида Fi(t – 1) &
& fi(t) – компонентой такого представ-
ления с левой частью Fi(t – 1) и правой
– fi(t). Дизъюнктивное представление
удовлетворяет условию ортогонально-
сти, если для i ≠ j (i, j ∈ {1, …, n}) Fi(t – 1) &
& Fj(t – 1) ≡ 0. Дизъюнктивное представ-
ление формулы F(t), удовлетворяющее
условию ортогональности, называется
нормальной формой, если для любых
i, j = 1, …, n конъюнкция Fi(t – 1) & fi(t) &
& Fj(t) либо тождественно равна нулю,
либо равна Fi(t – 1) & fij(t), где fij(t) не
равная тождественно нулю формула,
все атомы которой имеют ранг 0.
Нормальная форма формулы F(t)
в приведенном выше примере специ-
фикации имеет вид u(t – 1) & w(t – 1) &
& ¬w(t) ∨ ¬w(t – 1) & (u(t) ∨ ¬w(t)). Здесь
F1(t – 1) = u(t – 1) & w(t – 1), а F2(t – 1) =
= ¬w(t – 1). Нетрудно заметить, что для
формул глубины 1 любое дизъюнктив-
ное представление, удовлетворяющее
условию ортогональности, есть нор-
мальная форма, что существенно уп-
рощает процедуру синтеза для таких
формул.
Пусть для формулы F(t) в специ-
фикации S получена нормальная форма
вида (1). Σ-автомат A(S), удовлетворяю-
щий спецификации S, представляет со-
бой максимальный циклический подав-
томат автомата A′(S), состояния которо-
го q1, …, qn соответствуют формулам
F1(t−1), …, Fn(t – 1) и из состояния qi
имеется переход в состояние qj тогда и
только тогда, когда Fi(t – 1) & fi(t) & Fj(t) =
= Fi(t – 1) & fij(t), где fij(t) – не равна то-
ждественно нулю. При этом множест-
во входных символов, вызывающих
переход из qi в qj, задается формулой
fij(t). Таким образом, синтез автомата по
спецификации ∀tF(t) сводится к постро-
ению нормальной формы формулы F(t).
Построение нормальной формы
формулы F(t) по ее д.н.ф.
Построение нормальной формы
формулы F(t) по ее д.н.ф. состоит из
двух основных этапов: 1) построения
дизъюнктивного представления фор-
мулы F(t), удовлетворяющего условию
ортогональности, и 2) расщепления
компонент полученного дизъюнктивно-
го представления.
На первом этапе требуемое
представление получается путем по-
следовательного применения к парам
компонент дизъюнктивного представ-
ления следующего соотношения:
Fi(t – 1) & fi(t) ∨ Fj(t – 1) & fj(t) ⇔
⇔ Fi(t – 1) & ¬Fj(t – 1) & fi(t) ∨ ¬Fi(t – 1) &
& Fj(t – 1) & fj(t) ∨ Fi(t – 1) & Fj(t – 1) &
& (fi(t) ∨ fj(t)). (2)
В качестве иллюстрации такого
способа построения дизъюнктивного
представления, удовлетворяющего усло-
вию ортогональности, проделаем соот-
ветствующие преобразования для фор-
мулы F(t) = u(t – 1) & ¬w(t) ∨ ¬w(t – 1) &
& u(t) ∨ ¬w(t – 1) & ¬w(t). Здесь и ниже в
формулах подчеркнуты те компоненты,
к которым на очередном шаге приме-
няется соотношение (2). После первого
применения соотношения получим
u(t – 1) & w(t – 1) & ¬w(t) ∨ ¬u(t – 1) &
& ¬w(t – 1) & u(t) ∨ u(t – 1) & ¬w(t – 1) &
& (¬w(t) ∨ u(t)) ∨ ¬w(t – 1) & ¬w(t).
После следующего применения
будем иметь
u(t – 1)&w(t – 1)&¬w(t) ∨ u(t – 1) & ¬w(t – 1) &
& ¬w(t) ∨ ¬u(t – 1) & ¬w(t – 1) & (u(t) ∨
∨ ¬w(t)) ∨ u(t – 1) & ¬w(t – 1) & (¬w(t) ∨ u(t)).
Подчеркнутые компоненты все
еще не удовлетворяют условию орто-
гональности. Применение к ним соот-
ношения (2) дает представление
u(t – 1) & w(t – 1) & ¬w(t) ∨ u(t – 1) &
& ¬w(t – 1) & (¬w(t) ∨ u(t)) ∨¬u(t – 1) &
&¬w(t – 1) & (u(t) ∨ ¬w(t)),
удовлетворяющее требуемому условию.
На втором этапе для получения
нормальной формы формулы F(t) осу-
ществляется расщепление компонент
ее дизъюнктивного представления пу-
Формальные методы программирования
61
тем умножения их на ∨
=
n
i 1
Fi(t). Эквива-
лентность такого преобразования фор-
мулы F(t) показана в [6]. При этом ка-
ждая формула Fi(t − 1) & fi(t) (i = 1, …, n)
умножается на каждую Fj(t) (j = 1, …, n) и
дизъюнкция всех таких произведений
приводится к виду, удовлетворяющему
условию ортогональности. Поясним
сказанное на примере. Пусть дизъ-
юнктивное представление формулы
F(t) имеет вид ¬u(t – 2) & x(t – 1) & (u(t) ∨
∨ (t)) ∨ (u(t – 2) ∨ ¬x(t – 1)) & 1. Здесь фор-
мулы F1(t) и F2(t) равны соответствен-
но ¬u(t – 1) & x(t) и u(t – 1) ∨ ¬x(t). Осу-
ществим расщепление левой компо-
ненты.
¬u(t – 2) & x(t – 1) & (u(t) ∨ x(t)) & F1(t) =
= ¬u(t – 2) & x(t – 1) & (u(t) ∨ x(t)) &
& ¬u(t – 1) & x(t) = ¬u(t – 2) & ¬u(t – 1) &
& x(t – 1) & x(t).
¬u(t – 2) & x(t – 1) & (u(t) ∨ x(t)) & F2(t) =
= ¬u(t – 2) & x(t – 1) & (u(t) ∨ x(t)) &
& (u(t – 1) ∨ ¬x(t)) = ¬u(t – 2) & u(t – 1) &
& x(t – 1) & (u(t) ∨ x(t)) ∨ ¬u(t – 2) &
& x(t – 1) & u(t)&¬x(t).
Теперь формулу ¬u(t – 2) & ¬u(t –
– 1) & x(t – 1) & x(t) ∨ ¬u(t – 2) & u(t – 1) &
& x(t – 1) & (u(t) ∨ x(t)) ∨ ¬u(t – 2) & x(t – 1) &
& u(t) & ¬x(t) необходимо привести к ви-
ду, удовлетворяющему условию орто-
гональности. В результате получим:
¬u(t – 2) & u(t – 1) & x(t – 1) & (u(t) ∨ x(t)) ∨
∨ ¬u(t–2) & ¬u(t–1) & x(t – 1) & (u(t) ∨ x(t)),
что и представляет собой результат
расщепления.
Расщепления компоненты Fi(t−1) &
& fi(t) не происходит, если в получен-
ном дизъюнктивном представлении ее
произведения на ∨
=
n
i 1
Fi(t) все компонен-
ты имеют левую часть Fi(t − 1). Процесс
расщепления продолжается до тех пор,
пока на очередном шаге ни одна из
компонент не будет расщеплена. Не-
трудно показать, что количество после-
довательных расщеплений дизъюнк-
тивного представления формулы F(t)
ограничено сверху значением ее глу-
бины.
Построение нормальной формы
формулы F(t) по ее к.н.ф.
Построение нормальной формы
формулы F(t), заданной множеством
дизъюнктов (каждый дизъюнкт пред-
ставляет собой дизъюнкцию атомов
или их отрицаний), может быть осу-
ществлено следующим образом. Сна-
чала множество дизъюнктов превра-
щается в соответствующее ему мно-
жество конъюнктов отрицания фор-
мулы F(t). Таким образом получается
дизъюнктивное представление форму-
лы ¬F(t). Затем строится эквивалент-
ное ему дизъюнктивное представление,
удовлетворяющее условию ортогональ-
ности, которое снова инвертируется с
целью получения дизъюнктивного
представления исходной формулы F(t).
Для этого используется следующее
свойство дизъюнктивных представле-
ний пропозициональных формул с раз-
деленными переменными.
Пусть множество всех перемен-
ных, встречающихся в пропозицио-
нальной формуле f, разбито на два
подмножества: x1, ..., xm и y1, ..., yn.
Определение 3. f(x1, ..., xm, y1, ..., yn)
называется формулой с разделенными
переменными, если она имеет вид
∨
=
k
i 1
if ′ (x1, ..., xm) & if ′′ (y1, ..., yn). (3)
Утверждение 1. Если для форму-
лы f вида (3) выполняются следующие
условия:
а) ∨
=
k
i 1
if ′ (x1, ..., xm) ≡ 1;
б) для любых i ≠ j (i, j = 1, ..., k)
if ′ (x1, ..., xm) & jf ′ (x1, ..., xm) ≡ 0,
то ¬f эквивалентна формуле
∨
=
k
i 1
if ′ (x1, ..., xm) & (¬ if ′′ (y1, ..., yn)). (4)
Формальные методы программирования
62
Доказательство. Пусть σ = <α1, ...,
αm, β1, ..., βn> – набор значений соот-
ветственно переменных x1, ..., xm, y1, ..., yn.
Пусть формула (3) на этом наборе при-
нимает значение 1. Тогда найдется та-
кое i, что if ′ (α1, ..., αm) = if ′′ (β1, ..., βn) = 1.
В силу б) для всех j ≠ i jf ′ (α1, ..., αm) = 0.
Отсюда следует, что формула (4) на
наборе σ принимает значение 0. Пусть
теперь формула (3) на наборе σ при-
нимает значение 0. В силу а) найдется
такое i, что if ′ (α1, ..., αm) = 1, но по-
скольку значение формулы равно ну-
лю, то if ′′ (β1, ..., βn) = 0. Отсюда следует,
что формула (4) на наборе σ принимает
значение 1. Конец доказательства.
Таким образом, если дизъюнк-
тивное представление формулы F(t)
удовлетворяет условиям утверждения
1, то, чтобы его проинвертировать,
достаточно проинвертировать правую
часть каждой из его компонент. Оче-
видно, что в результате будет получено
дизъюнктивное представление форму-
лы F(t), удовлетворяющее условию ор-
тогональности. Теперь построение
нормальной формы формулы F(t) мо-
жет быть продолжено описанным вы-
ше методом расщепления компонент.
Полученное на промежуточном
этапе дизъюнктивное представление
формулы F(t), удовлетворяющее усло-
вию ортогональности, может не удов-
летворять условию а) утверждения 1, в
этом случае требуемое представление
получается в результате добавления
компоненты ¬(∨
−
n
i 1
Fi(t − 1)) & 0.
Пример синтеза автомата
Пусть формула F(t) в специфика-
ции автомата задана следующим мно-
жеством дизъюнктов.
(¬u(t – 1) ∨ ¬w(t – 1) ∨ ¬u(t) ∨ w(t)).
(¬w(t – 2) ∨ u(t – 1) ∨ ¬w(t – 1) ∨ u(t)).
(w(t – 1) ∨ ¬u(t) ∨ ¬w(t)).
(w(t – 1) ∨ u(t) ∨ w(t)).
(¬w(t – 2) ∨ u(t – 1) ∨ ¬w(t – 1) ∨ ¬w(t)).
(¬u(t – 2) ∨ ¬w(t – 1) ∨ u(t – 1) ∨ ¬w(t)).
(¬u(t – 2) ∨ ¬w(t – 1) ∨ u(t – 1) ∨ u(t)).
(w(t – 2) ∨ u(t – 2) ∨ ¬w(t – 1) ∨ ¬u(t) ∨ w(t)).
Соответствующее множество
конъюнктов, составляющих д.н.ф. фор-
мулы ¬F(t), имеет такой вид:
u(t – 1)w(t – 1) & u(t)¬w(t).
w(t – 2)¬u(t – 1)w(t – 1) & ¬u(t).
¬w(t – 1) & u(t)w(t).
¬w(t – 1) & ¬u(t)¬w(t).
w(t – 2)¬u(t – 1)w(t – 1) & w(t).
u(t – 2)w(t – 1)¬u(t – 1) & w(t).
u(t – 2)w(t – 1)¬u(t – 1) & ¬u(t).
¬w(t – 2)¬u(t – 2)w(t – 1) & u(t)¬w(t).
Здесь, для удобства, все знаки
конъюнкций, кроме конъюнкций, со-
единяющих левую и правую части
компонент (конъюнктов), опущены.
Прежде чем применять соотношение
(2), вынесем за скобки одинаковые ле-
вые части компонент. В результате
получим
u(t – 1)w(t – 1) & u(t)¬w(t).
w(t – 2)¬u(t – 1)w(t – 1) & (¬u(t) ∨ w(t)).
¬w(t – 1) & (u(t)w(t) ∨ ¬u(t)¬w(t)).
u(t – 2)w(t – 1)¬u(t – 1) & (¬u(t) ∨ w(t)).
¬w(t – 2)¬u(t – 2)w(t – 1) & u(t)¬w(t).
Вообще говоря, это преобразова-
ние может быть получено и путем
применения соотношения (2), однако
удобнее использовать вынесение за
скобки. Теперь вынесем за скобки
одинаковые правые части компонент.
Это преобразование направлено на по-
лучение автомата с минимальным ко-
личеством состояний, поэтому перед
началом расщепления компонент сле-
дует иметь дизъюнктивное представле-
ние, никакие две компоненты которого
не имеют одинаковых (эквивалентных)
левых частей. После выполнения этого
преобразования получим следующее
дизъюнктивное представление форму-
лы ¬F(t):
(w(t – 2) ∨ u(t – 2))¬u(t – 1)w(t–1) & (¬u(t) ∨
∨ w(t)) ∨ (¬u(t – 2)¬w(t – 2) ∨ u(t − 1))w(t – 1) &
& u(t)¬w(t) ∨ ¬w(t – 1) & (u(t)w(t) ∨ ¬u(t)¬w(t)).
Формальные методы программирования
63
Это представление удовлетворяет
обоим условиям утверждения 1, поэто-
му от него можно сразу перейти к со-
ответствующему дизъюнктивному пред-
ставлению формулы F(t), которое вы-
глядит следующим образом:
(w(t – 2) ∨ u(t – 2))¬u(t – 1)w(t – 1) & u(t)¬w(t) ∨
∨ (¬u(t – 2)¬w(t – 2) ∨ u(t − 1))w(t –1) & (¬u(t) ∨
w(t)) ∨ ¬w(t – 1) & (¬u(t)w(t) ∨ u(t)¬w(t)).
Здесь F1(t) = (u(t − 1) ∨ w(t − 1))¬u(t)w(t),
F2(t) = (¬u(t − 1)¬w(t − 1) ∨ u(t))w(t), F3(t) =
= ¬w(t).
Теперь можно приступить к
расщеплению компонент.
Расщепление компоненты F1(t − 1) &
& f1(t):
F1(t − 1)u(t)¬w(t) & F1(t) ≡ 0;
F1(t − 1)u(t)¬w(t) & F2(t) ≡ 0;
F1(t − 1)u(t)¬w(t) & F3(t) = F1(t − 1)u(t)¬w(t).
Таким образом, расщепления
первой компоненты не произошло.
Расщепление компоненты F2(t − 1) &
& f2(t):
F2(t − 1)(¬u(t) ∨ w(t)) & F1(t) =
= F2(t − 1)¬u(t)w(t);
F2(t − 1)(¬u(t) ∨ w(t)) & F2(t) =
= F2(t − 1)u(t)w(t);
F2(t − 1)(¬u(t) ∨ w(t))&F3(t) =
= F2(t − 1)¬u(t)¬w(t).
Вторая компонента также не рас-
щепилась.
Расщепление компоненты F3(t − 1) &
& f3(t):
F3(t − 1)(u(t)¬w(t) ∨ ¬u(t)w(t)) & F1(t) =
= u(t−1)¬w(t−1)¬u(t)w(t);
F3(t − 1)(u(t)¬w(t) ∨ ¬u(t)w(t)) & F2(t) =
¬u(t − 1)¬w(t − 1)¬u(t)w(t);
F3(t − 1)(u(t)¬w(t) ∨ ¬u(t)w(t)) & F3(t) =
= ¬w(t−1)u(t)¬w(t).
Значения новых компонент будут
получены после того, как формула
u(t − 1)¬w(t − 1)¬u(t)w(t) ∨ ¬u(t − 1)¬w(t − 1)
¬u(t)w(t) ∨ ¬w(t − 1)u(t)¬w(t) будет пред-
ставлена в виде, удовлетворяющем ус-
ловию ортогональности. Соответствую-
щее представление имеет вид
u(t − 1)¬w(t − 1)(¬u(t)w(t) ∨ u(t)¬w(t)) ∨
∨ ¬u(t − 1)¬w(t − 1)(¬u(t)w(t) ∨ u(t)¬w(t)) =
= F31(t − 1)(¬u(t)w(t) ∨ u(t)¬w(t)) ∨
∨ F32(t − 1)(¬u(t)w(t) ∨ u(t)¬w(t)).
Таким образом, F31(t) = u(t)¬w(t), а
F32(t) = ¬u(t)¬w(t).
Второй цикл расщеплений.
Расщепление компоненты F1(t − 1) &
& f1(t):
F1(t − 1)u(t)¬w(t) & F31(t) = F1(t − 1)u(t)¬w(t);
F1(t − 1)u(t)¬w(t) & F32(t) ≡ 0.
И на этот раз первая компонента
не расщепилась.
Расщепление компоненты F2(t − 1) &
& f2(t):
F2(t − 1)(¬u(t) ∨ w(t)) & F31(t) ≡ 0;
F2(t − 1)(¬u(t) ∨ w(t)) & F32(t) =
= F2(t−1)¬u(t)¬w(t).
Вторая компонента также не
расщепилась.
Расщепление компоненты F31(t −
– 1)(¬u(t)w(t) ∨ u(t)¬w(t)):
F31(t − 1)(¬u(t)w(t) ∨ u(t)¬w(t)) & F1(t) =
= F31(t−1)¬u(t)w(t);
F31(t − 1)(¬u(t)w(t) ∨ u(t)¬w(t)) & F2(t) ≡ 0;
F31(t − 1)(¬u(t)w(t) ∨ u(t)¬w(t)) & F31(t) =
= F31(t−1)u(t)¬w(t);
F31(t − 1)(¬u(t)w(t) ∨ u(t)¬w(t)) & F32(t) ≡ 0.
Расщепление компоненты F32(t −
– 1)(¬u(t)w(t) ∨ u(t)¬w(t)):
F32(t − 1)(¬u(t)w(t) ∨ u(t)¬w(t)) & F1(t) ≡ 0;
F32(t − 1)(¬u(t)w(t) ∨ u(t)¬w(t)) & F2(t) =
= F32(t − 1)¬u(t)w(t);
F32(t − 1)(¬u(t)w(t) ∨ u(t)¬w(t)) & F31(t) =
= F32(t−1)u(t)¬w(t);
F32(t − 1)(¬u(t)w(t) ∨ u(t)¬w(t)) & F32(t) ≡ 0.
Поскольку на втором цикле рас-
щеплений ни одна из имеющихся ком-
понент не расщепилась, процесс рас-
щепления заканчивается. Таким обра-
зом, получена нормальная форма фор-
мулы F(t), определяющая автомат A′(S)
для спецификации S = ∀tF(t). Так как
этот автомат циклический, то он сов-
Формальные методы программирования
64
падает с автоматом A(S), который при-
веден на рисунке.
Заключение
В статье предложен подход к
синтезу автомата, специфицированного
множеством дизъюнктов. При этом
используется разработанный ранее и
программно реализованный метод син-
теза автомата, в спецификации которо-
го формула F(t) представлена в д.н.ф.
По сравнению с синтезом по д.н.ф. до-
полнительные вычислительные затраты
предложенного метода связаны с ин-
вертированием правых частей компо-
нент некоторого дизъюнктивного пред-
ставления формулы ¬F(t). Поскольку
формулы в правых частях компонент,
как правило, простые и зависят от не-
большого количества переменных, то
эти вычислительные затраты сущест-
венно меньше затрат на перевод фор-
мулы спецификации из к.н.ф. в д.н.ф.
Особенностью рассмотренного
метода построения нормальной формы
формулы F(t) является то, что при рас-
щеплении компонент некоторые фор-
мулы необходимо сравнивать на логи-
ческую эквивалентность. Это срав-
нение может быть заменено сравнени-
ем формул на их идентичность, если
перед каждым таким сравнением вы-
полнять их эквивалентные преобразо-
вания, использующие операции склеи-
вания и поглощения элементарных
конъюнкций. Аналогичные оптимиза-
ционные преобразования следует так-
же выполнять при приведении форму-
лы к виду, удовлетворяющему условию
ортогональности.
1. Чеботарев А.Н. Синтез недетерминирован-
ного автомата по его логической специфи-
кации. I // Кибернетика и системный ана-
лиз. – 1995. – N 5. – C. 3—15.
2. Чеботарев А.Н. Синтез недетерминирован-
ного автомата по его логической специфи-
кации. II // Там же. – N 6. – C. 16—26.
3. Чеботарев А.Н. Проверка непротиворечиво-
сти простых спецификаций автоматных сис-
тем // Там же. – 1994. – N 3. – C. 3—11.
4. Чеботарев А.Н. Общий метод проверки со-
гласованности взаимодействующих автоматов
с конечной памятью // Там же. – 1999. –
N 6. – C. 25—37.
5. Чеботарев А.Н. Детерминизация логических
спецификаций автоматов // Там же. –
1995. – N1. – C. 3—12
6. Чеботарев А.Н. Синтез процедурного пред-
ставления автомата, специфицированного в
логическом языке L*. I // Там же. – 1997. –
N 4. – C. 60—74.
Получено 24.03.03
Об авторе
Чеботарев Анатолий Николаевич
д-р техн. наук, старш. научн. сотр.
Место работы автора:
Институт кибернетики им. В.М. Глушкова НАН
Украины,
просп. Академика Глушкова, 40
ГСП, г. Киев-187, 03680,
Украина
Тел. (044) 266 4549
E-mail: cheb@d105.icyb.kiev.ua
uw
u¬w
Рисунок. Автомат A(S)
¬u¬w
¬uw
¬uw
u¬w ¬uw
2
1
32
31
u¬w
|