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

Ранее в работе [1] авторами были подробно рассмотрены инструменты и средства унифицированного представления формул логик LTL и CTL в виде систем рекурсивных уравнений. Было показано, что RTL-нотация является до- статочно выразительной, чтобы с ее помощью задавать и модели систем, и верифицирующие их свойства (на базе логики как линейного времени, так и ветвящегося). Данная статья логически развивает эту тему и посвящена решению естественно возникшей проблемы, касающейся процесса верификации моделей систем, или Model Cheсking [2, 3], относительно свойств логики ветвящегося времени, заданных на базе RTL.

За счет небольших (по сравнению с [1]) изменений в синтаксисе, существенно упростивших восприятие RTL-формул, а также введения ряда аксиом авторам удалось сформировать весьма понятный и наглядный алгоритм верификации, который основан на таком стандартном и всем известном методе, как метод построения синхронной композиции. Разработанный алгоритм подробно описывается в статье, а его работа (для самопроверки) наглядно демонстрируется на нескольких доступных и известных примерах, взятых из работы [2]. Так, забегая вперед, можно сказать, что, помимо теоретической обоснованности алгоритма, на практике удалось проверить и подтвердить его работоспособность, получив аналогичные результаты верификации. В то же время нужно отметить, что в данной статье авторами не исследовалась возможность верификации больших распределенных программных систем. В основном речь идет о создании инструмента унифицированного представления формул логик LTL и CTL и использовании его для верификации моделей систем.

RTL-нотация

В основе RTL-нотации лежат семантические определения временных логик LTL и CTL [4–7] и системы рекурсивных уравнений [8]. Для упрощения задания в RTL семантических значений кванторов CTL расширим семантическое определение оператора продолжения по сравнению с тем, как это сделано в [9]. Оператор продолжения «∘», как и ранее, выступает в качестве связующего звена (перехода) между текущим состоянием и следующим. Для задания моделей систем это будет его единственным назначением. Для верифицируемого CTL-свойства оператор продолжения необходимо наделить возможностью характеризовать как квантор существования E, так и квантор всеобщности A. В связи с этим примем следующие обозначения:

«∘» – применяется как для моделей систем, так и для верифицируемых свойств (для моделей систем задает и описывает переходы состояний, а для верифицируемых свойств гарантирует проверку выполнимости хотя бы для одной из ветвей);

«•» – применяется только для верифицируемых свойств и гарантирует проверку выполнимости по всем ветвям.

Данное расширение оператора продолжения является по сути единственным необходимым изменением (по сравнению с [1]), которое дает нотации возможность формулировать выражения логики CTL. В таблице 1 приведены рекурсивные представления базовых операторов CTL в RTL-нотации с учетом использования операторов продолжения, соответствующих различным кванторам. Если формулы LTL задают лишь некоторый порядок наступления каких-либо событий в целом, то формулы CTL эти события соотносят с альтернативными путями развития вычислительного процесса. Это требуется, когда верифицируемая система пе- реходит в различные режимы работы (в зави- симости от исходных данных или условий), работает в многопоточном режиме [10] или результаты ее работы носят вероятностный характер [11].

Таблица 1

Рекурсивные представления операторов CTL в RTL-нотации

Table 1

Recursive representations of CTL statements in RTL notation

CTL	RTL
AXφ	∆ • φ
EXφ	∆ ∘ φ
AFφ = φ ∨ AX AFφ	F = φ + ∆ • F
EFφ = φ ∨ EX EFφ	F = φ + ∆ ∘ F
AGφ = φ ∧ AX AGφ	F = φ • F
EGφ = φ ∧ EX EGφ	F = φ ∘ F
A(φ1Uφ2) = φ2 ∨ φ1 ∧ AX A(φ1Uφ2)	F = φ2 + φ1 • F
E(φ1Uφ2) = φ2 ∨ φ1 ∧ EX E(φ1Uφ2)	F = φ2 + φ1 ∘ F

Аксиомы RTL:

A1.      ˥Fγ = G˥γ,

A2.      ˥Gγ = F˥γ,

A3.      ˥Aγ = E˥γ,

A4.      ˥Eγ = A˥γ,

A5.      ˥∆ = ∆,

A6.      ∆⍵ ∘ γ = ∆⍵,

A7.      ∆⍵ = ∆ ∘ ∆⍵,

A8.      γ1 + γ2 = γ2 + γ1,

A9.      γ + γ = γ,

A10.   (γ1 + γ2) + γ3 = γ1 + (γ2 + γ3),

A11.   γ1 ∘ (γ2 ∘ γ3) = (γ1 ∘ γ2) ∘ γ3,

A12.   (γ1 + γ2) ∘ γ3 = γ1 ∘ γ3 + γ2 ∘ γ3,

A13.   γ1 ∘ (γ2 + γ3) = γ1 ∘ γ2 + γ1 ∘ γ3,

