О классе формул языка L*, специфицирующих автоматы с конечной памятью

Размещено на http://www.allbest.ru/

Размещено на http://www.allbest.ru/

О классе формул языка L^*, специфицирующих автоматы с конечной памятью

А.Н. Чеботарев

Введение

Автоматы с конечной памятью [1, 2] играют важную роль в теории и практике проектирования дискретных систем. С одной стороны, эти автоматы обладают такими свойствами, которые позволяют упростить методы их анализа, преобразования и реализации, с другой -- практически всякая реализация автомата, то ли в виде аппаратурного модуля, то ли в виде программы, может рассматриваться как автомат с конечной памятью. Более того, любой автомат, не обладающий конечной памятью, за счет расширения его алфавита можно преобразовать в автомат с конечной памятью, сохраняя его функциональность, т.е. выполняемую им функцию. Логические языки спецификации автоматов, не обладающих конечной памятью, гораздо богаче языков спецификации автоматов с конечной памятью.

Примером языка, позволяющего специфицировать только автоматы с конечной памятью, является достаточно простой язык L [3]. Использование этого языка позволяет значительно упростить процедуры проектирования, т.е. перехода от декларативной спецификации требований к функционированию автомата к его императивному (процедурному) представлению. Язык L^* является расширением языка L за счет введения дополнительных выразительных средств, необходимых для спецификации автоматов, не обладающих конечной памятью. Заметим, что ни язык L^*, ни какой-либо другой язык логики предикатов первого порядка не дают возможности специфицировать произвольные автоматы. Тем не менее язык L^* позволяет специфицировать достаточно широкий класс автоматов, представляющих интерес с практической точки зрения.

Расширение языка L привело к существенному усложнению методов синтеза, основанных на теореме о спецификации [4]. Описанная в [4] версия языка L^* строилась таким образом, чтобы формулы языка могли быть эквивалентно преобразованы к виду, удовлетворяющему условиям теоремы о спецификации. Здесь рассматривается несколько расширенный вариант этого языка, выходящий за рамки требований теоремы о спецификации, в результате чего в некоторых случаях имеющиеся процедуры синтеза могут давать неверный результат. Кроме того, большинство методов проектирования, таких как проверка непротиворечивости спецификаций, их детерминизация, проверка реализуемости открытой системы, верификация, и другие, разработаны для спецификаций в языке L.

Поэтому большое значение имеет возможность преобразования спецификации из языка L^* в язык L. Учитывая, что в языке L могут быть специфицированы только автоматы с конечной памятью, такое преобразование предполагает переход от спецификации автомата, не обладающего конечной памятью, к спецификации соответствующего автомата с конечной памятью. Для обоснования способа такого преобразования необходимо охарактеризовать класс формул языка L^*, специфицирующих автоматы с конечной памятью. Очевидно, что все формулы языка L принадлежат этому классу, однако существенный интерес для такого преобразования представляют формулы, специфицирующие автоматы с конечной памятью и не принадлежащие языку L. В настоящей работе вводятся необходимые понятия, в терминах которых характеризуется класс формул, специфицирующих автоматы с конечной памятью. Такая характеризация позволяет обосновать переход от спецификации в языке L^* к спецификации в языке L.

1. Циклические -автоматы с конечной памятью

Языки L и L^* используются для спецификации и проектирования реактивных систем, в частности автоматов над бесконечными словами (сверхсловами). Основным объектом спецификации и синтеза является частичный, неинициальный, детерминированный автомат без выходов A = <, Q, _A>, где -- конечный входной алфавит, Q -- конечное множество состояний, _A: Q Q -- частичная функция переходов. Такой автомат назовем -автоматом.

-автомат A = <, Q, _A> называется циклическим, если для каждого q Q существуют такие , и q₁, q₂ Q, что q_{1 A}(q, ₁) и q _A(q₂, ₂).

Поведение циклического -автомата удобно описывать в терминах множеств слов и сверхслов над алфавитом , поэтому приведем основные определения, связанные с этими понятиями.

