Logika CTL

Przykład modelu logiki CTL

Logika CTL – jedna z logik temporalnych. Jest oparta na liniowej strukturze czasu.

Język

• taki sam, jak w logice CTL*

Formuły

• w porównaniu do logiki CTL*, każdy operator temopralny musi być poprzedzony przez operator ścieżkowy ($A$ bądź $E$):
  • formuła poprawna zarówno w CTL*, jak i w CTL: $AFAG\alpha \Rightarrow EFEG\beta$
  • formuła poprawna w CTL*, ale niepoprawna w CTL: $AFG\alpha \Rightarrow EFG\beta$
• każda taka para operatorów: $(AX,EX,AF,EF,AG,EG,AU,EU,AR,ER)$ tworzy operator logiki CTL.
• operatory $AU,EU,AX,EX$ są podstawowe, a z nich można wyprowadzić pozostałe:

$AF\alpha \equiv A(\mathrm{\top }U\alpha )$

$EF\alpha \equiv E(\mathrm{\top }U\alpha )$

$AG\alpha \equiv A(\alpha U\mathrm{\perp })$

$EG\alpha \equiv E(\alpha U\mathrm{\perp })$

$A(\alpha R\beta )\equiv A(\mathrm{\neg }(\mathrm{\neg }\alpha U\mathrm{\neg }\beta ))$

$E(\alpha R\beta )\equiv E(\mathrm{\neg }(\mathrm{\neg }\alpha U\mathrm{\neg }\beta ))$

Prawdziwość formuł

• oznaczenia:

$(M,s_i)\models \alpha$ – formuła $\alpha$ jest prawdziwa w strukturze $M$ w stanie $s_i$

• warunki prawdziwości podstawowych formuł:

$(M,s_i)\models p\iff p\in L(s_i)$

$(M,s_i)\models {\alpha }_1\wedge {\alpha }_2\iff (M,s_i)\models {\alpha }_1\wedge (M,s_i)\models {\alpha }_2$

$(M,s_i)\models \mathrm{\neg }\alpha \iff \mathrm{\neg }(M,s_i)\models \alpha$

$(M,s_i)\models A({\alpha }_{1}U{\alpha }_2)\iff \mathrm{\forall }{x}_i\mathrm{\exists }(k⩾i):(s_k\models {\alpha }_2\wedge \mathrm{\forall }j:(i⩽j<k)(s_j\models {\alpha }_1)$

$(M,s_i)\models E({\alpha }_{1}U{\alpha }_2)\iff \mathrm{\exists }{x}_i\mathrm{\exists }(k⩾i):(s_k\models {\alpha }_2\wedge \mathrm{\forall }j:(i⩽j<k)(s_j\models {\alpha }_1)$

$(M,s_i)\models AX\alpha \iff \mathrm{\forall }{x}_i(M,s_{i+1})\models \alpha$

$(M,s_i)\models EX\alpha \iff \mathrm{\exists }{x}_i(M,s_{i+1})\models \alpha$

Linki zewnętrzne

• Szablon:Cytuj
• Szablon:Cytuj