Computation Tree Logic

CTL formulas visualized

The Computation Tree Logic (CTL for short) is a temporal logic whose model of time has a tree-like structure. The temporal change of states and their properties is modeled by paths within this tree structure. The future has several paths here, although it is not specified which one will ultimately be implemented. Accordingly, statements can be made about possible developments.

The CTL is used to verify hardware and software, usually by model checkers .

The linear temporal logic (LTL) also belongs to the family of temporal logics , whereby only one future is possible here. A generalization of the two logics is called CTL *.

syntax

Minimal grammar

Let be a set of atomic statements (assertions), then each element is a CTL formula. Are and formulas, then , , , and . This defines the minimal grammar of CTL. As a rule, however, this is expanded to include the common Boolean operators , and , and some other temporal operators. ${\displaystyle AP}$ ${\displaystyle p\in AP}$ ${\displaystyle \phi }$ ${\displaystyle \psi }$ ${\displaystyle \neg \phi }$ ${\displaystyle \phi \lor \psi }$ ${\displaystyle {\text{EX}}\phi }$ ${\displaystyle {\text{EG}}\phi }$ ${\displaystyle \phi {\text{EU}}\psi }$ ${\displaystyle \land }$ ${\displaystyle \implies }$ ${\displaystyle \Leftrightarrow }$

Temporal operators

The extension of the minimal grammar by the following operators does not increase the power of the language , since all operators can be returned by transformations.

• Path operators:
  • ${\displaystyle A\phi }$- Follows on all paths ${\displaystyle \phi }$ (English: All )
  • ${\displaystyle E\phi }$- follows on at least one path ${\displaystyle \phi }$ (English: Exists )
• Path-specific operators:
  • ${\displaystyle X\phi }$- immediately follows ${\displaystyle \phi }$ (English: neXt state )
  • ${\displaystyle F\phi }$- sometime follows ${\displaystyle \phi }$ (English: some Future state or Finally )
  • ${\displaystyle G\phi }$- on the following path follows in each state ${\displaystyle \phi }$ ( globally )
  • ${\displaystyle \phi U\psi }$- follows until the status is reached (English: Until ) ${\displaystyle \phi }$ ${\displaystyle \psi }$
  • ${\displaystyle \phi W\psi }$- always follows or until the state is reached (English: Weak Until ) ${\displaystyle \phi }$ ${\displaystyle \psi }$

Path and path-specific operators can be combined with each other so that, for example, the following formulas result:

• ${\displaystyle EX\phi }$- applies in (at least) one next state ${\displaystyle \phi }$
• ${\displaystyle EF\phi }$- applies in (at least) one of the following states ${\displaystyle \phi }$
• ${\displaystyle EG\phi }$- There is (at least) one path, so that applies along the entire path ${\displaystyle \phi }$
• ${\displaystyle E[\phi U\psi ]}$- there is a path for which applies: until the first occurrence of applies ${\displaystyle \psi }$ ${\displaystyle \phi }$
• ${\displaystyle AX\phi }$- applies in every next state ${\displaystyle \phi }$
• ${\displaystyle AF\phi }$- one always reaches a state in which applies ${\displaystyle \phi }$
• ${\displaystyle AG\phi }$- applies on all paths in every state ${\displaystyle \phi }$
• ${\displaystyle A[\phi U\psi ]}$- it always applies until the first occurrence of ${\displaystyle \phi }$ ${\displaystyle \psi }$

semantics

CTL formulas are defined using transition systems. For a given sequence of states of the system (starting in state ), the operators are formally defined as follows, this is for fulfilled : ${\displaystyle T(s_{0})=s_{0},s_{1},\ldots }$ ${\displaystyle s_{0}}$ ${\displaystyle T(s_{0})\models \phi }$ ${\displaystyle T(s_{0})}$ ${\displaystyle \phi }$

• ${\displaystyle T(s_{0})\models \neg \phi \quad \Leftrightarrow \quad T(s_{0})\not \models \phi }$
• ${\displaystyle T(s_{0})\models \phi \lor \psi \quad \Leftrightarrow \quad T(s_{0})\models \phi {\text{ oder }}T(s_{0})\models \psi }$
• ${\displaystyle T(s_{0})\models EX\phi \quad \Leftrightarrow \quad T(s_{1})\models \phi }$
• ${\displaystyle T(s_{0})\models EG\phi \quad \Leftrightarrow \quad \forall i:T(s_{i})\models \phi }$
• ${\displaystyle T(s_{0})\models \phi EU\psi \quad \Leftrightarrow \quad \exists k:T(s_{k})\models \psi \land \forall i<k:T(s_{i})\models \phi }$

The transformations mentioned above make it possible to convert formulas into one another.

• ${\displaystyle \neg A\phi \equiv E\neg \phi }$
• ${\displaystyle \neg AF\phi \equiv EG\neg \phi }$
• ${\displaystyle \neg EF\phi \equiv AG\neg \phi }$
• ${\displaystyle \neg AX\phi \equiv EX\neg \phi }$
• ${\displaystyle AG\phi \equiv \phi \land AXAG\phi }$
• ${\displaystyle EG\phi \equiv \phi \land EXEG\phi }$
• ${\displaystyle AF\phi \equiv \phi \lor AXAF\phi }$
• ${\displaystyle EF\phi \equiv \phi \lor EXEF\phi }$
• ${\displaystyle A[\phi U\psi ]\equiv \psi \lor (\phi \land AXA[\phi U\psi ])}$
• ${\displaystyle E[\phi U\psi ]\equiv \psi \lor (\phi \land EXE[\phi U\psi ])}$

literature

• Clarke, Grumberg, Peled: Model Checking . MIT Press, 2000, ISBN 0-262-03270-8
• Rohit Kapur: CTL for Test Information of Digital ICS . Springer, 2002, ISBN 978-1-4020-7293-2
• B. Berard, Michel Bidoit, Alain Finkel: Systems and Software Verification. Model-checking Techniques and Tools. Springer, 2001, ISBN 3-540-41523-8
• M. Huth and M. Ryan: Logic in Computer Science - Modeling and Reasoning about Systems . Cambridge, 2004, ISBN 0-521-54310-X