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) $\mathrm{\forall }x\in S\mathrm{\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\to \{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 ):\mathrm{\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 \mathrm{\neg }A\mathrm{\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 $\mathrm{\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 ,$ $\mathrm{\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\iff p\in L(s)$
$(M,s)\models {\alpha }_1\wedge {\alpha }_2\iff (M,s)\models {\alpha }_1\wedge (M,s)\models {\alpha }_2$
$(M,s)\models \mathrm{\neg }\alpha \iff \mathrm{\neg }(M,s)\models \alpha$
$(M,s)\models E\beta \iff \beta$ jest prawdziwe dla jakiejś ścieżki $x$ rozpoczynającej się w stanie $s$
$(M,s)\models A\beta \iff \beta$ jest prawdziwe dla każdej ścieżki $x$ rozpoczynającej się w stanie $s$
$(M,x)\models \alpha \iff (M,s_0)\models \alpha$
$(M,x)\models {\beta }_1\wedge {\beta }_2\iff (M,x)\models {\beta }_1\wedge (M,x)\models {\beta }_2$
$(M,x)\models \mathrm{\neg }\beta \iff \mathrm{\neg }(M,x)\models \beta$
$(M,x)\models {\beta }_{1}U{\beta }_2\iff {\mathrm{\exists }}_{k\ge 0}((M,x_k)\models {\beta }_2\wedge \mathrm{\forall }j:(0\le j<k)(M,x_j)\models {\beta }_1)$
$(M,x)\models X\beta \iff (M,x_1)\models \beta$

Linki zewnętrzne

• Model Checking II Temporal Logic Model Checking