A14.   γ1 • (γ2 + γ3) = γ1 • γ2 + γ1 • γ3.

Сформулируем основные аксиомы, необходимые для построения синхронной композиции двух систем рекурсивных уравнений:

S1. φ1 ⊗ φ2 = φ1, если φ1 ⊆ φ2,

                φ2, если φ2 ⊆ φ1,

⊥ в противном случае.

S2. φ ⊗ ⊥ = ⊥,

S3. μ ∘ ⊥ = ⊥∘ μ = ⊥,

S4. φ ⊗ ∆ = φ,

S5. (φ1 ∘ μ1) ⊗ (φ2 ∘ μ2) = (φ1 ⊗ φ2) ∘ (μ1 ⊗ μ2),

S6. (φ1 ∘ μ1 + φ2 ∘ μ2) ⊗ (φ3 • μ3) = {(φ1⊗φ3) ∘ (μ1⊗μ3), (φ2⊗φ3) ∘ (μ2⊗μ3)},

S7. (φ1 ∘ μ1 + φ2 ∘ μ2) ⊗ (φ3 ∘ μ3) = (φ1⊗φ3) ∘ (μ1⊗μ3) + (φ2⊗φ3) ∘ (μ2⊗μ3),

S8. {φ1 ∘ μ1, φ1 ∘ μ2} = φ1 ∘ {μ1, μ2},

S9. {μ1, μ2} = {μ2, μ1},

S10. {μ, ⊥} = ⊥,

S11.    (φ1 ∘ μ1) ⊗ (φ2 ∘ (μ2 + μ3)) = (φ1⊗φ2) ∘ (μ1⊗μ2 + μ1⊗μ3),

S12. (φ1 ∘ μ1) ⊗ (φ2 • (μ2 + μ3)) = (φ1⊗φ2) ∘ (μ1⊗μ2 + μ1⊗μ3),

S13. {μ1, μ2 + μ3} = {μ1, μ2} + {μ1, μ3},

S14.    ∆ ∘ ⊥ = ⊥.

В записи вида {μ1, μ2} фигурные скобки означают связанное продолжение, что эквивалентно выполнению формулы μ1 & μ2, то есть связанное продолжение выполняется тогда и только тогда, когда выполняется каждое продолжение, входящее в его состав.

Верификация CTL-свойств с помощью RTL

Поскольку верификация LTL-свойств была подробно рассмотрена в работе [9], данная статья посвящена лишь верификации CTL-свойств, заданных с помощью RTL-нотации. Применение предложенного метода наглядно и всесторонне демонстрируется на типовых примерах задания верифицируемых свойств для систем небольших размеров, что является стандартным и общепринятым способом иллюстрации возможностей метода.

С помощью вышеописанных аксиом на базе RTL рассмотрим пример, представленный в [1] (см. рисунок).

В RTL-нотации данная модель M примет следующий вид:

S0 = {} ∘ (S1 + S3),

S1 = p ∘ S4,

S2 = p ∘ (S1 + S3),

S3 = p ∘ (S0 + S5),

S4 = {p, q} ∘ (S0 + S3 + S5),

S5 = {p, r} ∘ S2.

В качестве верифицируемого свойства используем CTL-свойство Φ = E((EX⌉p) U AF(q ∨ r)).

Выполним преобразование свойства Φ к RTL-виду:

Φ0 = E(Φ1 U Φ2) = Φ2 + Φ1 ∘ Φ0,

Φ1 = EX⌉p = △ ∘ ⌉p,

Φ2 = AF(q ∨ r) = (q + r) + △ • Φ2

⇔

Φ0 = (q + r) + △ • Φ2 + △ ∘ ⌉p ∘ Φ0

⇔

F0 = (q + r) + △ • F1 + △ ∘ F2,

F1 = (q + r) + △ • F1,

F2 = ⌉p ∘ F0.

Введем еще одно состояние, чтобы модель верифицирующего свойства описывала реагирующую систему, которое и станет допускающим состоянием (выделено жирным шрифтом):

F0 = (q + r) • F3 + △ • F1 + △ ∘ F2,

F1 = (q + r) • F3 + △ • F1,

F2 = ⌉p ∘ F0,

F3 = △ ∘ F3.

Переход в состояние F3 задан оператором «•», то есть должен выполняться для всех путей, поскольку данное состояние наступает только после выполнения AF(q ∨ r). Иными словами, только если все переходы состояния модели помечены q или r, можно выполнить переход в F3.

Правило выполнимости формулы Φ на модели M: Φ выполняется на M тогда и только тогда, когда из начального состояния синхронной композиции M⊗Φ существует хотя бы одна нетерминальная ветвь, ведущая в одно из ее допускающих состояний.

Выполним построение синхронной композиции M⊗Φ.

