ОБ ОДНОМ СПОСОБЕ СПЕЦИФИКАЦИИ РЕАКТИВНЫХ АЛГОРИТМОВ В ЛОГИЧЕСКОМ ЯЗЫКЕ ПЕРВОГО ПОРЯДКА
Институт кибернетики им. НАН Украины
03187, Киев-187, проспект Академика Глушкова, 40
т. (044) 266-10-45
e-mail: *****@***yb.
Предложен способ спецификации реактивных алгоритмов в логическом языке первого порядка с одноместными предикатами. Предполагается, что спецификация предназначена для синтеза процедурного представления алгоритма, поэтому средства языка ограничены таким образом, чтобы добиться максимального упрощения процедуры синтеза управляющей части алгоритма при минимальном сокращении необходимых выразительных средств.
The way of reactive algorithms specification in a language of monadic first-order logic is proposed. We assume that the specification is aimed at the synthesis of the procedural representation of the algorithm. The language facilities are restricted so as to gain maximum simplification of the synthesis procedure for the control part of an algorithm while minimizing the reduction of required expressiveness.
Введение
Под реактивными алгоритмами здесь понимаются алгоритмы, которые выполняют пошаговые преобразования бесконечных последовательностей входных символов в бесконечные последовательности выходных символов. Обычно такие алгоритмы описывают поведение систем, постоянно взаимодействующих со своим окружением. Существует большое количество логических языков для спецификации реактивных алгоритмов (в частности распределенных). К ним, в первую очередь, относятся языки, основанные на различных темпоральных логиках, наибольшее распространение из которых получили PLTL (PTL) [1, 2], CTL* [3], и языки, основанные на логике одноместных предикатов первого или второго порядка [4, 5]. Эти языки в подавляющем большинстве случаев используются для верификации алгоритмов (программ). Известно [б, 7], что логическая спецификация может также служить исходной информацией для синтеза процедурного (императивного) представления алгоритма. Требования к языку, ориентированному на синтез, значительно отличаются от требований к языку, ориентированному на верификацию. В соответствии с этим различаются и свойства таких языков. Использование одного и того же логического языка как для верификации, так и для синтеза влечет за собой усложнение общей процедуры синтеза.
В настоящей работе предполагается, что логический язык используется для спецификации реактивных алгоритмов с целью их синтеза. В основе такого языка лежит логика первого порядка с одноместными предикатами, интерпретируемыми на множестве целых чисел. Определяется семантика языка, т. е. способ установления соответствия между формулами языка и классами специфицируемых объектов; а также выясняются ограничения, которые налагает предложенный способ спецификации на вид специфицируемых алгоритмов.
Декларативные языки спецификации реактивных алгоритмов (в частности логические языки) предназначены для описания свойств проектируемых алгоритмов или требований к их поведению. Обычно понятие свойства или поведения формализуется в виде множества последовательностей (конечных или бесконечных) над конечным алфавитом. Принято такие свойства разделять на два класса: свойства безопасности (safety) и свойства живости (liveness) [8]. Первые из них гарантируют, что некоторые нежелательные ситуации при работе алгоритма не возникнут. Примерами таких свойств могут служить взаимное исключение, отсутствие дедлоков и т. д. Вторые ‑ гарантируют наступление некоторого желательного события, например, завершение работы программы (для вычислительных алгоритмов), активизация некоторого процесса и т. д. Языки, ориентированные на верификацию, должны иметь средства для выражения как свойств безопасности, так и свойств живости; языки же, ориентированные на синтез, достаточно ограничить только средствами для выражения свойств безопасности, что, как будет показано ниже, может дать дополнительные возможности использования языка. Кроме того, при описании верифицируемых свойств алгоритма можно ограничиться некоторыми (представляющими наибольший интерес) свойствами, при построении спецификации для целей синтеза необходимо указать все существенные свойства, касающиеся поведения алгоритма.
Будем полагать, что алгоритм состоит из двух частей: управляющей и информационной, взаимодействующих между собой и с внешней средой. Управляющая часть определяет последовательность и временные соотношения между выполнениями отдельных действий (операций) алгоритма; в информационной части осуществляется преобразование данных. Говоря о логическом языке спецификации алгоритма, мы прежде всего имеем в виду описание его управляющей части и тех аспектов информационной части, которые связаны со взаимодействием этих двух частей. Поэтому в качестве математической модели как управляющей, так и информационной частей алгоритма будет рассматриваться конечный автомат. Таким образом, имеется в виду язык для спецификации поведения конечных автоматов. Основные требования к языку спецификации определяются объектом спецификации. Как правило, конкретная спецификация определяет не один объект, а класс объектов, которые считаются эквивалентными в соответствии с некоторым отношением эквивалентности, определенным на множестве специфицируемых объектов. Поэтому в следующем разделе будут рассмотрены основные понятия, связанные со специфицируемыми объектами, т. е. автоматами, и соответствующим отношением эквивалентности.
Объект спецификации
В основе рассматриваемого подхода к спецификации автомата лежит понятие сверхслова (бесконечного слова, ω-слова).
Сверхслова. Пусть Σ ‑ конечный алфавит, 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 и n ∈ Z определим n-префикс u(-∞, n) и n-суффикс u(n+1, +∞) соответственно как обратное сверхслово …u(n-2)u(n-1)u(n) и сверхслово u(n+1)u(n+2)…. Если значение n не существенно, то будем говорить об ω-префиксе и ω-суффиксе двустороннего сверхслова. Для n ∈ N+ n-префиксом сверхслова l называется слово l(1)…l(n) и n-суффиксом обратного сверхслова g — слово g(1-n)… g(0).
На множестве Σ* ∪ Σ-ω ∪ Σω определим обычным образом (частичную) операцию конкатенации «⋅», которую распространим также на множества слов и сверхслов. Пусть L1 ⊆ Σ*, L2 ⊆ Σ* ∪ Σω, тогда L1⋅L2 = {r⋅l ⎮ r ∈ L1, l ∈ L2}.
Множество Σω будем рассматривать как топологическое пространство с так называемой естественной топологией. Открытыми множествами в этой топологии являются все множества вида K⋅Σω, где K ⊆ Σ*. Дополнение открытого множества в Σω называется замкнутым множеством. Симметричным образом вводится топология на Σ-ω.
Автоматы.
Определение 1. Конечный X – Y-автомат A — это четверка X, Y, Q, δA>, где X, Y, Q — конечные множества соответственно входных и выходных символов и (внутренних) состояний, а δA: Q × X × Y→ 2Q — функция переходов автомата.
Автомат A, среди состояний которого выделено одно или несколько начальных состояний, называется инициальным; в противном случае автомат называется неинициальным. Одна из особенностей рассматриваемого подхода к спецификации автоматов состоит в том, что инициальный автомат A0 задается в виде пары (A, F0), где A — неинициальный автомат, а F0 — начальное условие, определяющее в нем некоторое непустое подмножество начальных состояний. На всех этапах синтеза, где автомат (класс автоматов) представляется в виде формулы языка спецификации, рассматривается первый элемент этой пары и только на заключительном этапе, когда будет построено множество состояний специфицируемого автомата, используется второй элемент пары. Это сделано для того, чтобы ограничить вид термов языка, исключив термы, не содержащие переменной, и тем самым упростить процедуры синтеза. Таким образом, в дальнейшем будем рассматривать только неинициальные автоматы.
Определение 2. X – Y-автомат A = X, Y, Q, δA> называется квазидетерминированным, если для любых q ∈ Q, x ∈ X, y ∈Y ⎪δA(q, x, y)⎪ ≤ 1.
Квазидетерминированные X – Y-автоматы удобно рассматривать как детерминированные частичные автоматы без выхода, с входным алфавитом Σ = X×Y. Такой автомат A = , Q, δA>, где δA: Q × Σ → Q — частичная функция переходов, будем называть Σ-автоматом.
Определение 3. Σ-автомат A = , Q, δA> называется циклическим, если для каждого q ∈ Q выполняются следующие условия:
1) существуют такие σ1 ∈ Σ и q1 ∈ Q, что q1 = δA(q, σ1),
2) существуют такие σ2 ∈ Σ и q2 ∈ Q, что q = δA(q2, σ2).
Автомат, для которого выполняется только первое из приведенных в определении условий, будем называть квазициклическим.
Очевидно, что любой автомат, определяющий поведение управляющей или информационной части реактивного алгоритма, может быть задан в виде пары (A, F0), где A — циклический автомат.
Циклический Σ-автомат может быть однозначно охарактеризован в терминах допустимых входных сверхслов.
Определение 4. Входное сверхслово (Σ-сверхслово) l = σ1σ2… допустимо в состоянии q автомата A, если существует такое сверхслово состояний q0q1q2…, где q0 = q, что для любого i = 0, 1, 2,… δA(qi, σi+1) = qi+1. Входное сверхслово l допустимо для автомата A, если оно допустимо хотя бы в одном из его состояний.
Пусть множество Q состояний автомата A равно {q1, …, qn}. Семейство множеств Σ-сверхслов (
, … …, 
), где 
— множество всех сверхслов, допустимых в состоянии qi (i = 1, 2, …, n), назовем поведением (неинициального) автомата A.
Определение 5. Два автомата A1 и A2 с поведениями соответственно (
, …, 
) и (
, …, 
) называются (строго) эквивалентными, если каждое 
(i = 1, …, n) содержится среди
, …, 
и каждое 
(j = 1, …, m) содержится среди 
, …, 
.
Определеная таким образом эквивалентность детерминированных Σ-автоматов (как инициальных, так и неинициальных) достаточна для различения довольно тонких свойств их поведения, неразличимых при характеризации поведения автоматов множествами допустимых для них сверхслов.
Пусть (
, …, 
) — семейство множеств сверхслов в алфавите Σ. Рассмотрим необходимые и достаточные условия того, чтобы это семейство было поведением некоторого Σ-автомата с n состояниями.
Определение 6. Пусть L ⊆ Σω и r ∈ Σ*. Левым частным множества сверхслов L по слову r (обозначается r\L ) назыеается множество всех таких сверхслов l, что r⋅l ∈ L, т. е. r\L = {l ⎮ r⋅l ∈L}.
Утверждение 1. Семейство (
, …, 
) множеств Σ-сверхслов является поведением неинициального Σ-автомата с n состояниями тогда и только тогда, когда оно удовлетворяет следующим двум условиям:
1) для каждого i = 1, …, n и каждого σ ∈ Σ σ\Si либо совпадает с некоторым Sj (j ∈ {1, …, n}), либо пусто;
2) каждое Si (i = 1, …, n) замкнуто в естественной топологии.
Доказательство этого утверждения приведено в [9].
Язык спецификации
Мы не будем подробно описывать синтаксис языка спецификации, а только охарактеризуем лежащую в его основе логику предикатов первого порядка в пределах, достаточных для описания семантики формул. Более подробно с языком спецификации и методами синтеза можно познакомиться в [10]. Итак, рассматриваемый язык представляет собой фрагмент логики предикатов первого порядка с одноместными переменными предикатами и фиксированной областью интерпретации, в качестве которой выступает множество Z целых чисел с отношением линейного порядка.
Алфавит языка состоит из следующих символов:
а) символ предметной константы 0, интерпретируемый как целое число 0;
б) множество предметных переменных Var = {t, t1, t2, …}, определяемое конкретной спецификацией;
в) сигнатура одноместных предикатных символов Ω = {p1, …, pq} также определяется спецификацией;
г) двуместный предикатный символ « ≤ », интерпретируемый как отношение линейного порядка на множестве целых чисел;
д) два унарных функциональных символа +1 и -1, интерпретируемых соответственно как прибавление и вычитание единицы;
е) логические связки &, ∨, ¬, кванторы ∀, ∃ и скобки (, ).
Множество T термов состоит из двух непересекающихся подмножеств T0 = Z (константные термы) и T1 = {(ti + k)⎮ti ∈ Var, k ∈ Z}, где + — операция сложения целых чисел.
Формулы, используемые для спецификации неинициального автомата, имеют вид ∀tF(t), где F(t) — формула с одной свободной переменной, построенная с помощью логических связок и кванторов из атомарных формул вида pi(τj) и τi ≤ τj (pi ∈ Ω, τi, τj ∈ T1). Термы из T0 используются только в формулах, задающих начальные условия. В дальнейшем речь будет идти лишь о формулах, специфицирующих поведение неинициального автомата.
Каждой замкнутой формуле F = ∀tF(t) ставится в соответствие множество моделей для этой формулы, т. е. множество всех интерпретаций, на которых F истинна. Напомним, что в рассматриваемом языке не интерпретированы только одноместные предикатные символы. Пусть Ω = p1, …, pq> — упорядоченное множество всех одноместных предикатных символов, встречающихся в формуле F (сигнатура формулы F). Интерпретация формулы F задает упорядоченный набор 1, …, πq> определенных на Z одноместных предикатов, соответствующих предикатным символам из Ω. Пусть Σ — множество всех двоичных векторов длины q, тогда интерпретацию I = 1, …, πq> можно представить в виде двустороннего сверхслова в алфавите Σ, а множество всех моделей для F — в виде множества MF двусторонних сверхслов в этом алфавите. В дальнейшем мы не будем различать интерпретации для формулы F и соответствующие им двусторонние сверхслова и будем говорить об истинности или ложности F на двустороннем сверхслове.
Каждому u ∈ MF поставим в соответствие множество сверхслов Su = {l ∈ Σω ⎮ u(-∞, 0)⋅l ∈ MF}. Другими словами, Su состоит из всех тех сверхслов, конкатенация каждого из которых с 0-префиксом двустороннего сверхслова u соответствует модели для F. Таким образом получим совокупность множеств сверхслов ℜF = {Su ⎮ u ∈ MF}.
Основная идея, позволяющая использовать формулу F для спецификации автомата, состоит в том, что совокупность множеств сверхслов ℜF рассматривается как поведение некоторого Σ-автомата. При этом предполагается, что входной алфавит автомата представляет собой множество двоичных векторов длины q, где q — количество одноместных предикатных символов, встречающихся в формуле F. Это означает, что специфицируемый X – Y-автомат имеет структурные вход и выход, представленные соответствующим множеством двоичных каналов, и каждому такому каналу соответствует предикатный символ из сигнатуры формулы F. Непустое множество ℜF определяет поведение некоторого Σ-автомата только в том случае, если оно конечно и удовлетворяет условиям утверждения 1. Не для всякой формулы F = ∀tF(t) ℜF обладает указанными свойствами, а значит, не каждая такая формула специфицирует конечный автомат. Рассмотрим, например, формулу F = ∀t∃t1(t ≤ t1) & x(t1). Здесь Σ = {0, 1}, поскольку в формуле имеется всего один предикатный символ. Совокупность множеств Σ-сверхслов ℜF состоит из одного множества сверхслов, не имеющих ω-суффикса 000…. Это множество не замкнуто, в силу чего не может быть поведением никакого конечного автомата. Однако при некоторых ограничениях на класс рассматриваемых формул совокупность множеств сверхслов, ассоциируемая с формулой F, удовлетворяет сформулированным выше требованиям.
Определение 7. Замкнутая формула F фиктивна в интервале (k, +∞), если на любых двусторонних сверхсловах, k-префиксы которых совпадают, она либо одновременно истинна, либо одновременно ложна.
Определение 8. Формула F(t), с единственной свободной переменной t, называется k-ограниченной (k ∈ Z), если для любого τ ∈ Z F(t) фиктивна в интервале (τ + k, +∞).
Смысл последнего определения состоит в том, что при вычислении истинностного значения k-ограниченной формулы F(t) для любой интерпретации (u, τ), где u — интерпретация одноместных предикатных символов, а τ — значение переменной t, не нужно рассматривать значения предикатов для t > τ + k. Примером 0-ограниченной формулы F(t) может служить формула ∃t1(t1 ≤ t) & y(t1) & ∀t2((t1 t2 ≤ t) → ¬x(t2)). Формула y(t + 1)→ ¬x(t+3) 3-ограниченная, а формула ∃t1(t ≤ t1) & y(t1) ни для какого k ∈ Z не является k-ограниченной. В [9] доказано следующее утверждение.
Утверждение 2. Всякая непротиворечивая формула вида ∀tF(t), где F(t) — k-ограниченная формула, задает поведение конечного неинициального Σ-автомата.
Заметим, что с помощью k-ограниченных формул можно специфицировать только свойства безопасности. Таким образом, отказ от возможности специфицировать свойства живости — что для языка, ориентированного на синтез, вполне естественно, — а также использование в качестве области интерпретации формул множества целых чисел (а не натуральных) позволили специфицировать неинициальный автомат с точностью до (строгой) эквивалентности.
Определение 9. Неинициальный автомат A с поведением (
, …, 
) удовлетворяет формуле F, если каждое Si (i = 1, …, n) содержится в ℜF и для каждого Su ∈ ℜF найдется совпадающее с ним Si (i ∈ {1, …, n}).
Будем говорить, что формула F специфицирует класс всех автоматов, удовлетворяющих F. Как следует из определения 9, все автоматы удовлетворяющие F, попарно эквивалентны, а совокупность множеств сверхслов ℜF соответствует поведению приведенного автомата из этого класса эквивалентности.
Рассмотрим, какие ограничения предложенный способ спецификации налагает на класс специфицируемых алгоритмов. Непосредственно из способа построения совокупности множеств ℜF вытекает справедливость следующих утверждений.
1. Каждый ω-префикс любой модели для F однозначно определяет состояние специфицируемого автомата.
2. Для каждого ω-префикса g двустороннего сверхслова из MF существуют такие σ1 и σ2 ∈ Σ, что g = g1⋅σ1 и g⋅σ2 — ω-префикс некоторой модели для F.
Из первого утверждения следует, что всякий специфицируемый автомат — циклический, а из второго, — что специфицируемый Σ-автомат — детерминированный. Напомним, что детерминированному Σ-автомату может соответствовать недетерминированный (квазидетерминированный) X – Y-автомат.
Очевидно, что автомат, используемый в качестве модели управляющей части реактивного алгоритма, должен быть квазициклическим. Поскольку полная спецификация автомата включает в себя начальное условие, то цикличность неинициального автомата не налагает ограничений на класс специфицируемых инициальных автоматов.
Еще одно ограничение на класс специфицируемых автоматов связано с использованием языка первого порядка. Известно, что не любое множество сверхслов, допустимых конечным автоматом, может быть задано с помощью формулы языка первого порядка. Так, множество всех сверхслов в алфавите {a, b}, в которых между любыми двумя (последовательными) символами a имеется четное количество символов b, не может быть задано формулой первого порядка. Заметим, что здесь речь идет о формуле первого порядка, сигнатура одноместных предикатных символов которой состоит из двух символов a и b. Любая формула второго порядка, задающая это множество сверхслов, содержит подформулу, постулирующую существование предиката, различающего четное и нечетное количество последовательных символов b. Введя дополнительный символ для обозначения этого предиката и определив его подходящим образом, указанное множество сверхслов можно специфицировать в языке первого порядка, например, такой формулой:
∀t(a(t) → z(t) & ∀t1(((t1 ≤ t-1) & a(t1) & ∀t2((t1+1 ≤ t2 ≤ t-1) → b(t2))) → z(t1+1) &
& ∀t3((t1+1 ≤ t3 ≤ t) → (z(t3) ↔ ¬z(t3-1)))))&(a(t) ↔ ¬b(t)).
Здесь предикат z определен так, что на отрезке сверхслова, состоящем из символов b, его истинностные значения чередуются. Аналогичным образом, т. е. вводя дополнительные предикатные символы, любое множество сверхслов, специфицируемое в языке второго порядка, можно специфицировать в языке первого порядка.
Таким образом, при использовании спецификации для целей синтеза алгоритма, ограниченность выразительных возможностей языка первого порядка оказывается несущественной.
Заключение
Язык спецификации исходных данных, используемых для синтеза реактивных алгоритмов, должен строиться на основе компромиса между богатством его выразительных возможностей и сложностью процедур синтеза. Ограничение выразительных возможностей языка средствами первого порядка, а также ограничение класса используемых формул формулами вида ∀tF(t), где F(t) — 0-ограниченная формула, позволили построить достаточно эффективные процедуры синтеза [10], по сути не сокращая класса специфицируемых автоматов. Использование в качестве области интерпретации множества целых чисел также упростило процедуры синтеза, поскольку в этом случае формулы инвариантны относительно “сдвига”, т. е. формула ∀tF(t) равносильна формуле ∀tF(t+k) для любого k ∈ Z; кроме того, это позволило специфицировать автоматы с точностью до эквивилентности, когда поведение автомата определяется не множеством сверхслов, что соответствует слабой эквивалентности автоматов, а совокупностью множеств сверхслов.
