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(\top U\alpha )$

$EF\alpha \equiv E(\top U\alpha )$

$AG\alpha \equiv A(\alpha U\bot )$

$EG\alpha \equiv E(\alpha U\bot )$

$A(\alpha R\beta )\equiv A(\neg (\neg \alpha U\neg \beta ))$

$E(\alpha R\beta )\equiv E(\neg (\neg \alpha U\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\Leftrightarrow p\in L(s_{i})$

$(M,s_{i})\models \alpha _{1}\wedge \alpha _{2}\Leftrightarrow (M,s_{i})\models \alpha _{1}\wedge (M,s_{i})\models \alpha _{2}$

$(M,s_{i})\models \neg \alpha \Leftrightarrow \neg (M,s_{i})\models \alpha$

$(M,s_{i})\models A(\alpha _{1}U\alpha _{2})\Leftrightarrow \forall x_{i}\ \exists (k\geqslant i):(s_{k}\models \alpha _{2}\wedge \forall j:(i\leqslant j<k)(s_{j}\models \alpha _{1})$

$(M,s_{i})\models E(\alpha _{1}U\alpha _{2})\Leftrightarrow \exists x_{i}\ \exists (k\geqslant i):(s_{k}\models \alpha _{2}\wedge \forall j:(i\leqslant j<k)(s_{j}\models \alpha _{1})$

$(M,s_{i})\models AX\alpha \Leftrightarrow \forall x_{i}\ (M,s_{i+1})\models \alpha$

$(M,s_{i})\models EX\alpha \Leftrightarrow \exists x_{i}\ (M,s_{i+1})\models \alpha$

Linki zewnętrzne

• PawełP. Głuchowski PawełP., Temporal Logic and Timed Automata, CTL logic, Politechnika Wrocławska [dostęp 2020-06-27]  (ang.).
• Temporal Logics  (ang.).