В дальнейшем для краткости будем обозначать синхронную композицию (Si⊗Fj) через Ci,j. Допускающими состояниями композиции являются состояния, которые содержат допускающие состояния верифицирующего свойства (выделено жирным шрифтом). Поскольку попадание в состояние Ci,3 (i = 0¸5) порождает лишь переходы в состояния Cj,3 (j = 0¸5), все соответствующие уравнения могут быть сразу же заменены на одно Ce = △ ∘Ce и при появлении в правой части уравнений состояний Ci,3 их можно сразу заменять на Ce. Получим следующую цепочку равенств:

С0,0 = S0⊗F0 =

[{} ∘ (S1 + S3)] ⊗ [(q + r) • F3 + △ • F1 + △ ∘ F2] =

{} ∘ (S1 + S3)] ⊗ [(q + r) • F3] + [{} ∘ (S1 + S3)] ⊗ [△ • F1] + [{} ∘ (S1 + S3)] ⊗ [△ ∘ F2] =

[⊥ ∘ {S1⊗F3, S3⊗F3}] + [{} ⊗ △ ∘ {S1⊗F1, S3⊗F1}] + [{} ⊗ △ ∘ (S1⊗F2 + S3⊗F2)] =

{} ∘ {C1,1, C3,1} + {} ∘ (C1,2 + C3,2),

C1,1 = S1⊗F1 =

[p ∘ S4] ⊗ [(q + r) • F3 + △ • F1] =

[p ∘ S4] ⊗ [(q + r) • F3] + [p ∘ S4] ⊗ [△ • F1] =

[⊥ ∘ S4⊗F3] + [p ⊗ △∘ S4⊗F1] = p ∘ {C4,1},

C3,1 = S3⊗F1 =

[p ∘ (S0 + S5)] ⊗ [(q + r) • F3 + △ • F1] =

[p ∘ (S0 + S5)] ⊗ [(q + r) • F3] + [p ∘ (S0 + S5)] ⊗ [△ • F1] = [⊥ ∘ {S0⊗F3, S5⊗F3}] +

[p ∘ {S0⊗F1, S5⊗F1}] = p ∘ {C0,1, C5,1},

C1,2 = S1⊗F2 = [p ∘ S4] ⊗ [⌉p ∘ F1] = ⊥,

C3,2 = S3⊗F2 = [p ∘ (S0 + S5)] ⊗ [⌉p ∘ F1] = ⊥,

C4,1 = S4⊗F1 =

[{p, q} ∘ (S0 + S3 + S5)] ⊗ [(q + r) • F3 + △ • F1] =

[{p, q} ∘ (S0 + S3 + S5)] ⊗ [(q + r) • F3] + [{p, q} ∘ (S0 + S3 + S5)] ⊗ [△ • F1] =

[q ∘ {S0⊗F3, S3⊗F3, S5⊗F3}] + [{p, q} ∘ {S0⊗F1, S3⊗F1, S5⊗F1}] =

q ∘ {C0,3, C3,3, C5,3} + {p, q} ∘ {C0,1, C3,1, C5,1} =

q ∘ {Ce} + {p, q} ∘ {C0,1, C3,1, C5,1},

C0,1 = S0⊗F1 =

[{} ∘ (S1 + S3)] ⊗ [(q + r) • F3 + △ • F1] =

[{} ∘ (S1 + S3)] ⊗ [(q + r) • F3] + [{} ∘ (S1 + S3)] ⊗ [△ • F1] =

[⊥ ∘ {S1⊗F3, S3⊗F3}] + [{} ∘ {S1⊗F1, S3⊗F1}] =

{} ∘ {C1,1, C3,1},

C5,1 = S5⊗F1 =

[{p, r} ∘ S2] ⊗ [(q + r) • F3 + △ • F1] =

[{p, r} ∘ S2] ⊗ [(q + r) • F3] + [{p, r} ∘ S2] ⊗ [△ • F1] =

[r ∘ S2⊗F3] + [{p, r} ∘ S2⊗F1] =

r ∘ C2,3 + {p, r} ∘ C2,1 = r ∘ Ce + {p, r} ∘ C2,1,

C2,1 = S2⊗F1 =

[p ∘ (S1 + S3)] ⊗ [(q + r) • F3 + △ • F1] =

[p ∘ (S1 + S3)] ⊗ [(q + r) • F3] + [p ∘ (S1 + S3)] ⊗ [△ • F1] =

[⊥ ∘ {S1⊗F3, S3⊗F3}] + [p ∘ {S1⊗F1, S3⊗F1}] =

p ∘ {C1,1, C3,1},

Ce = △ ∘ Ce.

После исключения из композиции терминальных ветвей, ведущих в состояния C12 и C32, синхронная композиция примет вид

С0,0 = {} ∘ {C1,1, C3,1},

C1,1 = p ∘ {C4,1},

C3,1 = p ∘ {C0,1, C5,1},

C4,,1 = q ∘ Ce + {p, q} ∘ {C0,1, C3,1, C5,1},

