CTL*

CTL* är en superuppsättning av beräkningsträdlogik (CTL) och linjär temporal logik (LTL). Den kombinerar fritt vägkvantifierare och temporala operatorer. Precis som CTL är CTL* en logik för förgreningstid. Den formella semantiken för CTL*-formler definieras med avseende på en given Kripke-struktur .

Historia

LTL hade föreslagits för verifiering av datorprogram, först av Amir Pnueli 1977. Fyra år senare, 1981, uppfann EM Clarke och EA Emerson CTL- och CTL -modellkontroll . CTL* definierades av EA Emerson och Joseph Y. Halpern 1983.

CTL och LTL utvecklades oberoende före CTL*. Båda sublogikerna har blivit standarder i modellkontrollgemenskapen , medan CTL* är av praktisk betydelse eftersom det ger en uttrycksfull testbädd för att representera och jämföra dessa och andra logiker. Detta är förvånande eftersom beräkningskomplexiteten för modellkontroll i CTL* inte är värre än för LTL: de ligger båda i PSPACE .

Syntax

Språket för välformade CTL*-formler genereras av följande otvetydiga (med avseende på parentes) kontextfri grammatik :

$\$

$:=\bot \mid \top \mid p\mid (\neg \Phi )\mid (\Phi \land \Phi )\mid (\Phi \lor \Phi )\mid (\Phi \Rightarrow \Phi )\$

$\phi ::=\Phi \mid (\neg \phi )\mid (\phi \land \phi )\mid (\phi \lor \phi )\mid (\phi \Rightarrow \phi )\mid (\phi \Leftrightarrow \phi )\mid X\phi \mid F\phi \mid G\phi \mid [\phi U\phi ]\mid [\phi R\phi ]$

där $p$ sträcker sig över en uppsättning atomformler . Giltiga CTL*-formler byggs med den icke-terminala $\Phi$ . Dessa formler kallas tillståndsformler , medan de som skapas av symbolen $\phi$ kallas sökvägsformler . (Ovanstående grammatik innehåller några redundanser; till exempel $\Phi \lor \Phi$ såväl som implikation och ekvivalens kan definieras som bara för booleska algebror (eller propositionslogik ) från negation och konjunktion, och den temporala operatorerna X och U är tillräckliga för att definiera de andra två .)

Operatörerna är i princip samma som i CTL . I CTL måste dock varje temporal operator ( $X,F,G,U$ ) direkt föregås av en kvantifierare, medan detta inte krävs i CTL*. Den universella vägkvantifieraren kan definieras i CTL* på samma sätt som för klassisk predikatkalkyl ${\displaystyle A\phi =\neg E\neg \phi } ,$ även om detta inte är möjligt i CTL fragment.

Exempel på formler

• CTL*-formel som varken finns i LTL eller i CTL: $EX(p)\land AFG(p)$
• LTL-formel som inte finns i CTL: $\ AFG(p)$
• CTL-formel som inte finns i LTL: $\ EX(p)$
• CTL*-formel som finns i CTL och LTL: $\ AG(p)$

Anmärkning: När du tar LTL som delmängd av CTL*, prefixes alla LTL-formler implicit med den universella sökvägskvantifieraren $A$ .

Semantik

Semantiken för CTL* definieras med avseende på någon Kripke-struktur . Som namnen antyder tolkas tillståndsformler med avseende på tillstånden för denna struktur, medan sökvägsformler tolkas över vägar på den.

Ange formler

Om ett tillstånd $s$ i Kripke-strukturen uppfyller en tillståndsformel $\Phi$ betecknas det $s\models \Phi$ . Denna relation definieras induktivt enligt följande:

