Вероятностные темпоральные логики и алгоритмы верификации

PTL

PTL (propositional temporal logic) — темпоральная логика линейного времени. Формулы PTL выражают свойства бесконечных траекторий графа состояний ВМАС:

Ф: = true | a | Ф Щ Ф| Ф Ъ Ф | Ш Ф | X (Ф) | Ф U Ф.

a — пропозициональная переменная.

X (Ф) — оператор Next. Требует, чтобы свойство Ф выполнялось во втором состоянии пути.

Ф₁ U Ф₂ — оператор Until. Оператор выполняется, если на пути имеется состояние, в котором соблюдается свойство Ф₂ и в каждом предшествующем состоянии этого пути соблюдается свойство Ф₁.

В статье [Courcoubetis et al., 1995] приводится алгоритм верификации для этой логики, имеющий полиномиальную сложность от размера модели и экспоненциальную сложность от размера формулы верификации.

Ограниченный PTL

Это подмножество PTL без оператора Until:

Ф: = true | a | Ф Щ Ф| Ф Ъ Ф | Ш Ф | X (Ф).

Для ограниченного PTL автором разработан алгоритм верификации полиномиальной сложности от размера модели и размера формулы.

PCTL

PCTL (probabilistic computation tree logic) — темпоральная логика ветвящегося времени. Формулы PCTL выражают свойства деревьев вычислений:

Ф: = true | a | Ф Щ Ф| Ф Ъ Ф | Ш Ф | [X (Ф)]_Кp | [Ф U Ф]_Кp

К—О { і, >}, p О [0; 1].

a — пропозициональная переменная.

[X (Ф)]_Кp — выполнено, если с вероятностью Кp на следующем состоянии выполнено Ф.

[Ф₁ U Ф₂]_—Кp — выполнено, если с вероятностью Кp существует путь, на некотором состоянии которого выполнено Ф₂, а на всех предшествующих состояниях этого пути выполнено Ф₁.

Для логики PCTL существует алгоритм верификации полиномиальной сложности от размера модели и размера формулы, представленный в [Hansson et al., 1994].

Расширенный PCTL

Мы расширяем PCTL, добавляя формулы следующего вида:

Ф: = [X (k, Ф)]_—Кp | X^OR(k, Ф)]_—Кp | [X^AND(k, Ф)]_—Кp, (k? 1, целое) К—О { і, >}, p О [0; 1], k? 1 — целое.

Эти формулы имеют следующий смысл:

[X (k, Ф)]_—Кp — выполнено, если с вероятностью Кp существует путь, ровно на k-ом состоянии которого выполнено Ф,.

[X^OR(k, Ф)]_—Кp — выполнено, если с вероятностью Кp существует путь, для которого существует такое 1? i? k, что на i-ом состоянии этого пути выполнено Ф,.

[X^AND(k, Ф)]_—Кp — выполнено, если с вероятностью Кp существует путь, для которого для всех 1? i? k на i-ом состоянии этого пути выполнено Ф.

Для расширенного PCTL в работе обобщен известный алгоритм верификации PCTL из [Hansson et al., 1994]. При этом сохранены его оценки сложности: он является полиномиальным от размера модели, размера формулы и максимального k.