Логика дерева вычислений

редактировать

Логика дерева вычислений (CTL ) - логика времени ветвления , что означает, что его модель времени представляет собой древовидную структуру, в которой будущее не определено; в будущем есть разные пути, любой из которых может быть реальным, реализованным. Он используется в формальной проверке программных или аппаратных артефактов, обычно в программных приложениях, известных как средства проверки моделей, которые определяют, обладает ли данный артефакт безопасностью или живучесть свойства. Например, CTL может указывать, что, когда выполняется какое-то начальное условие (например, все программные переменные положительны или на шоссе, пересекающем две полосы движения, нет машин), тогда все возможные исполнения программы избегают некоторых нежелательных условий (например, деления числа на ноль или две машины, столкнувшиеся на шоссе). В этом примере свойство безопасности может быть проверено средством проверки модели, которое исследует все возможные переходы из состояний программы, удовлетворяющих начальному условию, и гарантирует, что все такие исполнения удовлетворяют этому свойству. Логика дерева вычислений находится в классе темпоральной логики, который включает в себя линейную временную логику (LTL). Хотя есть свойства, выражаемые только в CTL, и свойства, выражаемые только в LTL, все свойства, выражаемые в любой логике, также могут быть выражены в CTL *.

CTL впервые был предложен Эдмундом М. Кларком и Э. Аллен Эмерсон в 1981 году, который использовал его для синтеза так называемых скелетов синхронизации, то есть абстракций параллельных программ.

Содержание

1 Синтаксис CTL
2 Операторы
- 2.1 Логические операторы
- 2.2 Временные операторы
- 2.3 Минимальный набор операторов
3 Семантика CTL
- 3.1 Определение
- 3.2 Характеристика CTL
- 3.3 Семантические эквивалентности
4 Примеры
5 Отношения с другими логика
6 Расширения
7 См. также
8 Ссылки
9 Внешние ссылки

Синтаксис CTL

Язык языка правильно сформированных формул для CTL порождается следующей грамматикой :

ϕ :: = ⊥ ∣ ⊤ ∣ p ∣ (¬ ϕ) ∣ (ϕ ∧ ϕ) ∣ (ϕ ∨ ϕ) ∣ (ϕ ⇒ ϕ) ∣ (ϕ ⇔ ϕ) ∣ AX ϕ ∣ EX ϕ ∣ AF ϕ ∣ EF ϕ ∣ AG ϕ ∣ EG ϕ ∣ A [ϕ U ϕ] ∣ E [ϕ U ϕ] {\ displaystyle {\ begin {align} \ phi : : = \ bot \ mid \ top \ mid p \ mid (\ neg \ phi) \ mid (\ phi \ land \ phi) \ mid (\ phi \ lor \ phi) \ mid (\ phi \ Rightarrow \ phi) \ середина (\ phi \ Leftrightarrow \ phi) \\ \ mid \ quad {\ t_dv {AX}} \ phi \ mid {\ t_dv {EX}} \ phi \ mid {\ t_dv {AF}} \ phi \ mid {\ t_dv {EF}} \ phi \ mid {\ t_dv {AG}} \ phi \ mid {\ t_dv {EG}} \ phi \ mid {\ t_dv {A}} [\ phi {\ t_dv {U}} \ phi] \ mid {\ t_dv {E}} [\ phi {\ t_dv {U}} \ phi] \ end {выровнено}} }

{\ displaystyle {\ begin {align} \ phi :: = \ bot \ mid \ top \ mid p \ mid (\ neg \ p привет) \ mid (\ phi \ land \ phi) \ mid (\ phi \ lor \ phi) \ mid (\ phi \ Rightarrow \ phi) \ mid (\ phi \ Leftrightarrow \ phi) \\ \ mid \ quad { \ t_dv {AX}} \ phi \ mid {\ t_dv {EX}} \ phi \ mid {\ t_dv {AF}} \ phi \ mid {\ t_dv {EF}} \ phi \ mid {\ t_dv {AG}} \ phi \ mid {\ t_dv {EG}} \ phi \ mid {\ t_dv {A}} [\ phi {\ t_dv {U}} \ phi] \ mid {\ t_dv {E}} [\ phi {\ t_dv {U}} \ phi] \ end {align}}}

