Computation tree logic

Computational tree logic (CTL) is a temporal logic. It is often used to express properties of a system in the context of formal verification or model checking.

It uses basic propositions, often called atomic propositions, as its building blocks to make statements about the states of a system. [TODO: give an example of an atomic proposition]. CTL then combines theses propositions into formulas using boolean combinators and temporal combinators.

The boolean operators used are "not" (¬), "and" (∧), "or" (∨), "conditional" (→), and "biconditional" (↔). "Not" is an unary operator, the rest are binary operators. Along with these boolean operators CTL formulas can make use of the boolean constants true and false.

The temporal combinators are $X,F,G,U,W,A$ and $E$.

If we assume $P$ is an atomic proposition.

$XP$ states that $P$ is satisfied in the next state (you can see X as standing for neXt). $FP$ states that $P$ is satisfied sometime in the future. GP states that P is always satisfied.