С конечной памятью




Скачать 186.67 Kb.
НазваниеС конечной памятью
Дата публикации24.03.2013
Размер186.67 Kb.
ТипДокументы
uchebilka.ru > Математика > Документы


УДК 519.713.1

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

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


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

ВВЕДЕНИЕ

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

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

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

-автомат A = <, Q, A> называется циклическим, если для каждого qQ существуют такие ,    и q1, q2Q, что q1  A(q, 1) и q  A(q2, 2).

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

Пусть  — конечный алфавит, ^ Z — множество целых чисел, N+ = {zZz  0} и N = {z  Zz  0}. Отображение r множества {1, …, n} (nN+) в  называется словом длины n в алфавите  и обозначается r = r(1)r(2)…r(n). Отображения u: Z  , lN+  и 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. Для nN+ n-префиксом сверхслова l называется слово l(1)…l(n) и n-суффиксом обратного сверхслова gслово g(1  n)… g(0).

Сверхслово l = 12 … в алфавите  допустимо в состоянии q -автомата A, если существует такое сверхслово состояний q0q1q2, где q0 = q, что для любого i = 0, 1, 2, … qi+1 = A(qi, i+1).

Обратное сверхслово в алфавите  … представимо состоянием q -автомата A, если существует такое обратное сверхслово состояний …q2q1q0, где q0 = q, что для любого i = , , … A(qi, i+1) = qi+1.

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

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

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

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

Пусть A = <, Q, A> и q1, q2Q,   . Тройку <q1, , q2>, такую что A(q1, ) = q2, назовем переходом в -автомате A из состояния q1 в состояние q2. Будем говорить, что входное слово r = n переводит состояние q в состояние q, если для каждого i = 1, …, n в автомате A имеется переход <qi, i, qi+1> и q = q1, q= qn+1.

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

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

Доказательство. Необходимость. Допустим противное, т.е. что существуют такие состояния qi, qjQ, что 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(tit + k1)&F1(ti)&tj((ti + k2tjt + k3)  F2(tj)), где k1, k2, k3Z, 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), если k3k1 + k2 ). Правую часть равносильности (1) назовем 1-разверткой -формулы F(t).

Каждой замкнутой формуле F ставится в соответствие множество M(F) моделей для этой формулы, т.е. множество таких интерпретаций, на которых F истинна. Пусть  = {p1, …, pm} — множество всех предикатных символов, встречающихся в формуле F (сигнатура формулы). Интерпретация формулы F — это упорядоченный набор определенных на Z одноместных предикатов 1  m, соответствующих предикатным символам из . Интерпретацию I = <1  m> можно представить в виде двустороннего сверхслова в алфавите (), где  = {p1, …, pm}. Алфавит () представляет собой множество всех двоичных векторов длины m. Символы алфавита () иногда удобно рассматривать как отображения :   {0,1}. Пусть 1  , проекцией символа   () на 1 будем называть ограничение отображения  на 1. Понятие проекции символа на 1 естественным образом распространяется на слова и сверхслова, так что проекция сверхслова в алфавите () на 1 есть сверхслово в алфавите (1).

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

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

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

В [4] показано, что -автомат A(F) = <, QA, >, поведение которого совпадает с S(F) = {S1, …, Sn}, может быть определен следующим образом:  = (), QA = {q1, …, qn} и для qiQA ,    значение qi,  определено и равно qj тогда и только тогда, когда \Si = Sj , если \Si = , то значение qi,  не определено. Если функцию переходов автомата A(F) определить как *: QA*QA, то для qiQA, r  **qi, r = qj тогда и только тогда, когда r\Si = Sj. Заметим, что если r\Si = Sj и gPi, то grPj, и наоборот, если gPi и grPj, то r\Si = Sj

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

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

Доказательство. 1. Пусть слово r — суффикс обратного сверхслова gPj, т.е. g = g1r, и g1Pi. Тогда r\Si = Sj, т.е. *qi, r = qj. Таким образом, слово r представимо состоянием qj.

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

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

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

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

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

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

