Axiomatising extended computation tree logic
We present a sound and complete axiomatisation for extended computation tree logic. This language extends the standard computation tree logic CTL* by allowing path formulae to be expressed in linear time mu-calculus instead of linear-time temporal logic. The main novelties in the current paper are an inference rule in the axiom system reflecting the limit closure of paths, a new strongly aconjunctive deterministic normal form for formulae, and the way the completeness proof takes advantage of techniques provided by automata theory.
axiomatisation completeness temporal logics limit closure