CTL*

CTL* is a superset of computational tree logic (CTL) and linear temporal logic (LTL). It freely combines path quantifiers and temporal operators. Like CTL, CTL* is a branching time logic. The formal semantics of CTL* formulae are defined with respect to a given Kripke structure.

History

LTL has been proposed for the verification of computer programs first by Amir Pnueli in 1977. Four years later in 1981 E. M. Clarke and E. A. Emerson invented CTL and CTL model checking. CTL* was defined by E. A. Emerson and Joseph Y. Halpern in 1986.

Interestingly, CTL and LTL have been developed independently before CTL*. Both sublogics have become standards in the model checking community, while CTL* is of practical importance because it provides an expressive testbed for representing and comparing these and other logics. This is surprising because the computational complexity of model checking in CTL* is not worse than that of LTL: they both lie in PSPACE.

Syntax

The language of well-formed CTL* formulae is generated by the following unambiguous (wrt bracketing) context-free grammar:

\Phi ::=\bot \mid \top \mid p\mid (\neg \Phi )\mid (\Phi \land \Phi )\mid (\Phi \lor \Phi )\mid (\Phi \Rightarrow \Phi )\mid (\Phi \Leftrightarrow \Phi )\mid A\phi \mid E\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 ]

where $p$ ranges over a set of atomic formulas. Valid CTL*-formulae are built using the nonterminal $\Phi$ . These formulae are called state formulae, while those created by the symbol $\phi$ are called path formulae. (The above grammar contains some redundancies; for example $\Phi \lor \Phi$ as well as implication and equivalence can be defined as just for Boolean algebras (or propositional logic) from negation and conjunction, and the temporal operators X and U are sufficient to define the other two.)

The operators basically are the same as in CTL. However, in CTL, every temporal operator ( $X,F,G,U$ ) has to be directly preceded by a quantifier, while in CTL* this is not required. The universal path quantifier may be defined in CTL* in the same way as for classical predicate calculus $A\phi =\neg E\neg \phi$ , although this in not possible in the CTL fragment.

Examples of formulae

CTL* formula that is neither in LTL or in CTL: $EX(p)\land AFG(p)$
LTL formula that is not in CTL: $\ AFG(p)$
CTL formula that is not in LTL: $\ EX(p)$
CTL* formula that is in CTL and LTL: $\ AG(p)$

Remark: When taking LTL as subset of CTL*, any LTL formula is implicitly prefixed with the universal path quantifier $\ A$

Semantics

The semantics of CTL* are defined with respect to some Kripke structure. As the names imply, state formulae are interpreted with respect to the states of this structure, while path formulae are interpreted over paths on it.

State formulae

If a state $s$ of the Kripke structure satisfies a state formula $\Phi$ it is denoted $s\models \Phi$ . This relation is defined inductively as follows:

${\Big (}({\mathcal {M}},s)\models \top {\Big )}\land {\Big (}({\mathcal {M}},s)\not \models \bot {\Big )}$
${\Big (}({\mathcal {M}},s)\models p{\Big )}\Leftrightarrow {\Big (}p\in L(s){\Big )}$
${\Big (}({\mathcal {M}},s)\models \neg \Phi {\Big )}\Leftrightarrow {\Big (}({\mathcal {M}},s)\not \models \Phi {\Big )}$
${\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 )}$
${\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 )}$
${\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 )}$
${\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}{\big )}{\Big )}{\bigg )}$
${\Big (}({\mathcal {M}},s)\models A\phi {\Big )}\Leftrightarrow {\Big (}\pi \models \phi$ for all paths $\ \pi$ starting in $s{\Big )}$
${\Big (}({\mathcal {M}},s)\models E\phi {\Big )}\Leftrightarrow {\Big (}\pi \models \phi$ for some path $\ \pi$ starting in $s{\Big )}$

Path formulae

The satisfaction relation $\pi \models \phi$ for path formulae $\ \phi$ and a path $\pi =s_{0}\to s_{1}\to \cdots$ is also defined inductively. For this, let $\ \pi [n]$ denote the sub-path $s_{n}\to s_{n+1}\to \cdots$ :

${\Big (}\pi \models \Phi {\Big )}\Leftrightarrow {\Big (}({\mathcal {M}},s_{0})\models \Phi {\Big )}$
${\Big (}\pi \models \neg \phi {\Big )}\Leftrightarrow {\Big (}\pi \not \models \phi {\Big )}$
${\Big (}\pi \models \phi _{1}\land \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}\pi \models \phi _{1}{\big )}\land {\big (}\pi \models \phi _{2}{\big )}{\Big )}$
${\Big (}\pi \models \phi _{1}\lor \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}\pi \models \phi _{1}{\big )}\lor {\big (}\pi \models \phi _{2}{\big )}{\Big )}$
${\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 )}$
${\bigg (}\pi \models \phi _{1}\Leftrightarrow \phi _{2}{\bigg )}\Leftrightarrow {\bigg (}{\Big (}{\big (}\pi \models \phi _{1}{\big )}\land {\big (}\pi \models \phi _{2}{\big )}{\Big )}\lor {\Big (}\neg {\big (}\pi \models \phi _{1}{\big )}\land \neg {\big (}\pi \models \phi _{2}{\big )}{\Big )}{\bigg )}$
${\Big (}\pi \models X\phi {\Big )}\Leftrightarrow {\Big (}\pi [1]\models \phi {\Big )}$
${\Big (}\pi \models F\phi {\Big )}\Leftrightarrow {\Big (}\exists n\geqslant 0:\pi [n]\models \phi {\Big )}$
${\Big (}\pi \models G\phi {\Big )}\Leftrightarrow {\Big (}\forall n\geqslant 0:\pi [n]\models \phi {\Big )}$
${\Big (}\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]\models \phi _{1}{\big )}{\Big )}$

Decision problems

Model checking of CTL* is PSPACE-complete^[1] and satisfiability problem is in 2EXPTIME-complete.^[1]^[2]

References

1 2 Baier, Christel; Katoen, Joost-Pieter (2008-01-01). Principles of Model Checking (Representation and Mind Series). The MIT Press. ISBN 026202649X.
↑ "http://delivery.acm.org/10.1145/30000/22173/p240-vardi.pdf?ip=131.254.16.137&id=22173&acc=ACTIVE%2520SERVICE&key=7EBF6E77E86B478F%252E9BD6B3DBCD4B0A3B%252E4D4702B0C3E38B35%252E4D4702B0C3E38B35&CFID=839922977&CFTOKEN=84681748&__acm__=1474297820_4861bc9e061d390bb22019e6bb75c206" (PDF). doi:10.1145/30000/22173/p240-vardi.pdf. External link in |title= (help)

Amir Pnueli: The temporal logic of programs. 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: "Sometimes" and "not never" revisited: on branching versus linear time temporal logic. J. ACM 33, 1 (Jan. 1986), 151–178. DOI= http://doi.acm.org/10.1145/4904.4999
Ph. Schnoebelen: The Complexity of Temporal Logic Model Checking. Advances in Modal Logic 2002: 393–436

External links

CTL Teaching slides of professor Alessandro Artale at the Free University of Bozen-Bolzano

This article is issued from Wikipedia - version of the 9/20/2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.