Формула F(t), с единственной свободной переменной t, называется k-ограниченной (k  Z), если для любого   Z значения формулы F( – k) на всех двусторонних сверхсловах, имеющих одинаковые -префиксы, совпадают. Смысл данного определения состоит в том, что при вычислении истинностного значения k-ограниченной формулы F(t) в позиции  интерпретации u не нужно рассматривать значения предикатов для t   + k. Примером 0-ограниченной формулы F(t) может служить формула t1(t1t)&y(t1)&t2((t1t2t)  x(t2)). Будем рассматривать 0-ограниченные формулы как способ задания множеств обратных сверхслов, а именно, будем полагать, что формула F(t) задает множество 0-префиксов всех тех двусторонних сверхслов, на которых истинна F(0). Заметим, что множества обратных сверхслов, задаваемые -формулой и ее отрицанием, конечно неразделимы. Таким образом, необходимым условием того, что автомат, специфицируемый формулой F, не обладает конечной памятью, является наличие в ней -подформул. Однако наличие в спецификации -подформулы не всегда приводит к тому, что специфицируемый автомат не обладает конечной памятью. Ниже покажем, что любую спецификацию tF(t) в языке L* за счет введения дополнительных предикатных символов можно преобразовать в спецификацию tFz(t) в этом же языке, специфицирующую автомат с конечной памятью.

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

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

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

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

Утверждение 4. Всякая модель для формулы F = t(z(t)  (t)), где z — предикатный символ, не содержащийся в (t), является моделью для формулы F1 = t(z(t)  (z(t 1)&h(t) g(t))).

Доказательство. Пусть u — модель для формулы F, тогда в любой позиции   Z интерпретации u значения z() и () совпадают. Из этого следует, что формулы t(z(t)  ((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)  i(t)) является моделью для формулы fz = tfz(t)(zi(t)  (zi(t – 1)&hi(t) gi(t))), где hi(t) и gi(t) определяются 1-развертками соответствующих формул i(t).

Пусть g — 0-префикс модели для формулы Fz = tFz(t) = tfz(t)(zi(t)  i(t)) и 1-развертки для формул i(t) имеют соответственно вид i(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, т.е. что в любой его позиции  истинна формула Fz(t). Доказательство проведем индукцией по длине префикса сверхслова l, соответствующего позиции  этого сверхслова. Базис:  = 0. Префикс нулевой длины соответствует самой правой позиции обратного сверхслова g. Поэтому значения f(t) и Fz(t) в этой позиции совпадают. Покажем теперь, что из совпадения значений f(t) и Fz(t) в позиции  следует совпадение их значений в позиции  + 1. Для этого достаточно показать, что zi( + 1) = i( + 1) для всех i = 1, 2, …, n. Из истинности Fz(t) в позиции  следует, что zi() = i() (i = 1, 2, …, n), поэтому из i( + 1) = (i()&hi( + 1) gi( + 1)) и zi( + 1) = (zi()&hi( + 1) gi( + 1)) следует, что zi( + 1) = i( + 1) (i = 1, 2, …, n). Таким образом, значения f(t) и Fz(t) в позиции  + 1 совпадают.

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

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

Доказательство. Из утверждений 4 и 5 следует, что S(Fz)  S(fz), т.е. автомат, специфицируемый формулой Fz, является подавтоматом автомата, специфицируемого формулой fz. Поскольку fz — формула языка 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.

Поступила 14.02.2009



Добавить документ в свой блог или на сайт

Похожие:

С конечной памятью iconОгонь одной конечной жизни

С конечной памятью iconРеферат Тема: «Материалы с памятью формы»

С конечной памятью iconСпектры непериодических сигналов
Любой физически реализуемый сигнал ограничен во времени и обладает конечной энергией]

С конечной памятью iconПластипруф
Обеспечивает пластичность раствора без добавления избыточного количества воды, что ведет к увеличению конечной прочности

С конечной памятью iconТехническое описание
С буферной памятью и гальванической изоляцией каналов от шины питания компьютера, предназначеного для работы в пэвм типа

С конечной памятью iconДрайвер это совокупность программ (секций), предназначенная для управления...

С конечной памятью iconЛабораторная работа №3
...

С конечной памятью iconКомплект цветного видеодомофона "свободные руки" (с памятью)
Уведомление о посетителе и его фото отправляется через e-mail (одновременно до 10 адресов)

С конечной памятью iconБиография доктора Павлюк Е. А
Отец имел два диплома – архитектора и врача; был человеком с прекрасной памятью, также знал латынь

С конечной памятью iconМеталогический базис, ориентированный на моделирование и синтез аппаратуры
При этом в качестве первоисточников данных могут выступать только элементы с памятью, такие как

Вы можете разместить ссылку на наш сайт:
Школьные материалы


При копировании материала укажите ссылку © 2013
контакты
uchebilka.ru
Главная страница


<