C0,1 = {} ∘ {C1,1, C3,1},

C5,1 = r ∘ Ce + {p, r} ∘ C2,1,

C2,1 = p ∘ {C1,1, C3,1},

Ce = △ ∘ Ce.

Алгоритм маркировки состояний синхронной композиции

С помощью алгоритма маркировки состояний проверим выполнимость Φ на M.

Шаг 1. Пометим маркером F все допускаю- щие состояния композиции: F: Ce.

Шаг 2. Далее в цикле будем добавлять к ним те состояния, из которых есть переходы в уже помеченные состояния:

F: Ce, C4,1, C5,1, так как в Ce есть переходы из C4,1, C5,1;

F: Ce, C4,1, C5,1, С1,1, так как из С1,1 есть переход в уже помеченное состояние C4,1.

Больше никакие состояния не могут быть помечены. В частности, состояние C3,1 нельзя отметить маркером F, поскольку оно содержит связанное продолжение {C0,1, C5,1}, а С0,1 не было отмечено F.

Так как начальное состояние С0,0 не было помечено F, допускающее состояние из него недостижимо. А это означает невыполнение Φ на M, что совпадает с результатами, представленными в работе [2].

Проверка альтернативного свойства

Для этого же примера проверим выполнимость другого свойства Φ' = E((EX⌉p) U EF(q ∨ ∨ r)), которое, согласно представленному в работе [2] алгоритму верификации, будет выполняться на модели M.

Преобразуем свойство Φ' к RTL-виду:

Φ'0 = E(Φ'1 U Φ'2) = Φ'2 + Φ'1 ∘ Φ'0,

Φ'1 = EX⌉p = △ ∘ ⌉p,

Φ'2 = EF(q ∨ r) = (q + r) + △ ∘ Φ'2

⇔

Φ'0 = [(q + r) + △ ∘ Φ'2] + △ ∘ ⌉p ∘ Φ'0

⇔

F0 = [(q + r) + △ ∘ F1] + △ ∘ F2,

F1 = (q + r) + △ ∘ F1,

F2 = ⌉p ∘ F0.

Чтобы модель верифицирующего свойства описывала реагирующую систему, введем еще одно состояние, которое и станет допускающим (выделено жирным шрифтом):

F0 = (q + r) ∘ F3 + △ ∘ (F1 + F2),

F1 = (q + r) ∘ F3 + △ ∘ F1,

F2 = ⌉p ∘ F0,

F3 = △ ∘ F3.

Поскольку F3 наступает только после выполнения EF(q ∨ r), переход в это состояние задается оператором «∘». Необходимо, чтобы хотя бы один переход состояния модели был помечен q или r.

Выполним построение синхронной композиции M⊗Φ'.

В дальнейшем для краткости будем обозначать синхронную композицию (Si⊗Fj) через Cij, а (Si⊗F3) через Ce:

С0,0 = {} ∘ (C1,1 + C3,1),

C1,1 = p ∘ C4,1,

C3,1 = p ∘ (C0,1 + C5,1),

C4,1 = q ∘ Ce + {p, q} ∘ (C0,1 + C3,1 + C5,1),

C0,1 = {} ∘ (C1,1 + C3,1),

C5,1 = r ∘ Ce + {p, r} ∘ C2,1,

C2,1 = p ∘ (C1,1 + C3,1),

Ce = △ ∘ Ce.

Рассмотрим по шагам работу алгоритма маркировки:

1.    F: Ce,

2.    F: Ce, C4,1, C5,1,

3.    F: Ce, C4,1, C5,1, C1,1, C3,1,

4.    F: Ce, C4,1, C5,1, C1,1, C3,1, С0,0, C0,1, С2,1.

Состояние С0,0 входит во множество помеченных F, следовательно, Φ' выполняется на M, что совпадает с результатами, которые можно получить, используя алгоритм проверки, приведенный в работе [2].

Задача о козе, капусте и волке

Условия задачи. Лодочнику необходимо перевезти с левого берега на правый трех пассажиров: волка, козу и капусту. В любой момент времени лодочник может перевозить только одного пассажира. Главным условием задачи является то, что лодочнику нельзя оставлять без присмотра козу с капустой и волка с козой на любом из берегов, поскольку капуста и коза могут быть съедены.

Решение. Введем следующие обозначения: b – лодочник (boatman), w – волк (wolf), g – коза (goat) и c – капуста (cabbage). Запись вида ⌉x будет означать нахождение соответствующего субъекта на левом берегу, а запись x – на правом берегу, где x ∈ {b, w, g, c}. Таким образом, возможны 16 различных состояний.

Начальным состоянием S0 является состояние {⌉b, ⌉g, ⌉w, ⌉c}, когда все находятся на левом берегу, а заключительным состоянием S15 – {b, g, w, c}, когда все находятся на правом берегу.

