Logika 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 (${\displaystyle A}$ bądź ${\displaystyle E}$):
  • formuła poprawna zarówno w CTL*, jak i w CTL: ${\displaystyle AFAG\alpha \Rightarrow EFEG\beta }$
  • formuła poprawna w CTL*, ale niepoprawna w CTL: ${\displaystyle AFG\alpha \Rightarrow EFG\beta }$
• każda taka para operatorów: ${\displaystyle (AX,EX,AF,EF,AG,EG,AU,EU,AR,ER)}$ tworzy operator logiki CTL.
• operatory ${\displaystyle AU,EU,AX,EX}$ są podstawowe, a z nich można wyprowadzić pozostałe:

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

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

${\displaystyle AG\alpha \equiv A(\alpha U\bot )}$

${\displaystyle EG\alpha \equiv E(\alpha U\bot )}$

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

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

Prawdziwość formuł

• oznaczenia:

${\displaystyle (M,s_{i})\models \alpha }$ – formuła ${\displaystyle \alpha }$ jest prawdziwa w strukturze ${\displaystyle M}$ w stanie ${\displaystyle s_{i}}$

• warunki prawdziwości podstawowych formuł:

${\displaystyle (M,s_{i})\models p\Leftrightarrow p\in L(s_{i})}$

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

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

${\displaystyle (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})}$

${\displaystyle (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})}$

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

${\displaystyle (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 [online], Politechnika Wrocławska [dostęp 2020-06-27]  (ang.).
• Temporal Logics [online]  (ang.).