Пусть -- конечный алфавит, Z -- множество целых чисел, N⁺ = {z Z z 0} и N = {z Z z 0}. Отображение r множества {1, …, n} (n N⁺) в называется словом длины n в алфавите и обозначается r = r(1)r(2)…r(n). Отображения u: Z , l:N⁺ и g: N называются соответственно двусторонним сверхсловом (обозначается …u(2)u(1)u(0)u(1)u(2)…), сверхсловом (обозначается l(1)l(2)… ) и обратным сверхловом (обозначается …g(2)g(1)g(0)) в алфавите . Множество всех слов в алфавите обозначается ^*. Множества всех сверхслов и обратных сверхслов в алфавите будем обозначать соответственно и . Отрезок u()u( + 1)…u( + k) двустороннего сверхслова u обозначается u(, + k). Бесконечные отрезки u(-, k) и u(k + 1, ) назовем соответственно k-префиксом и k-суффиксом двустороннего сверхслова u. Для n N⁺ n-префиксом сверхслова l называется слово l(1)…l(n) и n-суффиксом обратного сверхслова g -- слово g(1 n)… g(0).

Сверхслово l = ₁₂ … в алфавите допустимо в состоянии q -автомата A, если существует такое сверхслово состояний q₀q₁q₂…, где q₀ = q, что для любого i = 0, 1, 2, … q_i+1 = _A(q_i, _i+1).

Обратное сверхслово в алфавите … представимо состоянием q -автомата A, если существует такое обратное сверхслово состояний …q₂q₁q₀, где q₀ = q, что для любого i = , , … _A(q_i, _i+1) = q_i+1.

Таким образом, с каждым состоянием q_i циклического -автомата ассоциируются два множества сверхслов: множество S(q_i) всех сверхслов, допустимых в состоянии q_i, и множество P(q_i) всех обратных сверхслов, представимых состоянием q_i. Аналогично, для произвольного k N⁺ рассмотрим множество S ^k(q_i) всех слов длины k, допустимых в состоянии q_i, и множество P ^k(q_i) всех слов длины k, представимых состоянием q_i.

Состояния q_i и q_j называются эквивалентными, если S(q_i) = S(q_j). Автомат, не имеющий эквивалентных состояний, называется приведенным.

Пусть множество Q состояний -автомата A равно {q₁, …, q_n}. Семейство множеств сверхслов (S(q₁),…, S(q_n)) назовем поведением автомата A.

Два автомата, A₁ и A₂, с поведениями соответственно () и () называются эквивалентными, если каждое (i = 1, …, n) содержится среди и каждое (i = 1, …, m) содержится среди .

Пусть A = <, Q, _A> и q₁, q₂ Q, . Тройку <q₁, , q₂>, такую что _A(q₁, ) = q₂, назовем переходом в -автомате A из состояния q₁ в состояние q₂. Будем говорить, что входное слово r = _n переводит состояние q в состояние q, если для каждого i = 1, …, n в автомате A имеется переход <q_i, _i, q_i+1> и q = q₁, q= q_n+1.

-автомат A называется автоматом с конечной памятью, если существует такое натуральное k, что для любого входного слова длины k все состояния автомата A, в которых оно допустимо, переводятся этим словом в эквивалентные состояния. Минимальное такое k называется глубиной памяти автомата.

Утверждение 1. Приведенный циклический -автомат A с множеством состояний Q обладает конечной памятью глубины не более k тогда и только тогда, когда для любых q_i, q_j Q (q_i q_j) P^k(q_i) P^k(q_j) = .

Доказательство. Необходимость. Допустим противное, т.е. что существуют такие состояния q_i, q_j Q, что P^k(q_i) P^k(q_j) . Тогда существуют состояния, которые одним и тем же словом длины k переводятся в неэквивалентные состояния (в силу приведенности автомата), что противоречит определению автомата с конечной памятью глубины k.

Достаточность. Если множества слов длины k, представимых состояниями автомата A, не пересекаются, то каждое слово длины k, допустимое для автомата A, содержится только в одном из P^k(q_i) (q_i Q). Отсюда следует, что каждое слово длины k переводит все состояния автомата A, в которых оно допустимо, в одно и то же состояние, из чего, в свою очередь, вытекает, что автомат A обладает конечной памятью глубины не более k. Конец доказательства.

