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

УДК 519.713.1

А. Н. ЧЕБОТАРЕВ

О КЛАССЕ ФОРМУЛ ЯЗЫКА L*, СПЕЦИФИЦИРУЮЩИХ АВТОМАТЫ
С КОНЕЧНОЙ ПАМЯТЬЮ

Ключевые слова: язык спецификации L*, $-формула, двустороннее сверхслово,
S-автомат, автомат с конечной памятью, k-разделимость.

ВВЕДЕНИЕ

Автоматы с конечной памятью [1, 2] играют важную роль в теории и практике проектирования дискретных систем. С одной стороны, эти автоматы обладают такими свойствами, которые позволяют упростить методы их анализа, преобразования и реализации, с другой — практически всякая реализация автомата, то ли в виде аппаратурного модуля, то ли в виде программы, может рассматриваться как автомат с конечной памятью. Более того, любой автомат, не обладающий конечной памятью, за счет расширения его алфавита можно преобразовать в автомат с конечной памятью, сохраняя его функциональность, т. е. выполняемую им функцию. Логические языки спецификации автоматов, не обладающих конечной памятью, гораздо богаче языков спецификации автоматов с конечной памятью. Примером языка, позволяющего специфицировать только автоматы с конечной памятью, является достаточно простой язык L [3]. Использование этого языка позволяет значительно упростить процедуры проектирования, т. е. перехода от декларативной спецификации требований к функционированию автомата к его императивному (процедурному) представлению. Язык L* является расширением языка L за счет введения дополнительных выразительных средств, необходимых для спецификации автоматов, не обладающих конечной памятью. Заметим, что ни язык L*, ни какой-либо другой язык логики предикатов первого порядка не дают возможности специфицировать произвольные автоматы. Тем не менее язык L* позволяет специфицировать достаточно широкий класс автоматов, представляющих интерес с практической точки зрения. Расширение языка L привело к существенному усложнению методов синтеза, основанных на теореме о спецификации [4]. Описанная в [4] версия языка L* строилась таким образом, чтобы формулы языка могли быть эквивалентно преобразованы к виду, удовлетворяющему условиям теоремы о спецификации. Здесь рассматривается несколько расширенный вариант этого языка, выходящий за рамки требований теоремы о спецификации, в результате чего в некоторых случаях имеющиеся процедуры синтеза могут давать неверный результат. Кроме того, большинство методов проектирования, таких как проверка непротиворечивости спецификаций, их детерминизация, проверка реализуемости открытой системы, верификация, и другие, разработаны для спецификаций в языке L. Поэтому большое значение имеет возможность преобразования спецификации из языка L* в язык L. Учитывая, что в языке L могут быть специфицированы только автоматы с конечной памятью, такое преобразование предполагает переход от спецификации автомата, не обладающего конечной памятью, к спецификации соответствующего автомата с конечной памятью. Для обоснования способа такого преобразования необходимо охарактеризовать класс формул языка L*, специфицирующих автоматы с конечной памятью. Очевидно, что все формулы языка L принадлежат этому классу, однако существенный интерес для такого преобразования представляют формулы, специфицирующие автоматы с конечной памятью и не принадлежащие языку L. В настоящей работе вводятся необходимые понятия, в терминах которых характеризуется класс формул, специфицирующих автоматы с конечной памятью. Такая характеризация позволяет обосновать переход от спецификации в языке L* к спецификации в языке L.

ЦИКЛИЧЕСКИЕ S-АВТОМАТЫ С КОНЕЧНОЙ ПАМЯТЬЮ

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

S-автомат A = <S, Q, dA> называется циклическим, если для каждого q Î Q существуют такие s1, s2 Î S и q1, q2 Î Q, что q1 Î dA(q, s1) и q Î dA(q2, s2).

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

