CTL*

Last updated November 25, 2023

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 had 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 1983.^[1]

CTL and LTL were 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^{[ citation needed ]} 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 (with respect to bracketing) context-free grammar:

{\displaystyle \Phi

{\displaystyle \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 is 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

CTL* model checking (of an input formula on a fixed model) is PSPACE-complete ^[2] and the satisfiability problem is 2EXPTIME-complete.^[2]^[3]

Related Research Articles

Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions and relations between propositions, including the construction of arguments based on them. Compound propositions are formed by connecting propositions by logical connectives. Propositions that contain no logical connectives are called atomic propositions.

Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems of intuitionistic logic do not assume the law of the excluded middle and double negation elimination, which are fundamental inference rules in classical logic.

In mathematics, constructive analysis is mathematical analysis done according to some principles of constructive mathematics.

In logic, temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time. It is sometimes also used to refer to tense logic, a modal logic-based system of temporal logic introduced by Arthur Prior in the late 1950s, with important contributions by Hans Kamp. It has been further developed by computer scientists, notably Amir Pnueli, and logicians.

Computation tree logic (CTL) is a branching-time logic, meaning that its model of time is a tree-like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is realized. It is used in formal verification of software or hardware artifacts, typically by software applications known as model checkers, which determine if a given artifact possesses safety or liveness properties. For example, CTL can specify that when some initial condition is satisfied, then all possible executions of a program avoid some undesirable condition. In this example, the safety property could be verified by a model checker that explores all possible transitions out of program states satisfying the initial condition and ensures that all such executions satisfy the property. Computation tree logic belongs to a class of temporal logics that includes linear temporal logic (LTL). Although there are properties expressible only in CTL and properties expressible only in LTL, all properties expressible in either logic can also be expressed in CTL*.

In logic, a rule of inference is admissible in a formal system if the set of theorems of the system does not change when that rule is added to the existing rules of the system. In other words, every formula that can be derived using that rule is already derivable without that rule, so, in a sense, it is redundant. The concept of an admissible rule was introduced by Paul Lorenzen (1955).

Independence-friendly logic is an extension of classical first-order logic (FOL) by means of slashed quantifiers of the form $and, where is a finite set of variables. The intended reading of is "there is a which is functionally independent from the variables in ". IF logic allows one to express more general patterns of dependence between variables than those which are implicit in first-order logic. This greater level of generality leads to an actual increase in expressive power; the set of IF sentences can characterize the same classes of structures as existential second-order logic.$

In mathematical logic, Heyting arithmetic $is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it.$

Epistemic modal logic is a subfield of modal logic that is concerned with reasoning about knowledge. While epistemology has a long philosophical tradition dating back to Ancient Greece, epistemic logic is a much more recent development with applications in many fields, including philosophy, theoretical computer science, artificial intelligence, economics and linguistics. While philosophers since Aristotle have discussed modal logic, and Medieval philosophers such as Avicenna, Ockham, and Duns Scotus developed many of their observations, it was C. I. Lewis who created the first symbolic and systematic approach to the topic, in 1912. It continued to mature as a field, reaching its modern form in 1963 with the work of Kripke.

In abstract algebraic logic, a branch of mathematical logic, the Leibniz operator is a tool used to classify deductive systems, which have a precise technical definition and capture a large number of logics. The Leibniz operator was introduced by Wim Blok and Don Pigozzi, two of the founders of the field, as a means to abstract the well-known Lindenbaum–Tarski process, that leads to the association of Boolean algebras to classical propositional calculus, and make it applicable to as wide a variety of sentential logics as possible. It is an operator that assigns to a given theory of a given sentential logic, perceived as a term algebra with a consequence operation on its universe, the largest congruence on the algebra that is compatible with the theory.

Axiomatic constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. The same first-order language with " $" and " " of classical set theory is usually used, so this is not to be confused with a constructive types approach. On the other hand, some constructive theories are indeed motivated by their interpretability in type theories.$

In mathematics, a set $is inhabited if there exists an element .$

In mathematical logic, a definable set is an n-ary relation on the domain of a structure whose elements satisfy some formula in the first-order language of that structure. A set can be defined with or without parameters, which are elements of the domain that can be referenced in the formula defining the relation.

In theoretical computer science, the modal μ-calculus is an extension of propositional modal logic by adding the least fixed point operator μ and the greatest fixed point operator ν, thus a fixed-point logic.

Probabilistic Computation Tree Logic (PCTL) is an extension of computation tree logic (CTL) that allows for probabilistic quantification of described properties. It has been defined in the paper by Hansson and Jonsson.

Fair computational tree logic is conventional computational tree logic studied with explicit fairness constraints.

In logic, philosophy, and theoretical computer science, dynamic logic is an extension of modal logic capable of encoding properties of computer programs.

Dynamic epistemic logic (DEL) is a logical framework dealing with knowledge and information change. Typically, DEL focuses on situations involving multiple agents and studies how their knowledge changes when events occur. These events can change factual properties of the actual world : for example a red card is painted in blue. They can also bring about changes of knowledge without changing factual properties of the world : for example a card is revealed publicly to be red. Originally, DEL focused on epistemic events. We only present in this entry some of the basic ideas of the original DEL framework; more details about DEL in general can be found in the references.

Metric temporal logic (MTL) is a special case of temporal logic. It is an extension of temporal logic in which temporal operators are replaced by time-constrained versions like until, next, since and previous operators. It is a linear-time logic that assumes both the interleaving and fictitious-clock abstractions. It is defined over a point-based weakly-monotonic integer-time semantics.

In model checking, a field of computer science, timed propositional temporal logic (TPTL) is an extension of propositional linear temporal logic (LTL) in which variables are introduced to measure times between two events. For example, while LTL allows to state that each event p is eventually followed by an event q, TPTL furthermore allows to give a time limit for q to occur.

References

↑ Emerson, E. Allen; Halpern, Joseph Y. (1983). ""Sometimes" and "Not Never" revisited". Proceedings of the 10th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL '83. pp. 127–140. doi:10.1145/567067.567081. ISBN 0897910907. S2CID 15728260.
1 2 Baier, Christel; Katoen, Joost-Pieter (2008-01-01). Principles of Model Checking (Representation and Mind Series). The MIT Press. ISBN 978-0262026499.
↑ Orna Kupferman; Moshe Y. Vardi (June 1999). "Church's problem revisited". Bulletin of Symbolic Logic . 5 (2): 245–263. doi:10.2307/421091. JSTOR 421091. S2CID 18833301.

Amir Pnueli: The temporal logic of programs. Proceedings of the 18th IEEE 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. Journal of the 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 page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.

[EmersonHalpern1983-1] Emerson, E. Allen; Halpern, Joseph Y. (1983). ""Sometimes" and "Not Never" revisited". Proceedings of the 10th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL '83. pp. 127–140. doi:10.1145/567067.567081. ISBN 0897910907. S2CID 15728260.

[:0-2] 1 2 Baier, Christel; Katoen, Joost-Pieter (2008-01-01). Principles of Model Checking (Representation and Mind Series). The MIT Press. ISBN 978-0262026499.

[3] Orna Kupferman; Moshe Y. Vardi (June 1999). "Church's problem revisited". Bulletin of Symbolic Logic . 5 (2): 245–263. doi:10.2307/421091. JSTOR 421091. S2CID 18833301.

[1]

[2]

[3]