Logika CTL*

Logika CTL* – jedna z logik temporalnych. Jest oparta na rozgałęzionej strukturze czasu (rozszerzenie logiki LTL o warianty czasu).

Struktura czasu

Strukturą czasu w CTL* jest drzewiasta struktura $M=(S,R,L),$ gdzie:

• $S$ – zbiór stanów $S=\{s_{0},s_{1},s_{2},\dots \}$
• $R$ – relacja między stanami (następstwo czasu) $\forall x\in S\ \exists y\in S:(x,y)\in R$
• $L$ – wartościowanie (przypisanie każdemu ze stanów wyrażeń, które są prawdziwe w tym stanie)

$L:S\times WA\rightarrow \{0,1\},WA$ – zbiór wyrażeń atomowych

• ścieżką jest w $M$ jest każda sekwencja momentów czasu:

$x=(s_{0},s_{1},s_{2},\dots ):\forall i(s_{i},s_{i+1})\in R$

• $x_{i}$ oznacza ścieżkę rozpoczynającą się w stanie $s_{i}{:}$ $x_{i}=\{s_{i},s_{i+1},s_{i+2},\dots \}$

Język

• wszystkie składniki logiki LTL,
• operatory ścieżkowe:
  • $A$ – $A\alpha$ dla każdej ścieżki czasu prawdziwe jest $\alpha$
  • $E$ – $E\alpha$ istnieje taka ścieżka czasu, dla której prawdziwe jest $\alpha$ $(E\alpha \equiv \neg A\neg \alpha )$

Formuły

Niech $WA$ będzie zbiorem wyrażeń atomowych.

• każde wyrażenie $\alpha \in WA$ jest formułą stanową
• jeśli $\alpha _{1}$ i $\alpha _{2}$ są formułami stanowymi, to $\alpha \wedge \beta$ i $\neg \alpha$ też są formułami stanowymi
• jeśli $\alpha _{1}$ i $\alpha _{2}$ są formułami stanowymi, to $\alpha U\beta$ i $X\alpha$ też są formułami stanowymi
• jeśli $\alpha$ jest formułą ścieżkową, to $A\alpha$ i $E\alpha$ są formułami stanowymi
• jeśli $\alpha$ i $\beta$ są formułami ścieżkowymi, to $\alpha \wedge \beta ,$ $\neg \alpha ,$ $\alpha U\beta$ i $X\alpha$ też są formułami ścieżkowymi
• każda formuła stanowa jest formułą ścieżkową

Oznacza to, że każda formuła w CTL* musi zaczynać się od operatora ścieżkowego $A$ lub $E$

Prawdziwość formuł

• oznaczenia:

$(M,s)\models \alpha$ – formuła stanowa $\alpha$ jest prawdziwa w strukturze $M$ w stanie $s$
$(M,x)\models \beta$ – formuła ścieżkowa $\beta$ jest prawdziwa w strukturze $M$ na ścieżce $x$

• warunki prawdziwości podstawowych formuł:

$(M,s)\models p\Leftrightarrow p\in L(s)$
$(M,s)\models \alpha _{1}\wedge \alpha _{2}\Leftrightarrow (M,s)\models \alpha _{1}\wedge (M,s)\models \alpha _{2}$
$(M,s)\models \neg \alpha \Leftrightarrow \neg (M,s)\models \alpha$
$(M,s)\models E\beta \Leftrightarrow \beta$ jest prawdziwe dla jakiejś ścieżki $x$ rozpoczynającej się w stanie $s$
$(M,s)\models A\beta \Leftrightarrow \beta$ jest prawdziwe dla każdej ścieżki $x$ rozpoczynającej się w stanie $s$
$(M,x)\models \alpha \Leftrightarrow (M,s_{0})\models \alpha$
$(M,x)\models \beta _{1}\wedge \beta _{2}\Leftrightarrow (M,x)\models \beta _{1}\wedge (M,x)\models \beta _{2}$
$(M,x)\models \neg \beta \Leftrightarrow \neg (M,x)\models \beta$
$(M,x)\models \beta _{1}U\beta _{2}\Leftrightarrow \exists _{k\geq 0}((M,x_{k})\models \beta _{2}\wedge \forall j:(0\leq j<k)\quad (M,x_{j})\models \beta _{1})$
$(M,x)\models X\beta \Leftrightarrow (M,x_{1})\models \beta$

Linki zewnętrzne

• Model Checking II Temporal Logic Model Checking