Пусть S — конечный алфавит, Z — множество целых чисел, N+ = {z Î Zô z > 0} и N- = {z Î Zô z £ 0}. Отображение r множества {1, …, n} (n Î N+) в S называется словом длины n в алфавите S и обозначается r = r(1)r(2)…r(n). Отображения u: Z ® S, l: N+® S и g: N-® S называются соответственно двусторонним сверхсловом (обозначается …u(-2)u(-1)u(0)u(1)u(2)…), сверхсловом (обозначается l(1)l(2)… ) и обратным сверхловом (обозначается …g(-2)g(-1)g(0)) в алфавите S. Множество всех слов в алфавите S обозначается S*. Множества всех сверхслов и обратных сверхслов в алфавите S будем обозначать соответственно Sw и S-w. Отрезок u(t)u(t + 1)…u(t + k) двустороннего сверхслова u обозначается u(t, t + 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 = s1s2 … в алфавите S допустимо в состоянии q S-автомата A, если существует такое сверхслово состояний q0q1q2…, где q0 = q, что для любого i = 0, 1, 2, … qi+1 = dA(qi, si+1).

Обратное сверхслово в алфавите S …s-1s0 представимо состоянием q S-автомата A, если существует такое обратное сверхслово состояний …q-2q-1q0, где q0 = q, что для любого i = -1, -2, … dA(qi, si+1) = qi+1.

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

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

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

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

Пусть A = <S, Q, dA> и q1, q2 Î Q, s Î S. Тройку <q1, s, q2>, такую что dA(q1, s) = q2, назовем переходом в S-автомате A из состояния q1 в состояние q2. Будем говорить, что входное слово r = s1¼sn переводит состояние q¢ в состояние q², если для каждого i = 1, …, n в автомате A имеется переход <qi, si, qi+1> и q¢ = q1, q²= qn+1.

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

Утверждение 1. Приведенный циклический S-автомат A с множеством состояний Q обладает конечной памятью глубины не более k тогда и только тогда, когда для любых qi, qj Î Q (qi ¹ qj) Pk(qi) Ç Pk(qj) = Æ.

Доказательство. Необходимость. Допустим противное, т. е. что существуют такие состояния qi, qj Î Q, что Pk(qi) Ç Pk(qj) ¹Æ. Тогда существуют состояния, которые одним и тем же словом длины k переводятся в неэквивалентные состояния (в силу приведенности автомата), что противоречит определению автомата с конечной памятью глубины k.

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

ЯЗЫКИ СПЕЦИФИКАЦИИ L И L*

Языки L* и L построены на основе соответствующих фрагментов логики предикатов первого порядка с одноместными предикатами, определенными на множестве моментов дискретного времени, в качестве которого выступает множество Z целых чисел. Спецификация в обоих языках имеет вид формулы "tF(t), где F(t) — формула с одной свободной переменной t. В языке L формула F(t) строится с помощью логических связок из атомов вида p(t + k), где p — одноместный предикатный символ, t — переменная, принимающая значения из множества Z, а k — целочисленная константа (сдвиг во времени). Язык L* отличается от языка L тем, что при построении формулы F(t) наряду с атомарными формулами используются формулы вида $ti(ti £ t + k1)&F1(ti)&"tj((ti + k2 £ tj £ t + k3) ® F2(tj)), где k1, k2, k3 Î Z, F2(tj) — формула языка L, а F1(ti) — формула языка L*. Такие формулы будем называть $-формулами. Для эквивалентного преобразования формул F(t) такого вида часто используется равносильность [5]

F(t) Û F(t - 1)&h(t) Ú g(t), (1)

где F(t - 1) обозначает формулу, полученную из F(t) путем замены t на t - 1, h(t) = F2(t + k3), а g(t) = (F1(t + k1) Ú …Ú F1(t - k2 + k3+1), если k3 < k1 + k2, или F1(t + k1) & F2(t + k3) & … & F2(t + k1 + k2), если k3 ³ k1 + k2 ). Правую часть равносильности (1) назовем 1-разверткой $-формулы F(t).

Каждой замкнутой формуле F ставится в соответствие множество M(F) моделей для этой формулы, т. е. множество таких интерпретаций, на которых F истинна. Пусть W = {p1, …, pm} — множество всех предикатных символов, встречающихся в формуле F (сигнатура формулы). Интерпретация формулы F — это упорядоченный набор определенных на Z одноместных предикатов p1, ¼, pm, соответствующих предикатным символам из W. Интерпретацию I = <p1, ¼, pm> можно представить в виде двустороннего сверхслова в алфавите S(W), где W = {p1, …, pm}. Алфавит S(W) представляет собой множество всех двоичных векторов длины m. Символы алфавита S(W) иногда удобно рассматривать как отображения s: W ® {0,1}. Пусть W1 Í W, проекцией символа s Î S(W) на W1 будем называть ограничение отображения s на W1. Понятие проекции символа на W1 естественным образом распространяется на слова и сверхслова, так что проекция сверхслова в алфавите S(W) на W1 есть сверхслово в алфавите S(W1).

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

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

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

В [4] показано, что S-автомат A(F) = <S, QA, d>, поведение которого совпадает с S(F) = {S1, …, Sn}, может быть определен следующим образом: S = S(W), QA = {q1, …, qn} и для qi Î QA , s Î S значение d(qi, s) определено и равно qj тогда и только тогда, когда s\Si = Sj , если s\Si = Æ, то значение d(qi, s) не определено. Если функцию переходов автомата A(F) определить как d*: QA´S* ® QA, то для qi Î QA, r Î S* d*(qi, r) = qj тогда и только тогда, когда r\Si = Sj. Заметим, что если r\Si = Sj и g Î Pi, то g×r Î Pj, и наоборот, если g Î Pi и g×r Î Pj, то r\Si = Sj×

Два 0-префикса, g1, g2 Î P(F), назовем эквивалентными, если множества всех допустимых продолжений для них совпадают, т. е. S(g1) = S(g2). Таким образом, совокупности множеств S(F) = {S1, …, Sn} соответствует разбиение множества P(F) на классы эквивалентности P1, …, Pn.

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

Доказательство. 1. Пусть слово r — суффикс обратного сверхслова g Î Pj, т. е. g = g1×r, и g1 Î Pi. Тогда r\Si = Sj, т. е. d*(qi, r) = qj. Таким образом, слово r представимо состоянием qj.

2. Пусть r представимо состоянием qj, т. е. существует такое состояние qi, что d*(qi, r) = qj. Как следует из определения функции переходов d* автомата A(F), r\Si = Sj. Пусть g Î Pi. Тогда g×r Î Pj, т. е. r — суффикс обратного сверхслова, принадлежащего Pj. Конец доказательства.

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

СПЕЦИФИКАЦИИ АВТОМАТОВ С КОНЕЧНОЙ ПАМЯТЬЮ

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

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

Справедливость этой теоремы следует непосредственно из утверждений 1 и 2.

Формула F(t), с единственной свободной переменной t, называется k-ограниченной (k ΠZ), если для любого t Î Z значения формулы F(t – k) на всех двусторонних сверхсловах, имеющих одинаковые t-префиксы, совпадают. Смысл данного определения состоит в том, что при вычислении истинностного значения k-ограниченной формулы F(t) в позиции t интерпретации u не нужно рассматривать значения предикатов для t > t + k. Примером 0-ограниченной формулы F(t) может служить формула $t1(t1 £ t)&y(t1)&"t2((t1 < t2 £ t) ® Øx(t2)). Будем рассматривать 0-ограниченные формулы как способ задания множеств обратных сверхслов, а именно, будем полагать, что формула F(t) задает множество 0-префиксов всех тех двусторонних сверхслов, на которых истинна F(0). Заметим, что множества обратных сверхслов, задаваемые $-формулой и ее отрицанием, конечно неразделимы. Таким образом, необходимым условием того, что автомат, специфицируемый формулой F, не обладает конечной памятью, является наличие в ней $-подформул. Однако наличие в спецификации $-подформулы не всегда приводит к тому, что специфицируемый автомат не обладает конечной памятью. Ниже покажем, что любую спецификацию "tF(t) в языке L* за счет введения дополнительных предикатных символов можно преобразовать в спецификацию "tFz(t) в этом же языке, специфицирующую автомат с конечной памятью.

Формула Fz(t) получается из формулы F(t) следующим образом. Все имеющиеся в F(t) $-подформулы вида ji(ti) (i = 1, 2, …, n) последовательно, начиная с подформул, имеющих максимальную глубину вложения в другие $-подформулы, заменяются атомами вида zi(ti + ri), где ri — ранг заменяемой $-подформулы [5], а zi — новый предикатный символ, отсутствующий в текущей формуле. Полученную формулу обозначим fz(t). С каждым введенным предикатом zi(t), соответствующим формуле ji(ti), ассоциируется формула zi(t) « ji(t – ri), где ji(t – ri) получается из ji(ti) заменой ti на t – ri. Формула Fz(t) имеет вид fz(t) (zi(t) « ji(t – ri)).

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

Доказательство. Пусть u1 — модель для формулы "tFz(t). Покажем, что формула F(t) истинна в произвольной позиции t проекции u1 на W. Поскольку u1 — модель для формулы "tFz(t), то fz(t) истинна в позиции t и для каждого t Î Z значение zi(t + ri) совпадает со значением ji(t). Формула F(t) получается, если в fz(t) вместо всех вхождений атомов вида zi(ti + ri) подставить правые части эквивалентностей для zi(t), заменив в них t на ti + ri. Отсюда следует, что F(t) истинна в позиции t проекции u1 на W. Обратно, имея модель u для формулы "tF(t), легко построить соответствующую модель для "tFz(t), положив для каждого t ΠZ и i = 1, 2, …, n zi(t) = ji(t – ri). Остальные предикатные символы в каждой позиции t имеют те же значения, что и в модели u. Конец доказательства.

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

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

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

Из этого утверждения следует, что всякая модель для формулы Fz = "tfz(t)(zi(t) « ji(t)) является моделью для формулы fz = "tfz(t)(zi(t) « (zi(t – 1)&hi(t) Ú gi(t))), где hi(t) и gi(t) определяются 1-развертками соответствующих формул ji(t).

Пусть g — 0-префикс модели для формулы Fz = "tFz(t) = "tfz(t)(zi(t) « ji(t)) и 1-развертки для формул ji(t) имеют соответственно вид ji(t – 1)&hi(t) Ú gi(t) (i = 1, 2, …, n).

Утверждение 5. Множества всех допустимых продолжений для g, определяемых формулой Fz и формулой fz = "tf(t) = "tfz(t)(zi(t) « (zi(t – 1)&hi(t) Ú gi(t))), совпадают.

Доказательство. Пусть l — допустимое продолжение для g, определяемое формулой fz, покажем, что оно допустимо и для формулы Fz, т. е. что в любой его позиции t истинна формула Fz(t). Доказательство проведем индукцией по длине префикса сверхслова l, соответствующего позиции t этого сверхслова. Базис: t = 0. Префикс нулевой длины соответствует самой правой позиции обратного сверхслова g. Поэтому значения f(t) и Fz(t) в этой позиции совпадают. Покажем теперь, что из совпадения значений f(t) и Fz(t) в позиции t следует совпадение их значений в позиции t + 1. Для этого достаточно показать, что zi(t + 1) = ji(t + 1) для всех i = 1, 2, …, n. Из истинности Fz(t) в позиции t следует, что zi(t) = ji(t) (i = 1, 2, …, n), поэтому из ji(t + 1) = (ji(t)&hi(t + 1) Ú gi(t + 1)) и zi(t + 1) = (zi(t)&hi(t + 1) Ú gi(t + 1)) следует, что zi(t + 1) = ji(t + 1) (i = 1, 2, …, n). Таким образом, значения f(t) и Fz(t) в позиции t + 1 совпадают.

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

Теорема 2. Формула Fz = "tfz(t)(zi(t) « ji(t)), полученная из формулы языка L* описанным выше способом, специфицирует автомат с конечной памятью.

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

ЗАКЛЮЧЕНИЕ

Известно, что любой (конечный) автомат, не обладающий конечной памятью, можно преобразовать в автомат с конечной памятью путем добавления переменных, определяющих структуру выходного алфавита, и коррекции функции выходов таким образом, чтобы сохранялось поведение соответствующего S-автомата относительно исходного алфавита. В настоящей статье такое преобразование осуществляется регулярным образом на уровне спецификации требований к функционированию автомата. Спецификация в языке 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.

Поступила 14.02.2009