Вначале на базе RTL-нотации построим модель Μ, описывающую все возможные варианты развития событий для поставленной задачи, включая те, которые противоречат ее главному условию. При появлении новых состояний будем записывать их в левой колонке:

S0 = {} ◦ S1,

{⌉b, ⌉g, ⌉w, ⌉c}:       S1 = {b, g} ◦ S2 + {b, w} ◦ S3 + {b, c} ◦ S4 + {b} ◦ S5,

{b, g, ⌉w, ⌉c}:    S2 = {g} ◦ S6 + {} ◦ S1,

{b, ⌉g, w, ⌉c}:    S3 = {w} ◦ S7 + {} ◦ S1,

{b, ⌉g, ⌉w, c}:    S4 = {c} ◦ S8 + {} ◦ S1,

{b, ⌉g, ⌉w, ⌉c}:   S5 = {} ◦ S1,

{⌉b, g, ⌉w, ⌉c}:       S6 = {b, g, w} ◦ S9 + {b, g, c} ◦ S10 + {b, g} ◦ S2,

{⌉b, ⌉g, w, ⌉c}:       S7 = {b, g, w} ◦ S9 + {b, w, c} ◦ S11 + {b, w} ◦ S3,

{⌉b, ⌉g, ⌉w, c}:       S8 = {b, g, c} ◦ S10 + {b, w, c} ◦ S11 + {b, c} ◦ S4,

{b, g, w, ⌉c}:     S9 = {w} ◦ S7 + {g} ◦ S6 + {g, w} ◦ S12,

{b, g, ⌉w, c}:     S10 = {c} ◦ S8 + {g} ◦ S6 + {g, c} ◦ S13,

{b, ⌉g, w, c}:     S11 = {c} ◦ S8 + {w} ◦ S7 + {w, c} ◦ S14,

{⌉b, g, w, ⌉c}:    S12 = {b, g, w, c} ◦ S15 + {b, g, w} ◦ S9,

{⌉b, g, ⌉w, c}:    S13 = {b, g, w, c} ◦ S15 + {b, g, c} ◦ S10,

{⌉b, ⌉g, w, c}:    S14 = {b, g, w, c} ◦ S15 + {b, w, c} ◦ S11,

{b,  g,  w,  c}:                    S15 = {w, c} ◦ S14 + {g, c} ◦ S13 + {g, w} ◦ S12 + {g, w, c} ◦ S16,

{⌉b, g, w, c}:     S16 = {b, g, w, c} ◦ S15.

Выполним проверку CTL-свойства Φ, целью которого является доказательство того, что задача не имеет решения:

Φ = A⌉[(g ≡ c ∨ g ≡ w) → (g ≡ b) U (b ∧ g ∧ w ∧ c)].

«Среди всех возможных путей не существует такого, на котором все переправятся на правый берег при условии, что, когда коза находится на одном берегу с капустой или волком, рядом с ней находится лодочник».

Преобразуем условие Φ, воспользовавшись следующим правилом: ⌉(φ1Uφ2) = ⌉φ1R⌉φ2,

Φ = A[(g ≡ c ∨ g ≡ w) ∧ ⌉(g ≡ b) R (⌉b ∨ ⌉g ∨ ⌉w ∨ ⌉c)].

Получим рекурсивное определение оператора R через оператор U:

⌉(φ1Uφ2) = ⌉(φ2 ∨ φ1 ∧ X(φ1Uφ2)) ≡

⌉(φ1Uφ2) = ⌉φ2 ∧ (⌉φ1 ∨ X⌉(φ1Uφ2)) ≡

⌉(φ1Uφ2) = ⌉φ2 ∧ ⌉φ1 ∨ ⌉φ2 ∧ X⌉(φ1Uφ2).

φ1Rφ2 = φ2 ∧ φ1 ∨ φ2 ∧ X(φ1Rφ2).

В RTL-нотации данный оператор задается следующим образом: F = {φ1, φ2} + φ2 ◦ F.

Выполним преобразование свойства Φ к RTL-виду:

Φ = A(α R β) = {α, β} + β • Φ0,

α = (g ≡ c ∨ g ≡ w) ∧ ⌉(g ≡ b) = (g ≡ c ∨ g ≡ w) ∧ (g ≡ ⌉b) = (g ≡ c ≡ ⌉b) + (g ≡ w ≡ ⌉b),

β = ⌉b + ⌉g + ⌉w + ⌉c.

Чтобы модель верифицирующего свойства описывала реагирующую систему, введем допускающее состояние F1 (выделено жирным шрифтом):

F0 = {α, β} • F1 + β • F0,

F1 = △ ◦ F1.

Переход в F1 задается оператором «•», поскольку свойство считается выполненным лишь при его выполнении по всем возможным путям.

Замечание. Такой же результат получим, если осуществим непосредственный переход от выражения ⌉(φ1Uφ2) к RTL-виду.

