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 ${\displaystyle M=(S,R,L),}$ gdzie:

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

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

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

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

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

Język

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

Formuły

Niech ${\displaystyle WA}$ będzie zbiorem wyrażeń atomowych.

• każde wyrażenie ${\displaystyle \alpha \in WA}$ jest formułą stanową
• jeśli ${\displaystyle \alpha _{1}}$ i ${\displaystyle \alpha _{2}}$ są formułami stanowymi, to ${\displaystyle \alpha \wedge \beta }$ i ${\displaystyle \neg \alpha }$ też są formułami stanowymi
• jeśli ${\displaystyle \alpha _{1}}$ i ${\displaystyle \alpha _{2}}$ są formułami stanowymi, to ${\displaystyle \alpha U\beta }$ i ${\displaystyle X\alpha }$ też są formułami stanowymi
• jeśli ${\displaystyle \alpha }$ jest formułą ścieżkową, to ${\displaystyle A\alpha }$ i ${\displaystyle E\alpha }$ są formułami stanowymi
• jeśli ${\displaystyle \alpha }$ i ${\displaystyle \beta }$ są formułami ścieżkowymi, to ${\displaystyle \alpha \wedge \beta ,}$ ${\displaystyle \neg \alpha ,}$ ${\displaystyle \alpha U\beta }$ i ${\displaystyle 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 ${\displaystyle A}$ lub ${\displaystyle E}$

Prawdziwość formuł

• oznaczenia:

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

• warunki prawdziwości podstawowych formuł:

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

Linki zewnętrzne

• Model Checking II Temporal Logic Model Checking