An axiomatization of ECTL
Ryo Kashima · Journal of Logic and Computation · 2013
ECTL is an extension of the computation tree logic (CTL) with two operators ∃GF and ∀FG where ∃GFϕ and ∀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 ∀G(ϕ → ψ ) → (∃GFϕ → ∃GFψ), ∃GFϕ ↔ ∃F(ϕ ∧ ∃X∃GFϕ), ∀G(ϕ → ∃X∃Fψ) → (ψ → ∃GFϕ) and ∀FGϕ ↔ ¬ ∃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: (i) ϕ is provable in this axiomatization of ECTL; (ii) ϕ is valid in any model; (iii) ϕ is valid in any finite model.