1. ${\Big (}({\mathcal {M}},s)\modeller \top {\Big )}\land { \Big (}({\mathcal {M}},s)\inte \models \bot {\Big )}$
2. ${\Big (}({\mathcal {M}},s)\modeller p{\Big )}\Leftrightarrow {\Big (}p\in L(s){\Big )}$
3. ${\Big (}({\mathcal {M}},s)\modeller \neg \Phi {\Big )} \Leftrightarrow {\Big (}({\mathcal {M}},s)\not \models \Phi {\Big )}$
4. ${\Big (}({\mathcal { M}},s)\models \Phi _{1}\land \Phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s) \models \Phi _{1}{\big )}\land {\big (}({\mathcal {M}},s)\models \Phi _{2}{\big )}{\Big )}$
5. ${\Big (}({\mathcal { M}},s)\models \Phi _{1}\lor \Phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s) \models \Phi _{1}{\big )}\lor {\big (}({\mathcal {M}},s)\models \Phi _{2}{\big )}{\Big )}$
6. ${\Big (}({\mathcal M}},s)\models \Phi _{1}\Rightarrow \Phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s) \not \models \Phi _{1}{\big )}\lor {\big (}({\mathcal {M}},s)\models \Phi _{2}{\big )}{\Big ) }$
7. ${\bigg (}({\mathcal {M}},s)\models \Phi _{1}\Leftrightarrow \Phi _{2} {\bigg )}\Leftrightarrow {\bigg (}{\Big (}{\big (}({\mathcal {M}},s)\models \Phi _{1}{\big )}\land {\ big (}({\mathcal {M}},s)\models \Phi _{2}{\big )}{\Big )}\lor {\Big (}\neg {\big (}({\mathcal {M}},s)\models \Phi _{1}{\big )}\land \neg {\big (}({\mathcal {M}},s)\models \Phi _{2}{\ stor )}{\Big )}{\bigg )}$
8. ${\Big (}({\mathcal {M}},s)\models A\phi {\Big )}\Leftrightarrow {\Big ( }\pi \models \phi$ för alla sökvägar $\ \pi$ som börjar på $s{\Big )}$
9. ${\Big (}({\mathcal {M}},s)\models E\phi {\Big )}\Leftrightarrow {\Big ( }\pi \models \phi$ för någon väg $\ \pi$ som börjar på $s{\Big )}$

Sökvägsformler

Nöjdhetsrelationen $\pi \models \phi$ för sökvägsformler $\ \phi$ och en bana $\pi =s_{0}\to s_{1}\to \cdots$ definieras också induktivt. För detta, låt $\ \pi [n]$ beteckna undersökvägen $s_{n}\to s_{n+1}\to \ cdots$ :

1. ${\Big (}\pi \models \Phi {\Big )}\Leftrightarrow {\Big (}({\mathcal {M}}, s_{0})\models \Phi {\Big )}$
2. ${\Big (}\pi \models \neg \phi {\Big )}\Leftrightarrow {\Big (}\pi \not \models \phi {\ Stora )}$
3. ${\Big (}\pi \models \phi _{1}\land \phi _{2 }{\Big )}\Leftrightarrow {\Big (}{\big (}\pi \models \phi _{1}{\big )}\land {\big (}\pi \models \phi _{2} {\stor stor )}$
4. ${\Big (}\pi \models \phi _{1}\lor \phi _{2 }{\Big )}\Leftrightarrow {\Big (}{\big (}\pi \models \phi _{1}{\big )}\lor {\big (}\pi \models \phi _{2} {\stor stor )}$
5. ${\Big (}\pi \models \phi _{1}\Rightarrow \phi _{2} }{\Big )}\Leftrightarrow {\Big (}{\big (}\pi \not \models \phi _{1}{\big )}\lor {\big (}\pi \models \phi _{ 2}{\big )}{\Big )}$
6. $stil$
7. ${\Big (}\pi \models X\phi {\Big )}\Leftrightarrow {\Big (}\pi [1]\models \ phi {\Big )}$
8. ${\Big (}\pi \models F\phi {\Big )}\Leftrightarrow {\Big (}\exists n\ geqslant 0:\pi [n]\models \phi {\Big )}$
9. ${\Big (}\pi \models G\phi {\Big )}\Leftrightarrow {\Big (}\forall n\ geqslant 0:\pi [n]\modeller \phi {\Big )}$
10. $}\) pi \models [\phi _{1}U\phi _{2}]{\Big )}\Leftrightarrow {\Big (}\exists n\geqslant 0:{\big (}\pi [n]\models \ phi _{2}\land \forall 0\leqslant k<n:~\pi [k]\modeller \phi _{1}{\big )}{\Big )}}$

Beslutsproblem

Modellkontroll av CTL* är PSPACE-komplett och tillfredsställbarhetsproblemet är 2EXPTIME -komplett.

Se även

• Temporal logik
• Kripke struktur
• Modellkontroll
• Reo Coordination Language

• Amir Pnueli : Programs tidsmässiga logik. Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS), 1977, 46–57. DOI= 10.1109/SFCS.1977.32
• E. Allen Emerson , Joseph Y. Halpern : "Ibland" och "inte aldrig" återbesökt: om förgrening kontra linjär tid tidslogik. J. ACM 33, 1 (januari 1986), 151-178. DOI= http://doi.acm.org/10.1145/4904.4999
• Ph. Schnoebelen: Komplexiteten av kontroll av tidslogikmodeller. Advances in Modal Logic 2002: 393–436

externa länkar

• CTL Undervisningsbilder av professor Alessandro Artale vid Free University of Bozen-Bolzano