2. Языки спецификации L и L^*

Языки L^* и L построены на основе соответствующих фрагментов логики предикатов первого порядка с одноместными предикатами, определенными на множестве моментов дискретного времени, в качестве которого выступает множество Z целых чисел. Спецификация в обоих языках имеет вид формулы tF(t), где F(t) -- формула с одной свободной переменной t. В языке L формула F(t) строится с помощью логических связок из атомов вида p(t + k), где p -- одноместный предикатный символ, t -- переменная, принимающая значения из множества Z, а k -- целочисленная константа (сдвиг во времени). Язык L^* отличается от языка L тем, что при построении формулы F(t) наряду с атомарными формулами используются формулы вида $t_i(t_i t + k₁)&F₁(t_i)&t_j((t_i + k₂ t_j t + k₃) F₂(t_j)), где k₁, k₂, k₃ Z, F₂(t_j) -- формула языка L, а F₁(t_i) -- формула языка L^*. Такие формулы будем называть -формулами. Для эквивалентного преобразования формул F(t) такого вида часто используется равносильность [5]

F(t) F(t 1)&h(t) Ъ--g(t), (1)

где F(t 1) обозначает формулу, полученную из F(t) путем замены t на t 1, h(t) = F₂(t + k₃), а g(t) = (F₁(t + k₁) Ъ--…Ъ--F₁(t k₂ + k₃+1), если k₃ < k₁ + k₂, или F₁(t + k₁) & F₂(t + k₃) & … & F₂(t + k₁ + k₂), если k₃ і k₁ + k₂ ). Правую часть равносильности (1) назовем 1-разверткой -формулы F(t).

Каждой замкнутой формуле F ставится в соответствие множество M(F) моделей для этой формулы, т.е. множество таких интерпретаций, на которых F истинна. Пусть = {p₁, …, p_m} -- множество всех предикатных символов, встречающихся в формуле F (сигнатура формулы). Интерпретация формулы F -- это упорядоченный набор определенных на Z одноместных предикатов _{1 m}, соответствующих предикатным символам из . Интерпретацию I = <_{1 m}> можно представить в виде двустороннего сверхслова в алфавите (), где = {p₁, …, p_m}. Алфавит () представляет собой множество всех двоичных векторов длины m. Символы алфавита () иногда удобно рассматривать как отображения : {0,1}. Пусть ₁ , проекцией символа () на ₁ будем называть ограничение отображения на ₁. Понятие проекции символа на ₁ естественным образом распространяется на слова и сверхслова, так что проекция сверхслова в алфавите () на ₁ есть сверхслово в алфавите (₁).

В дальнейшем не будем различать интерпретации и соответствующие им двусторонние сверхслова, поэтому можно говорить об истинностном значении формулы F на двустороннем сверхслове u и значении формулы F(t) в некоторой позиции двустороннего сверхслова u.

Пусть P(F) -- множество 0-префиксов всех моделей из M(F). Каждому g P(F) поставим в соответствие множество сверхслов S(g) = {l | gl M(F)}. Другими словами, S(g) состоит из всех тех сверхслов, конкатенация каждого из которых с 0-префиксом g соответствует модели для F. Такие сверхслова назовем допустимыми продолжениями 0-префикса g. Таким образом получим совокупность множеств сверхслов S(F) = {S(g) g P(F)}. Основная идея, позволяющая использовать формулу F для спецификации автомата, состоит в том, что совокупность множеств сверхслов S(F) рассматривается как поведение некоторого -автомата.

Пусть S и r ^*. Левым частным множества сверхслов S по слову r (обозначается r\S) называется множество всех таких сверхслов l, что rl S, т.е. r\S = {l | rl S}. Таким образом, если r\S = S₁, то rS₁ S.

