An axiomatization of ECTL

摘要

ECTL is an extension of the computation tree logic (CTL) with two operators 3GF and z(V)FG where (E)GFφ and (V)FGψ represent 'there is a path along which φ holds infinitely often' and 'along any path, there exists a state after which ψ always holds', respectively. A Hilbert-style axiomatization of ECTL is defined by adding the schemata (V)G(φ→ψ)→((E)GFφ→(E)GFψ), (E)GFψ↔(E)F((φ∧(E)X(E)GFφ), (V)G(φ→(E)X(E)Fφ)→(φ→(E)GFφ) and (V)FGφ↔(E)GFφ to the axioms of CTL. We prove its soundness and completeness with respect to arbitrary and finite models, i.e. equivalence of the following three conditions: (ⅰ) φ is provable in this axiomatization of ECTL; (ⅱ) φ is valid in any model; (ⅲ) φ is valid in any finite model.