Supplement to Temporal Logic
Supplement: An Axiomatic System for CTL
To obtain a complete axiomatization of CTL it suffices to replace the axioms of the linear time temporal logic LTL by their path-quantified versions. For instance, the axioms characterizing the temporal operators G and U as fixed points now become:
- ∃Gφ↔(φ∧∃X∃Gφ);
- ∀Gφ↔(φ∧∀X∀Gφ);
- ∃(φUψ)↔(ψ∨(φ∧∃X∃(φUψ)));
- ∀(φUψ)↔(ψ∨(φ∧∀X∀(φUψ))).
The inference rules are modus ponens and the ∀G-necessitation rule: if ⊢φ, then ⊢∀Gφ.