В [4] показано, что -автомат A(F) = <, Q_A, >, поведение которого совпадает с S(F) = {S₁, …, S_n}, может быть определен следующим образом: = (), Q_A = {q₁, …, q_n} и для q_i Q_A , значение q_i, определено и равно q_j тогда и только тогда, когда \S_i = S_j , если \S_i = , то значение q_i, не определено. Если функцию переходов автомата A(F) определить как ^*: Q_A^* Q_A, то для q_i Q_A, r ^{* *}q_i, r = q_j тогда и только тогда, когда r\S_i = S_j. Заметим, что если r\S_i = S_j и g P_i, то gr P_j, и наоборот, если g P_i и gr P_j, то r\S_i = S_j

Два 0-префикса, g₁, g₂ P(F), назовем эквивалентными, если множества всех допустимых продолжений для них совпадают, т.е. S(g₁) = S(g₂). Таким образом, совокупности множеств S(F) = {S₁, …, S_n} соответствует разбиение множества P(F) на классы эквивалентности P₁, …, P_n.

Утверждение 2. Множество k-суффиксов (k N⁺) всех обратных сверхслов из класса P_j совпадает с множеством всех слов длины k, представимых состоянием q_j автомата A(F).

Доказательство. 1. Пусть слово r -- суффикс обратного сверхслова g P_j, т.е. g = g₁r, и g₁ P_i. Тогда r\S_i = S_j, т.е. ^*q_i, r = q_j. Таким образом, слово r представимо состоянием q_j.

2. Пусть r представимо состоянием q_j, т.е. существует такое состояние q_i, что ^*q_i, r = q_j. Как следует из определения функции переходов ^* автомата A(F), r\S_i = S_j. Пусть g P_i. Тогда gr P_j, т.е. r -- суффикс обратного сверхслова, принадлежащего P_j. Конец доказательства.

Хотя это утверждение справедливо для слов произвольной длины, оно не справедливо для сверхслов. Множество P_j может не совпадать с множеством всех обратных сверхслов, представимых состоянием q_j.

3. Спецификации автоматов с конечной памятью

Непересекающиеся множества P_i и P_j обратных сверхслов в одном и том же алфавите называются k-разделимыми, если существует такое k N⁺, что множества k-суффиксов всех обратных сверхслов из P_i и всех обратных сверхслов из P_j не пересекаются. Два непересекающихся множества обратных сверхслов называются конечно неразделимыми, если не существует такого k N⁺, что они k-разделимы.

Теорема 1. Формула F = tF(t) языка L^* специфицирует автомат с конечной памятью тогда и только тогда, когда существует такое k N⁺, что классы эквивалентности обратных сверхслов из P(F) попарно k-разделимы.

Справедливость этой теоремы следует непосредственно из утверждений 1 и 2. Формула F(t), с единственной свободной переменной t, называется k-ограниченной (kZ), если для любого Z значения формулы F( - k) на всех двусторонних сверхсловах, имеющих одинаковые -префиксы, совпадают. Смысл данного определения состоит в том, что при вычислении истинностного значения k-ограниченной формулы F(t) в позиции интерпретации u не нужно рассматривать значения предикатов для t + k. Примером 0-ограниченной формулы F(t) может служить формула t₁(t₁ t)&y(t₁)&t₂((t₁ t₂ t) x(t₂)). Будем рассматривать 0-ограниченные формулы как способ задания множеств обратных сверхслов, а именно, будем полагать, что формула F(t) задает множество 0-префиксов всех тех двусторонних сверхслов, на которых истинна F(0). Заметим, что множества обратных сверхслов, задаваемые -формулой и ее отрицанием, конечно неразделимы. Таким образом, необходимым условием того, что автомат, специфицируемый формулой F, не обладает конечной памятью, является наличие в ней -подформул. Однако наличие в спецификации -подформулы не всегда приводит к тому, что специфицируемый автомат не обладает конечной памятью. Ниже покажем, что любую спецификацию tF(t) в языке L^* за счет введения дополнительных предикатных символов можно преобразовать в спецификацию tF_z(t) в этом же языке, специфицирующую автомат с конечной памятью.