Выполним построение синхронной композиции M⊗Φ.

В дальнейшем для краткости будем обозначать синхронную композицию (Si⊗Fj) через Ci,j.

Допускающими состояниями композиции являются те, которые содержат допускающие состояния верифицирующего свойства. По- скольку попадание в состояние Ci,1 (i = 0¸5) по- рождает лишь переходы в состояния Cj,1 (j = 0¸5), все соответствующие уравнения могут быть сразу же заменены на одно уравнение Ce = △ ∘Ce и при появлении в правой части уравнений состояний Ci,1 их можно сразу заменять на Ce :

C0,0 = {} ◦ C1­,0,

C1,0 = {⊥ ◦ Ce, {b, w} ◦ Ce, {b, c} ◦ Ce, b ◦ Ce} + {{b, g} ◦ C2­,0, {b, w} ◦ C3,0, {b, c} ◦ C4,0, b ◦ C5,0},

C2,0 = {g ◦ C6,0, {} ◦ C1­,0},

C3,0 = {w ◦ C7,0, {} ◦ C1­,0},

C4,0 = {c ◦ C8,0, {} ◦ C1­,0},

C5,0 = {} ◦ C1,0,

C6,0 = {{b, g, w} ◦ C9,0, {b, g, c} ◦ C10,0,{b, g} ◦ C2,0},

C7,0 = {⊥ ◦ Ce, ⊥ ◦ Ce, {b, w} ◦ Ce} + {{b, g, w} ◦ C9,0, {b, w, c} ◦ C11,0, {b, w} ◦ C3,0},

C8,0 = {⊥ ◦ Ce, ⊥ ◦ Ce, {b, c} ◦ Ce} + {{b, g, c} ◦ C10,0, {b, w, c} ◦ C11,0, {b, c} ◦ C4,0},

C9,0 = {⊥ ◦ Ce, ⊥ ◦ Ce, {g, w} ◦ Ce} + {{w} ◦ C7,0, {g} ◦ C6,0, {g, w} ◦ C12,0},

C10,0 = {⊥ ◦ Ce, ⊥ ◦ Ce, {g, c} ◦ Ce} + {{c} ◦ C8,0, {g} ◦ C6,0, {g, c} ◦ C13,0},

C11,0 = {{c} ◦ C8,0, {w} ◦ C7,0, {w, c} ◦ C14,0},

C12,0 = {⊥ ◦ C15,0, {b, g, w} ◦ C9,0},

C13,0 = {⊥ ◦ C15,0, {b, g, c} ◦ C10,0},

C14,0 = {⊥ ◦ C15,0, {b, w, c} ◦ C11,0},

C15,0 = {⊥ ◦ Ce, {g, c} ◦ Ce, {g, w} ◦ Ce, {g, w, c} ◦ Ce} + {{w, c} ◦ C14,0, {g, c} ◦ C13,0, {g, w} ◦ C12,0, {g, w, c} ◦ C16,0},

C16,0 = ⊥,

Ce = △ ∘Ce.

После исключения всех терминальных ветвей синхронная композиция примет вид C0,0 = ⊥, откуда следует тривиальное решение о невыполнимости Φ на Μ.

Проверка альтернативного свойства

Пусть теперь Φ' = E[(g ≡ c ∨ g ≡ w) → (g ≡ b) U (b ∧ g ∧ w ∧ c)] – «Среди всех возможных путей существует хотя бы один такой, на котором все переправятся на правый берег при условии, что, когда коза находится на одном берегу с капустой или волком, то рядом с ней находится лодочник».

Выполним преобразование свойства Φ' к RTL-виду:

Φ' = E(α U β) = β + α ◦ Φ',

α = (g ≡ c ∨ g ≡ w) → (g ≡ b) = (g ≡ ⌉c ∧ g ≡ ⌉w) ∨ (g ≡ b) = {g ≡ ⌉c ≡ ⌉w} + (g ≡ b),

β = (b ∧ g ∧ w ∧ c) = {b, g, w, c}.

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

F0 = β ◦ F1 + α ◦ F0,

F1 = △ ◦ F1­.

Переход в F1 задается оператором «◦», поскольку верифицирующее свойство выполняется для некоторого состояния модели M тогда и только тогда, когда β выполнится хотя бы для одного из его переходов.

Выполним построение синхронной композиции M⊗Φ' с учетом принятых обозначений:

C0,0 = {} ◦ C1­,0,

C1,0 = {b, g} ◦ С2,0,

C2,0 = {g} ◦ C6,0 + {} ◦ C1­,0,

C6,0 = {b, g, w} ◦ C9,0 + {b, g, c} ◦ C10,0 + {b, g} ◦ C2,0,

C9,0 = {w} ◦ C7,0 + {g} ◦ C6,0,

C10,0 = {c} ◦ C8,0 + {g} ◦ C6,0,