где $p {\ displaystyle p}$ $p$ находится в пределах набора атомарных формул. Необязательно использовать все связки - например, ${¬, ∧, AX, AU, EU} {\ displaystyle \ {\ neg, \ land, {\ t_dv {AX}}, {\ t_dv {AU }}, {\ t_dv {EU}} \}}$ ${\ displaystyle \ {\ neg, \ land, {\ t_dv {AX}}, {\ t_dv {AU}}, {\ t_dv {EU}} \}}$ содержит полный набор связок, и остальные могут быть определены с их помощью.

$A {\ displaystyle {\ t_dv {A}}}$ $\t_dv{A}$ означает «по всем путям» (неизбежно)
$E {\ displaystyle {\ t_dv {E}}}$ $\ t_dv {E}$ означает «по крайней мере (существует) один путь» (возможно)

Например, следующая формула CTL правильно построена:

EF (EG p ⇒ AF r {\ displaystyle {\ t_dv {EF }} ({\ t_dv {EG}} p \ Rightarrow {\ t_dv {AF}} r}

\ t_dv {EF} (\ t_dv {EG} p \ Rightarrow \ t_dv {AF} r

)

Следующая формула CTL неверна:

EF (r U q) {\ displaystyle {\ t_dv {EF}} {\ big (} r {\ t_dv {U}} q ​​{\ big)}}

\ t_dv {EF} \ большой (r \ t_dv {U} q \ big)

Проблема с этой строкой в том, что $U {\ displaystyle U}$ $U$ может встречаться только в паре с $A {\ displaystyle A}$ $A$ или $E {\ displaystyle E}$ $E$ . Он использует атомарные предложения в качестве строительных блоков для создания утверждений о состояниях системы. CTL затем объединяет эти предложения в формулы, используя логические операторы и темпоральные логики.

Операторы

Логические операторы

логические операторы являются обычными: ¬, ∨, ∧, ⇒ и ⇔. Наряду с Операторы se В формулах CTL также могут использоваться логические константы true и false.

Временные операторы

Временные операторы следующие:

Квантификаторы по путям
- Aφ - A ll: φ должен удерживаться на всех путях, начиная с текущего состояния.
- Eφ - E существует: существует по крайней мере один путь, начинающийся с текущего состояния где φ выполняется.
Специфические для пути кванторы
- Xφ - Ne x t: φ должен удерживаться в следующем состоянии (этот оператор иногда обозначается как N вместо X).
- Gφ - G локально: φ должен удерживать весь последующий путь.
- Fφ - F наконец: φ в конечном итоге должен удерживаться (где-то на последующем пути).
- φ Uψ - U ntil: φ должен удерживаться по крайней мере до тех пор, пока в некоторой позиции не будет удерживаться ψ. Это означает, что ψ будет проверяться в будущем.
- φ Wψ - W eak до: φ должен удерживаться, пока не будет выполнено ψ. Отличие от U состоит в том, что нет гарантии, что ψ когда-либо будет проверяться. Оператор W иногда называют «если».

В CTL * временные операторы можно свободно смешивать. В CTL оператор всегда должен быть сгруппирован в две группы: один оператор пути, за которым следует оператор состояния. См. Примеры ниже. CTL * строго более выразителен, чем CTL.

Минимальный набор операторов

В CTL есть минимальный набор операторов. Все формулы CTL можно преобразовать для использования только этих операторов. Это полезно при проверке модели. Один минимальный набор операторов: {true, ∨, ¬, EG, EU, EX}.

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

EFφ == E [true U (φ)] (поскольку F φ == [истина U (φ)])
AXφ == ¬ EX (¬φ)
AGφ == ¬ EF (¬φ) == ¬ E [истина U (¬φ)]
AFφ == A [истина U φ] == ¬ EG (¬φ)
A[φUψ] == ¬ (E [(¬ψ) U ¬ (φ∨ψ) ] ∨ EG (¬ψ))

Семантика CTL

Определение

Формулы CTL интерпретируются в Transition Systems. Система переходов - это тройка $M = (S, →, L) {\ displaystyle {\ mathcal {M}} = (S, {\ rightarrow}, L)}$ ${\ displaystyle {\ mathcal {M}} = (S, {\ rightarrow}, L)}$ , где $S {\ displaystyle S}$ $S$ - это набор состояний, $→ ⊆ S × S {\ displaystyle {\ rightarrow} \ substeq S \ times S}$ ${\ displaystyle {\ rightarrow} \ substeq S \ times S}$ - переход отношение, которое предполагается последовательным, т. е. каждое состояние имеет по крайней мере одного преемника, а $L {\ displaystyle L}$ $L$ - функция маркировки, присваивающая состояниям пропозициональные буквы. Пусть $M = (S, →, L) {\ displaystyle {\ mathcal {M}} = (S, \ rightarrow, L)}$ $\ mathcal {M} = (S, \ rightarrow, L)$ будет такой переходной моделью

s ∈ S, ϕ ∈ F {\ displaystyle s \ in S, \ phi \ in F}

s \ in S, \ phi \ in F

, где F - набор wffs на языке из

M {\ displaystyle {\ mathcal {M}}}

{\ mathcal {M}}

Тогда отношение семантического entailment $(M, s ⊨ ϕ) {\ displaystyle ({\ mathcal {M }}, s \ models \ phi)}$ $(\ mathcal {M}, s \ models \ phi)$ определяется рекурсивно на $ϕ {\ displaystyle \ phi}$ $\ phi$ :

$((M, s) ⊨ ⊤) ∧ ((M, s) ⊭ ⊥) {\ displaystyle {\ Big (} ({\ mathcal {M}}, s) \ models \ top {\ Big)} \ land {\ Big (} ({\ mathcal {M}}, s) \ not \ модели \ бот {\ Big)}}$ ${\ Big (} ({\ mathcal {M}}, s) \ models \ top {\ Big)} \ land {\ Big (} ({\ mathcal {M}}, s) \ not \ models \ bot {\ Big) }$
$((M, s) ⊨ p) ⇔ (p ∈ L (s)) {\ displaystyle {\ Big (} ({\ mathcal {M}}, s) \ models p {\ Big)} \ Leftrightarrow {\ Big (} p \ in L (s) {\ Big)}}$ ${\ Big (} ({\ mathcal {M}}, s) \ models p {\ Big)} \ Leftrightarrow {\ Big (} p \ in L (s) {\ Big)}$
$((M, s) ⊨ ¬ ϕ) ⇔ ((M, s) ⊭ ϕ) {\ displaystyle {\ Big (} ({\ mathcal {M}}, s) \ models \ neg \ phi {\ Big)} \ Leftrightarrow {\ Big (} ({\ mathcal {M}}, s) \ не \ models \ phi {\ Big)}}$ $\ Big ((\ mathcal {M}, s) \ models \ neg \ phi \ Big) \ Leftrightarrow \ Big ((\ mathcal { M}, s) \ not \ models \ phi \ Big)$
$((M, s) ⊨ ϕ 1 ∧ ϕ 2) ⇔ ( ((M, s) ⊨ ϕ 1) ∧ ((M, s) ⊨ ϕ 2)) {\ displaystyle {\ Big (} ({\ mathcal {M}}, s) \ models \ phi _ {1} \ земля \ phi _ {2} {\ Big)} \ Leftrightarrow {\ Big (} {\ big (} ({\ mathcal {M}}, s) \ models \ phi _ {1} {\ big)} \ land {\ big (} ({\ mathcal {M}}, s) \ models \ phi _ {2} {\ big)} {\ Big)}}$ $\ Big ((\ mathcal {M}, s) \ models \ phi_1 \ land \ phi_2 \ Big) \ Leftrightarrow \ Big (\ big ((\ mathcal {M}, s) \ models \ phi_1 \ big) \ land \ big ((\ mathcal {M}, s) \ models \ phi_2 \ big) \ Big)$
$((M, s) ⊨ ϕ 1 ∨ ϕ 2) ⇔ (((M, s) ⊨ ϕ 1) ∨ ((M, s) ⊨ ϕ 2)) {\ displaystyle {\ Big (} ({\ mathcal {M}}, s) \ models \ phi _ { 1} \ lor \ phi _ {2} {\ Big)} \ Leftrightarrow {\ Big (} {\ big (} ({\ mathcal {M}}, s) \ models \ phi _ {1} {\ big) } \ lor {\ big (} ({\ mathcal {M}}, s) \ models \ phi _ {2} {\ big)} {\ Big)}}$ $\ Big ((\ mathcal {M}, s) \ models \ phi_1 \ lor \ phi_2 \ Big) \ Leftrightarrow \ Big (\ big ((\ mathcal {M}, s) \ models \ phi_1 \ big) \ lor \ big ((\ mathcal {M}, s) \ models \ phi_2 \ big) \ Big)$
$((M, s) ⊨ ϕ 1 ⇒ ϕ 2) ⇔ (((M, s) ⊭ ϕ 1) ∨ ((M, s) ⊨ ϕ 2)) {\ displaystyle {\ Big (} ({\ mathcal {M}}, s) \ models \ phi _ {1} \ Rightarrow \ phi _ {2} {\ Big)} \ Leftrightarrow {\ Big (} {\ big (} ({\ mathcal {M}}, s) \ not \ models \ phi _ {1 } {\ big)} \ lor {\ big (} ({\ mathcal {M}}, s) \ models \ phi _ {2} {\ big)} {\ Big)}}$ $\ Big ((\ mathcal {M}, s) \ models \ phi_1 \ Rightarrow \ phi_2 \ Big) \ Leftrightarrow \ Big (\ big ((\ mathcal { M}, s) \ not \ models \ phi_1 \ big) \ lor \ big ((\ mathcal {M}, s) \ models \ phi_2 \ big) \ Big)$
$((M, s) ⊨ ϕ 1 ⇔ ϕ 2) ⇔ (((((M, s) ⊨ ϕ 1) ∧ ((M, s) ⊨ ϕ 2)) ∨ (¬ ((M, s) ⊨ ϕ 1) ∧ ¬ ( ( РС) ⊨ ϕ 2))) {\ displaystyle {\ bigg (} ({\ mathcal {M}}, s) \ models \ phi _ {1} \ Leftrightarrow \ phi _ {2} {\ bigg)} \ Leftrightarrow { \ bigg (} {\ Big (} {\ big (} ({\ mathcal {M}}, s) \ models \ phi _ {1} {\ big)} \ land {\ big (} ({\ mathcal { M}}, s) \ models \ phi _ {2} {\ big)} {\ Big)} \ lor {\ Big (} \ neg {\ big (} ({\ mathcal {M}}, s) \ модели \ phi _ {1} {\ big)} \ land \ neg {\ big (} ({\ mathcal {M}}, s) \ models \ phi _ {2} {\ big)} {\ Big)} {\ bigg)}}$ $\ bigg ((\ mathcal {M}, s) \ models \ phi_1 \ Leftrightarrow \ phi_2 \ bigg) \ Leftrightarrow \ bigg (\ Big (\ big ((\ mathcal {M}, s) \ models \ phi_1 \ big) \ lan d \ big ((\ mathcal {M}, s) \ models \ phi_2 \ big) \ Big) \ lor \ Big (\ neg \ big ((\ mathcal {M}, s) \ models \ phi_1 \ big) \ земля \ neg \ big ((\ mathcal {M}, s) \ models \ phi_2 \ big) \ Big) \ bigg)$
$((M, s) ⊨ AX ϕ) ⇔ (∀ ⟨s → s 1⟩ ((M, s 1) ⊨ ϕ)) {\ displaystyle {\ Big (} ({\ mathcal {M}}, s) \ models AX \ phi {\ Big)} \ Leftrightarrow {\ Big (} \ forall \ langle s \ rightarrow s_ {1} \ rangle {\ big (} ({\ mathcal {M} }, s_ {1}) \ models \ phi {\ big)} {\ Big)}}$ $\ Big ((\ mathcal {M}, s) \ models AX \ phi \ Big) \ Leftrightarrow \ Big (\ forall \ langle s \ rightarrow s_1 \ rangle \ big ((\ mathcal {M}, s_1) \ models \ phi \ big) \ Big)$
$((M, s) ⊨ EX ϕ) ⇔ (∃ ⟨s → s 1⟩ ((M, s 1) ⊨ ϕ)) {\ Displaystyle {\ Big (} ({\ mathcal {M}}, s) \ models EX \ phi {\ Big)} \ Leftrightarrow {\ Big (} \ exists \ langle s \ rightarrow s_ { 1} \ rangle {\ big (} ({\ mathcal {M}}, s_ {1}) \ models \ phi {\ big)} {\ Big)}}$ $\ Big ((\ mathcal {M}, s) \ models EX \ phi \ Big) \ Leftrightarrow \ Big (\ exists \ langle s \ rightarrow s_1 \ rangle \ big ((\ mathcal {M}, s_1) \ models \ phi \ big) \ Big)$
$((M, s) ⊨ AG ϕ) ⇔ (∀ ⟨s 1 → s 2 →…⟩ (s = s 1) ∀ i ((M, si) ⊨ ϕ)) {\ displaystyle {\ Big (} ({\ mathcal {M}}, s) \ models AG \ phi {\ Big)} \ Leftrightarrow {\ Big (} \ forall \ langle s_ {1} \ rightarrow s_ {2} \ rightarrow \ ldots \ rangle (s = s_ {1}) \ forall i {\ big (} ({\ mathcal {M}}, s_ {i}) \ models \ phi {\ big)} {\ Big)}}$ $\ Big ((\ mathcal {M}, s) \ models AG \ phi \ Big) \ Leftrightarrow \ Big (\ forall \ langle s_1 \ rightarrow s_2 \ rightarrow \ ldots \ rangle (s = s_1) \ forall i \ big ((\ mathcal {M}, s_i) \ models \ phi \ big) \ Big)$
$((M, s) ⊨ EG ϕ) ⇔ (∃ ⟨s 1 → s 2 →…⟩ (s = s 1) ∀ i ((M, si) ⊨ ϕ)) { \ Displaystyle {\ Big (} ({\ mathcal {M}}, s) \ models EG \ phi {\ Big)} \ Leftrightarrow {\ Big (} \ exists \ langle s_ {1} \ rightarrow s_ {2} \ rightarrow \ ldots \ rangle (s = s_ {1}) \ forall i {\ big (} ({\ mathcal {M}}, s_ {i}) \ models \ phi {\ big)} {\ Big)}}$ $\ Big ((\ mathcal {M}, s) \ models EG \ phi \ Big) \ Leftrightarrow \ Big (\ exists \ langle s_1 \ rightarrow s_2 \ rightarrow \ ldots \ rangle (s = s_1) \ forall i \ big ((\ mathcal {M}, s_i) \ models \ phi \ big) \ Big)$
$((M, s) ⊨ AF ϕ) ⇔ (∀ ⟨s 1 → s 2 →…⟩ (s = s 1) ∃ я ((M, si) ⊨ ϕ)) {\ displaystyle {\ Big ( } ({\ mathcal {M}}, s) \ models AF \ phi {\ Big)} \ Leftrightarrow {\ Big (} \ forall \ langle s_ {1} \ rightarrow s_ {2} \ rightarrow \ ldots \ rangle ( s = s_ {1}) \ exists i {\ big (} ({\ mathcal {M}}, s_ {i}) \ models \ phi {\ big)} {\ Big)}}$ $\ Big ((\ mathcal {M}, s) \ models AF \ phi \ Big) \ Leftrightarrow \ Big (\ forall \ langle s_1 \ rightarrow s_2 \ rightarrow \ ldots \ rangle (s = s_1) \ exists i \ big ((\ mathcal {M}, s_i) \ models \ phi \ big) \ Big)$
$((M, s) ⊨ EF ϕ) ⇔ (∃ ⟨s 1 → s 2 →…⟩ (s = s 1) ∃ я ((M, si) ⊨ ϕ)) {\ displaystyle {\ Big (} ({\ mathcal {M}}, s) \ models EF \ phi {\ Big)} \ Leftrightarrow {\ Big (} \ exists \ langle s_ {1} \ rightarrow s_ {2} \ rightarrow \ ldots \ rangle (s = s_ { 1}) \ exists i {\ big (} ({\ mathcal {M}}, s_ {i}) \ models \ phi {\ big)} {\ Big)}}$ $\ Big ((\ mathcal {M}, s) \ models EF \ phi \ Big) \ Leftrightarrow \ Big (\ exists \ langle s_1 \ rightarrow s _2 \ rightarrow \ ldots \ rangle (s = s_1) \ существует i \ big ((\ mathcal {M}, s_i) \ models \ phi \ big) \ Big)$
$((M, s) ⊨ A [ϕ 1 U ϕ 2]) ⇔ (∀ ⟨s 1 → s 2 →…⟩ (s = s 1) ∃ i (((M, si) ⊨ ϕ 2) ∧ (∀ (j < i) ( M, s j) ⊨ ϕ 1))) {\displaystyle {\bigg (}({\mathcal {M}},s)\models A[\phi _{1}U\phi _{2}]{\bigg)}\Leftrightarrow {\bigg (}\forall \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\Big (}{\big (}({\mathcal {M}},s_{i})\models \phi _{2}{\big)}\land {\big (}\forall (j$ $\ bigg ((\ mathcal {M}, s) \ models A [\ phi_1 U \ phi_2] \ bigg) \ Leftrightarrow \ bigg (\ forall \ langle s_1 \ rightarrow s_2 \ rightarrow \ ldots \ rangle (s = s_1) \ существует i \ Big (\ big ((\ mathcal {M}, s_i) \ models \ phi_2 \ big) \ land \ big (\ forall (j <i) (\ mathcal {M}, s_j) \ models \ phi_1 \ big) \ Big) \ bigg)$
$(( M, s) ⊨ E [ϕ 1 U ϕ 2]) ⇔ (∃ ⟨s 1 → s 2 →…⟩ (s = s 1) ∃ i (((M, si) ⊨ ϕ 2) ∧ (∀ (j < i) ( M, s j) ⊨ ϕ 1))) {\displaystyle {\bigg (}({\mathcal {M}},s)\models E[\phi _{1}U\phi _{2}]{\bigg)}\Leftrightarrow {\bigg (}\exists \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\Big (}{\big (}({\mathcal {M}},s_{i})\models \phi _{2}{\big)}\land {\big (}\forall (j$ $\ bigg ((\ mathcal {M}, s) \ models E [\ phi_1 U \ phi_2] \ bigg) \ Leftrightarrow \ bigg (\ exists \ langle s_1 \ rightarrow s_2 \ rightarrow \ ldots \ rangle (s = s_1) \ exists i \ Big ( \ big ((\ mathcal {M}, s_i) \ models \ phi_2 \ big) \ land \ big (\ forall (j <i) (\ mathcal {M}, s_j) \ models \ phi_1 \ big) \ Big) \ bigg)$

Характеристика CTL

Правила 10–15 выше относятся к путям вычислений в моделях и являются тем, что в конечном итоге характеризует «Дерево вычислений»; они представляют собой утверждения о природе бесконечно глубокого дерева вычислений, основанного на данном состоянии $s {\ displaystyle s}$ $s$ .

Семантические эквивалентности

Формулы $ϕ {\ displaystyle \ phi}$ $\ phi$ и $ψ {\ displaystyle \ psi}$ $\ psi$ называются семантически эквивалентными, если любое состояние в любой модели, удовлетворяющее одному, удовлетворяет и другое. Это обозначается $ϕ ≡ ψ {\ displaystyle \ phi \ Equiv \ psi}$ $\ phi \ Equiv \ psi$

Можно видеть, что A и E двойственны, являясь кванторами универсального и экзистенциального пути вычислений соответственно: $¬ A ϕ ≡ E ¬ ϕ {\ displaystyle \ neg A \ phi \ Equiv E \ neg \ phi}$ $\ neg A \ phi \ Equiv E \ neg \ phi$ .

Кроме того, то же самое с G и F.

Следовательно, экземпляр Законов Де Моргана может быть сформулировано в CTL:

¬ AF ϕ ≡ EG ¬ ϕ {\ displaystyle \ neg AF \ phi \ Equiv EG \ neg \ phi}

\ neg AF \ phi \ Equiv EG \ neg \ phi

¬ EF ϕ ≡ AG ¬ ϕ {\ displaystyle \ neg EF \ phi \ Equiv AG \ neg \ phi}

\ neg EF \ phi \ Equiv AG \ neg \ phi

¬ AX ϕ ≡ EX ¬ ϕ {\ displaystyle \ neg AX \ phi \ Equiv EX \ neg \ phi}

\ neg AX \ phi \ Equiv EX \ neg \ phi

Используя такие тождества, можно показать, что подмножество временных связок CTL является адекватным, если он содержит $EU {\ displaystyle EU}$ $EU$ , хотя бы один из ${AX, EX} {\ displaystyle \ {AX, EX \}}$ $\ {AX, EX \ }$ и по крайней мере одну из ${EG, AF, AU} {\ displaystyle \ {EG, AF, AU \}}$ $\ {EG, AF, AU \}$ и логических связок.

Важные эквивалентности ниже называются законами расширения; они позволяют вовремя развернуть верификацию связки CTL по отношению к ее преемникам.

AG ϕ ≡ ϕ ∧ AXAG ϕ {\ displaystyle AG \ phi \ Equiv \ phi \ land AXAG \ phi}

AG \ phi \ Equiv \ phi \ land AX AG \ phi

EG ϕ ≡ ϕ ∧ EXEG ϕ {\ displaystyle EG \ phi \ Equiv \ phi \ land EXEG \ phi}

EG \ phi \ Equiv \ phi \ land EX EG \ phi

AF ϕ ≡ ϕ ∨ AXAF ϕ {\ displaystyle AF \ phi \ Equiv \ phi \ lor AXAF \ phi}

AF \ phi \ Equiv \ phi \ lor AX AF \ phi

EF ϕ ≡ ϕ ∨ EXEF ϕ {\ displaystyle EF \ phi \ Equiv \ phi \ lor EXEF \ phi}

EF \ phi \ Equiv \ phi \ lor EX EF \ phi

A [ϕ U ψ] ≡ ψ ∨ (ϕ ∧ AXA [ϕ U ψ]) {\ displaystyle A [\ phi U \ psi] \ Equiv \ psi \ lor (\ phi \ land AXA [ \ phi U \ psi])}

A [\ phi U \ psi] \ Equiv \ psi \ lor (\ phi \ land AX A [\ phi U \ psi])

E [ϕ U ψ] ≡ ψ ∨ (ϕ ∧ EXE [ϕ U ψ]) {\ displaystyle E [\ phi U \ psi] \ эквив \ psi \ lor (\ phi \ land EXE [\ phi U \ psi])}

E [\ phi U \ psi] \ Equiv \ psi \ lor (\ phi \ land EX E [\ phi U \ psi])

Примеры

Пусть «P» означает «я люблю шоколад», а Q - «на улице тепло».

AG.P

«Отныне я буду любить шоколад, что бы ни случилось».

EF.P

«Возможно, когда-нибудь я буду любить шоколад, хотя бы на один день».

AF.EG.P

«Всегда возможно (AF), что я внезапно начнёт любить шоколад всё остальное время ". (Примечание: не только до конца моей жизни, поскольку моя жизнь конечна, а G бесконечна).

EG.AF.P

«Это критический момент в моей жизни. В зависимости от того, что произойдет дальше (E), возможно, что в остальное время (G) всегда будет какое-то время в будущем (AF), когда я буду любить шоколад. Однако, если в следующий раз произойдет что-то не так, то все ставки отменены и нет никаких гарантий относительно буду ли я когда-нибудь любить шоколад ».

Два следующих примера показывают разницу между CTL и CTL *, поскольку они допускают, чтобы оператор while не определялся каким-либо оператором пути (A или E ):

AG(PUQ)

«С этого момента, пока на улице не станет жарко, я буду любить шоколад каждый божий день. Когда на улице станет тепло, все ставки на то, буду ли я больше любить шоколад. О, и это в конечном итоге гарантированно будет тепло снаружи, даже если только на один день. "

EF((EX.P) U(AG.Q))

" Возможно, что: рано или поздно наступит время, когда будет тепло вечно ( AG.Q) и что до этого времени там всегда будет способ заставить меня полюбить шоколад на следующий день (EX.P). "

Отношения с другими логиками

Логика дерева вычислений (CTL) является подмножеством CTL *, а также модальное μ-исчисление. CTL также является фрагментом книги Алура, Хенцингера и Купфермана Temporal Logic (ATL) с переменным временем.

Логика дерева вычислений (CTL) и Линейная временная логика (LTL) оба являются подмножеством CTL *. CTL и LTL не эквивалентны и имеют общее подмножество, которое является правильным подмножеством как CTL, так и LTL.

FG.P существует в LTL, но не в CTL.
AG(P $⇒ {\ displaystyle \ Rightarrow}$ $\ Rightarrow$ ((EX.Q) $∧ {\ displaystyle \ land}$ $\ land$ (EX¬Q))) и AG.EF .P существует в CTL, но не в LTL.

Расширения

CTL был расширен квантором второго порядка $∃ p {\ displaystyle \ exists p}$ ${\ displaystyle \ exists p}$ и $∀ p {\ displaystyle \ forall p}$ $\ forall p$ . Есть две семантики:

семантика дерева. Помечаем узлы дерева вычислений. QCTL * = QCTL = MSO над деревьями. Проверка модели и ее выполнимость полностью завершены.
семантика структуры. Мы маркируем состояния. QCTL * = QCTL = MSO по графикам. Проверка модели является PSPACE-полной, но выполнимость неразрешима.

Было предложено сокращение от задачи проверки модели QCTL с семантикой структуры до TQBF (истинные количественные двоичные формулы), чтобы использовать преимущества решателей QBF.

См. Также

Ссылки

EM Кларк; E.A. Эмерсон (1981). «Разработка и синтез каркасов синхронизации с использованием временной логики ветвления» (PDF). Логика программ, Труды семинара, Конспект лекций по информатике. Спрингер, Берлин. 131 : 52–71.
Майкл Хут; Марк Райан (2004). Логика в информатике (второе издание). Издательство Кембриджского университета. п. 207. ISBN 978-0-521-54310-1.
Emerson, E.A.; Халперн, Дж. Ю. (1985). «Процедуры принятия решений и выразительность во временной логике ветвления времени». Журнал компьютерных и системных наук. 30 (1): 1–24. doi : 10.1016 / 0022-0000 (85) 90001-7.
Clarke, E.M.; Эмерсон, Э. А. и Систла, А. П. (1986). «Автоматическая проверка конечных параллельных систем с использованием спецификаций временной логики». Транзакции ACM по языкам и системам программирования. 8 (2): 244–263. doi : 10.1145 / 5397.5399.
Эмерсон, Э. А. (1990). «Временная и модальная логика». В Ян ван Леувен (ред.). Справочник по теоретической информатике, т. B. Пресса MIT. С. 955–1072. ISBN 978-0-262-22039-2.

Внешние ссылки

Обучающие слайды CTL