Формула F_z(t) получается из формулы F(t) следующим образом. Все имеющиеся в F(t) $-подформулы вида _i(t_i) (i = 1, 2, …, n) последовательно, начиная с подформул, имеющих максимальную глубину вложения в другие $-подформулы, заменяются атомами вида z_i(t_i + r_i), где r_i -- ранг заменяемой $-подформулы [5], а z_i -- новый предикатный символ, отсутствующий в текущей формуле. Полученную формулу обозначим f_z(t). С каждым введенным предикатом z_i(t), соответствующим формуле _i(t_i), ассоциируется формула z_i(t) _i(t - r_i), где _i(t - r_i) получается из _i(t_i) заменой t_i на t - r_i. Формула F_z(t) имеет вид f_z(t) (z_i(t) _i(t - r_i)).

Утверждение 3. Проекция любой модели для формулы tF_z(t) на сигнатуру формулы F(t) является моделью для формулы tF(t), и наоборот, для любой модели u формулы tF(t) существует модель для формулы tF_z(t), проекция которой на совпадает с u.

Доказательство. Пусть u₁ -- модель для формулы tF_z(t). Покажем, что формула F(t) истинна в произвольной позиции проекции u₁ на . Поскольку u₁ -- модель для формулы tF_z(t), то f_z(t) истинна в позиции и для каждого Z значение z_i( + r_i) совпадает со значением _i(). Формула F(t) получается, если в f_z(t) вместо всех вхождений атомов вида z_i(t_i + r_i) подставить правые части эквивалентностей для z_i(t), заменив в них t на t_i + r_i. Отсюда следует, что F(t) истинна в позиции проекции u₁ на . Обратно, имея модель u для формулы tF(t), легко построить соответствующую модель для tF_z(t), положив для каждого Z и i = 1, 2, …, n z_i() = _i( - r_i). Остальные предикатные символы в каждой позиции имеют те же значения, что и в модели u. Конец доказательства.

Пусть 1-развертка $-формулы (t) имеет вид (t 1)&h(t) Ъ--g(t), где формулы h(t) и g(t) не содержат вхождений $-формул.

Утверждение 4. Всякая модель для формулы F = t(z(t) (t)), где z -- предикатный символ, не содержащийся в (t), является моделью для формулы F₁ = t(z(t) (z(t 1)&h(t) Ъ--g(t))).

Доказательство. Пусть u -- модель для формулы F, тогда в любой позиции Z интерпретации u значения z() и () совпадают. Из этого следует, что формулы t(z(t) ((t 1)&h(t) Ъ--g(t))) и F₁ = t(z(t) (z(t 1)&h(t) Ъ--g(t))) в любой позиции интерпретации u принимают одно и то же значение. Таким образом, в силу равносильности (1) u -- модель для формулы F₁. Конец доказательства.

Из этого утверждения следует, что всякая модель для формулы F_z = tf_z(t)(z_i(t) _i(t)) является моделью для формулы f_z = tf_z(t)(z_i(t) (z_i(t - 1)&h_i(t) Ъ--g_i(t))), где h_i(t) и g_i(t) определяются 1-развертками соответствующих формул _i(t).

Пусть g -- 0-префикс модели для формулы F_z = tF_z(t) = tf_z(t)(z_i(t) _i(t)) и 1-развертки для формул _i(t) имеют соответственно вид _i(t - 1)&h_i(t) Ъ--g_i(t) (i = 1, 2, …, n).

Утверждение 5. Множества всех допустимых продолжений для g, определяемых формулой F_z и формулой f_z = tf(t) = tf_z(t)(z_i(t) (z_i(t - 1)&h_i(t) Ъ--g_i(t))), совпадают.

