An axiomatization of ECTL
An axiomatization of ECTL
复制标题
ECTL 的公理化
DOI：
10.1093/logcom/ext005
复制
发表时间：
2014
影响因子：
0.7
通讯作者：
Ryo Kashima
中科院分区：
文献类型：
--
作者：
J. Jarvinen;M. Kondo;J. Mattila and S. Radeleczki;Zhi-Zhong Chen;Ryo Kashima
ECTL是计算树逻辑（CTL）的扩展，它有两个运算符，分别表示“有一条路径沿着，它无穷地保持不变”和“沿着沿着任何路径，存在一个状态，在此状态之后，它总是保持不变”。ECTL的希尔伯特式公理化是通过在CTL的公理上增加模式<$G（→）→（<$GF → <$GF）、<$GF参与者F（<$GF X <$GF）、<$G（<$→ <$X <$GF）→（<$GF → <$GF）和<$GF参与者<$GF来定义的。我们证明了它的可靠性和完备性的任意和有限的模型，即以下三个条件的等价性：（i）在这个公理化的ECTL是可证明的;（ii）在任何模型中是有效的;（iii）在任何有限的模型中是有效的。
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.