C7,0 = {b, g, w} ◦ C9,0 + {b, w, c} ◦ C11,0,

C8,0 = {b, g, c} ◦ C10,0 + {b, w, c} ◦ C11,0,

C11,0 = {c} ◦ C8,0 + {w} ◦ C7,0 + {w, c} ◦ C14,0,

C14,0 = {b, g, w, c} ◦ Ce + {b, w, c} ◦ C11,0,

Ce = △ ∘Ce.

Применив алгоритм маркировки, получим следующий результат:

1.      F: Ce,

2.      F: Ce, C14,0,

3.      F: Ce, C14,0, C11,0,

4.      F: Ce, C14,0, C11, C7,0, C8,0,

5.      F: Ce, C14,0, C11, C7,0, C8,0, C9,0, C10,0,

6.      F: Ce, C14,0, C11, C7,0, C8,0, C9,0, C10,0, C6,0,

7.      F: Ce, C14,0, C11, C7,0, C8,0, C9,0, C10,0, C6,0, C2,0,

8.      F: Ce, C14,0, C11, C7,0, C8,0, C9,0, C10,0, C6,0, C2,0, C1­,0,

9.      F: Ce, C14,0, C11, C7,0, C8,0, C9,0, C10,0, C6,0, C2,0, C1,0, C0,0.

Состояние С0,0 входит во множество состояний, помеченных F, следовательно, Φ' выполняется на M. Так, взяв все возможные пути переходов из конечного состояния в начальное (не проходящими несколько раз через одно и то же состояние), получим все возможные решения данной задачи:

C0,0 → C1,0 → C2,0 → C6,0 → C9,0 → C7,0 → C11,0 → C14,0 → Ce,

C0,0 → C1,0 → C2,0 → C6,0 → C10,0 → C8,0 → C11,0 → C14,0 → Ce.

Обозначая положительными значениями предикатов факт переезда соответствующих субъектов на правый берег, а отрицательными значениями предикатов – факт переезда на левый берег, получим следующие последовательности действий, являющиеся решениями задачи:

bg ⇒ ⌉b ⇒ bw ⇒ ⌉b⌉g ⇒ bc ⇒ ⌉b ⇒ bg,

bg ⇒ ⌉b ⇒ bc ⇒ ⌉b⌉g ⇒ bw ⇒ ⌉b ⇒ bg.

Оценка сложности

Верификация данным методом включает в себя два отдельных алгоритма:

– алгоритм построения синхронной компо­зиции,

– алгоритм маркировки состояний.

Для оценки сложности метода в целом нужно оценить сложность каждого из алгоритмов отдельно. Произведем вначале оценку сложности алгоритма построения синхронной композиции. Обозначим через m число уравнений (состояний) верифицируемой модели, через p – число уравнений верифицирующего свойства, через n – максимальное число переходов любого из уравнений верифицируемой модели, а через t – максимальное число переходов любого из уравнений верифицирующего свойства. Оценка сложности алгоритма синхрокомпозиции в таком случае может быть задана выражением O(mpnt).

Оценим сложность алгоритма маркировки состояний. Поскольку общее число операций данного алгоритма зависит от максимального числа состояний синхрокомпозиции и не может превысить это значение, оценка сложности есть O(mp).

Таким образом, суммарная сложность верификации данным методом составляет O(mpnt + + mp) ≡ O(mp(nt + 1)) ≌ O(mpnt). Проанализируем, как именно следует понимать данную оценку. Положим m ~ p и n ~ t. Это означает, что размеры верифицируемой модели и верифицирующего свойства изменяются пропорционально. В этом случае оценка примет вид O(m2n2). На первый взгляд, может показаться, что в таком виде оценка способна стать серьезной преградой на пути верификации моделей больших систем. Однако при верификации больших систем размеры верифицирующих свойств, как правило, остаются крайне небольшими (не сопоставимыми с размерами проверяемых моделей), а следовательно, в таком виде оценка может быть применена лишь для систем небольших размеров. Принимая во внимание тот факт, что для больших систем m ≫ p и n ≫ t, оценка примет вид O(Cmn) ≌ O(mn), где C = pt есть константа, обозначающая предельное значение произведения переменных p и t. Таким образом, оценка сложности верификации данным методом напрямую зависит от условий взаимосвязей переменных m, p, n и t между собой. В таблице 2 представлены раз- личные вариации данной оценки для различных условий.

Таблица 2

Вариации оценки сложности метода верификации CTL-свойств на базе RTL-нотации

Table 2

Variations in assessing the complexity of the CTL properties verification method based on RTL notation