Доказательство. Пусть l -- допустимое продолжение для g, определяемое формулой f_z, покажем, что оно допустимо и для формулы F_z, т.е. что в любой его позиции истинна формула F_z(t). Доказательство проведем индукцией по длине префикса сверхслова l, соответствующего позиции этого сверхслова. Базис: = 0. Префикс нулевой длины соответствует самой правой позиции обратного сверхслова g. Поэтому значения f(t) и F_z(t) в этой позиции совпадают. Покажем теперь, что из совпадения значений f(t) и F_z(t) в позиции следует совпадение их значений в позиции + 1. Для этого достаточно показать, что z_i( + 1) = _i( + 1) для всех i = 1, 2, …, n. Из истинности F_z(t) в позиции следует, что z_i() = _i() (i = 1, 2, …, n), поэтому из _i( + 1) = (_i()&h_i( + 1) Ъ--g_i( + 1)) и z_i( + 1) = (z_i()&h_i( + 1) Ъ--g_i( + 1)) следует, что z_i( + 1) = _i( + 1) (i = 1, 2, …, n). Таким образом, значения f(t) и F_z(t) в позиции + 1 совпадают.

Обратное утверждение, т.е. что допустимое для формулы F_z продолжение обратного сверхслова g совпадает с допустимым его продолжением для формулы f_z, следует из того, что множество моделей для F_z содержится в множестве моделей для f_z. Конец доказательства.

Теорема 2. Формула F_z = tf_z(t)(z_i(t) _i(t)), полученная из формулы языка L^* описанным выше способом, специфицирует автомат с конечной памятью.

Доказательство. Из утверждений 4 и 5 следует, что S(F_z) S(f_z), т.е. автомат, специфицируемый формулой F_z, является подавтоматом автомата, специфицируемого формулой f_z. Поскольку f_z -- формула языка L, специфицируемый ею автомат обладает конечной памятью [6]. Любой его подавтомат также обладает конечной памятью. Конец доказательства.

Заключение

Известно, что любой (конечный) автомат, не обладающий конечной памятью, можно преобразовать в автомат с конечной памятью путем добавления переменных, определяющих структуру выходного алфавита, и коррекции функции выходов таким образом, чтобы сохранялось поведение соответствующего -автомата относительно исходного алфавита.

В настоящей статье такое преобразование осуществляется регулярным образом на уровне спецификации требований к функционированию автомата. Спецификация в языке L^* за счет введения дополнительных предикатных символов преобразуется в спецификацию в этом же языке, но специфицирующую автомат с конечной памятью. При этом проекция всех моделей преобразованной спецификации на исходную сигнатуру совпадает с множеством всех моделей для исходной спецификации. В статье доказывается, что преобразованная спецификация обладает всеми необходимыми свойствами.

Поскольку класс автоматов с конечной памятью совпадает с классом автоматов, специфицируемых в языке L, для преобразованной спецификации в языке L^* существует эквивалентная ей спецификация в языке L. При наличии способа получения такой спецификации синтез требуемого автомата может быть осуществлен средствами, разработанными для языка L. Таким способом может быть решено несколько проблем. Во-первых, устраняется необходимость проверки состояний синтезированного автомата на фиктивность, во-вторых, расширяются возможности применения методов синтеза к спецификациям, не удовлетворяющим теореме о спецификации [4].

В связи с этим в настоящей работе рассматривается расширенный вариант языка L^*, выходящий за рамки требований теоремы о спецификации, на которой были основаны все методы синтеза. Расширение языка L^* состоит в том, что в качестве подформул, входящих в -формулы языка, могут использоваться не только -формулы и формулы языка L, но и произвольные формулы языка L^*.

автомат память предикатный язык

Список литературы

1. Гилл А. Введение в теорию конечных автоматов. -- М.: Наука, 1966. -- 227 с.

2. Брауэр В. Введение в теорию конечных автоматов. -- М.: Радио и связь, 1987. -- 392 с.

3. Чеботарев А.Н. Об одном подходе к функциональной спецификации автоматных систем. I // Кибернетика и системный анализ. -- 1993. -- № 3. -- С. 31-42.

4. Чеботарев А.Н. Расширение логического языка спецификации и проблема синтеза // Там же. -- 1996. -- № 6. -- С. 11-27.

5. Чеботарев А.Н. Синтез процедурного представления автомата, специфицированного в логическом языке L^*. I // Там же. -- 1997. -- № 4. -- С. 60-74.

6. Чеботарев А.Н. Об одном подходе к функциональной спецификации автоматных систем. III // Там же. -- 1993. -- № 6. -- С. 3-14.

Размещено на Allbest.ru