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.

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.

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

where ${\displaystyle p}$ ranges over a set of atomic formulas. Valid CTL*-formulae are built using the nonterminal ${\displaystyle \Phi }$. These formulae are called state formulae, while those created by the symbol ${\displaystyle \phi }$ are called path formulae. (The above grammar contains some redundancies; for example ${\displaystyle \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.)

...
Wikipedia