Вариация	Условие	Описание
O(m2n2)	m ~ p, n ~ t	Число состояний и переходов верифицируемой модели и верифицирующего свойства изменяется пропорционально. Данная оценка применима для моделей систем небольших размеров
O(mn)	m ≫ p, n ≫ t	Число состояний и переходов верифицируемой модели значительно превосходит число состояний и переходов верифицирующего свойства. Данная оценка применима для моделей систем больших размеров
O(m)	m ≫ p, n ≫ t, m ~ n	Число состояний и переходов верифицируемой модели значительно превосходит число состояний и переходов верифицирующего свойства, при этом число переходов модели изменяется пропорционально числу ее состояний. Данная оценка применима для моделей систем очень больших размеров

  Заключение

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

Так, обновленное в данной статье синтаксическое определение нотации позволило проще, понятнее и единообразно задавать выражения обеих логик: LTL и CTL, а описанные аксиомы построения синхронной композиции дают возможность легко осуществлять проверку их выполнимости относительно произвольных моделей систем, также заданных с помощью RTL. Алгоритм маркировки дополнил процесс верификации свойств логики ветвящегося времени, упростив и формализовав этап анализа синхрокомпозиции.

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

Представленные в статье результаты подтверждают идею о возможности унифицированного представления формул темпоральных логик LTL и CTL для анализа свойств моделей систем.

Литература

1.    Кораблин Ю.П., Шипов А.А. Унифицированное представление формул логик LTL и CTL системами рекурсивных уравнений // Программные продукты и системы. 2019. T. 32. № 1. С. 20–25. DOI: 10.15827/0236-235X.125.020-025.

2.    Карпов Ю.Г. Model Checking. Верификация параллельных и распределенных программных систем. СПб: Изд-во БХВ-Петербург, 2010. 552 с.

3.    Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ. Model Checking. М.: Изд-во МЦНМО, 2002. 416 с.

4.    Pnueli. The temporal logic of program. Proc. 18th Annyv. Symp. on Foundation of Computer Science. 1977, pp. 46–57.

5.    Manna Z., Pnueli A. The temporal logic of reactive and concurrent systems: Specification. 1992, 427 p.

6.    Kroger F., Merz S. Temporal logic and state systems. Springer Publ., 2008, 436 p.

7.    Huth M., Ryan M. Logic in computer science: modelling and reasoning about systems. Cambridge Univ. Press, 2004, 443 p.

8.    Хоар Ч. Взаимодействующие последовательные процессы; [пер. с англ.]. М.: Мир, 1989. 264 с. DOI: 10.1145/359576.359585.

9.    Кораблин Ю.П., Шипов А.А., Кочергин А.С. Верификация моделей систем на базе эквациональ­ной характеристики формул LTL // Программные продукты и системы. 2017. № 3. С. 456–460. DOI: 10.15827/0236-235X.119.456-460.

10. Olderog E.-R., Apt K.R. Fairness in parallel programs, the transformational approach. ACM TOPLAS, 1988, vol. 10, iss. 3, pp. 420–455. DOI: 10.1145/44501.44504.

11. Li Y.M., Li Y., Ma Zh. Computation tree logic model checking based on possibility measures. Fuzzy Sets and Systems. 2015, no. 1, vol. 262, pp. 44–59.

References

1. Korablin Yu.P., Shipov A.A. Unified representation of LTL and CTL logic formulas by recursive equation systems. Software & Systems. 2019, vol. 32, no. 1, pp. 20–25. DOI: 10.15827/0236-235X.125.020-025(in Russ.).
2. Karpov Yu.G. Model Checking. Verification of Parallel and Distributed Software Systems. St. Petersburg, BHV Peterburg Publ., 2010, 552 p.
3. Klark E.M., Gramberg O., Peled D. Program Model Verification. Model Checking. Moscow, MTsNMO Publ., 2002, 416 p.
4. Pnueli A. The temporal logic of program. Proc. 18th Annyv. Symp. on Foundation of Computer Science. 1977, pp. 46–57.
5. Manna Z., Pnueli A. The Temporal Logic of Reactive and Concurrent Systems: Specification. 1992, 427 p.
6. Kroger F., Merz St. Temporal Logic and State Systems. Springer, 2008, 436 p.
7. Huth M., Ryan M. Logic in Computer Science: Modelling and Reasoning About Systems. Cambridge Univ. Press, 2004, 443 p.
8. Hoare C.A.R. Communicating sequential processes. Comm. of the ACM. 1978, vol. 21, no. 8, pp. 666–677. DOI: 10.1145/359576.359585.
9. Korablin Yu.P., Shipov A.A., Kochergin A.S. Verification of system models based on the equational characteristics of LTL formulas. Software & Systems. 2017, vol. 30, no. 3, pp. 456–460 (in Russ.).
10. Olderog E.-R., Apt K.R. Fairness in parallel programs, the transformational approach. ACM TOPLAS. 1988, vol. 10, iss. 3, pp. 420–455. DOI: 10.1145/44501.44504.
11. Li Y.M., Li Y., Ma Zh. Computation tree logic model checking based on possibility measures. Fuzzy Sets and Systems. 2015, vol. 262, pp. 44–59.