您的位置: 首页 > 文章 > Model Checking for CTL(二) Model Checking for CTL(二) 分类: 文章 • 2023-09-16 23:47:49 2.4 Model checking algorithms for CTL 2.4.1 Existential Normal Form 所有CLT公式都可以用“存在”形式来表达。 ∀XΦ = ¬∃X¬Φ ∀(Φ U Ψ) = ¬∃(¬Ψ U (¬Φ ∧ ¬Ψ)) ∧ ¬∃