Clausal reasoning for branching-time logics
Clausal reasoning for branching-time logics
复制标题
DOI：
--
复制
发表时间：
2010-12
期刊：
影响因子：
--
通讯作者：
Lan Zhang
中科院分区：
文献类型：
--
作者：
Lan Zhang
计算树逻辑（CTL）是一种分支时间时序逻辑，其时间的底层模型是对分支到未来的可能性的选择。它已广泛应用于计算机科学和人工智能领域，例如时态数据库、硬件验证、程序推理、多代理系统以及并发和分布式系统。在本文中，我们首先提出了一种针对 CTL 的改进的分句解析演算 R�,S CTL。该微积分需要将任意 CTL 公式进行多项式时间可计算变换为可等满足的子句范式，该形式在带有索引存在路径量词的 CTL 扩展中表述。微积分本身由八步解析规则、两个偶发性解析规则和两个重写规则组成，可以用作 CTL 可满足性问题的 EXPTIME 决策过程的基础。我们给出了子句范式的形式语义，证明了子句范式变换保留了可满足性，为演算 R�,S CTL 的健全性和完整性提供了证明，并讨论了基于 R�,S CTL 的决策过程的复杂性。由于 R�,S CTL 基于 Bolotov 的 CTL 分句消解演算的思想，我们提供了我们的演算 R�,S CTL 和 Bolotov 的 CTL 演算之间的比较，以表明 R�,S CTL 在许多领域改进了 Bolotov 的演算。特别是，我们的微积分旨在允许一阶解析技术模拟 R�,S CTL 的解析规则，以便可以通过重用任何一阶解析定理证明来实现 R�,S CTL。其次，我们介绍 CTL-RP，即我们对 R�,S CTL 微积分的实现。 CTL-RP 是第一个针对 CTL 实现的基于解析的定理证明器。证明者将任意 CTL 公式作为输入，并将其转换为一组子句范式的 CTL 公式。此外，为了使用一阶技术，子句范式中的公式被转换为一阶公式，除了那些与事件相关的公式，即包含事件运算符3的公式。为了实现步骤解析并重写微积分R�,S CTL的规则，我们提出了一种使用一阶有序解析和选择来模拟步骤解析规则和相关证明的方法。这种方法使我们能够利用一阶定理证明器，它通过选择实现一阶有序解析，以实现我们的微积分。按照这种方法，CTL-RP 利用一阶定理证明器 SPASS 对 CTL 进行解析推理，并作为 SPASS 的修改来实现。特别是，为了实现偶发事件解决规则，CTL-RP 使用一种称为循环搜索算法的算法来增强 SPASS，用于处理 CTL 中的偶发事件。为了研究 CTL-RP 的性能，我们将 CTL-RP 与基于 tableau 的 CTL 定理证明器进行了比较。实验表明CTL-RP具有良好的性能。 i ii 摘要 第三，我们将用于开发 R�,S CTL 的方法应用于开发交替时间时序逻辑 (ATL) 片段的子句解析演算。 ATL 是分支时间时序逻辑的概括和扩展，其中时序运算符由代理集参数化。非正式地说，CTL 公式可以视为具有单一代理的 ATL 公式。对路径的选择性量化使 ATL 能够明确地表达联盟能力，这自然使 ATL 成为开放系统和类似游戏的多智能体系统的规范和验证的形式主义。在本文中，我们重点关注ATL的Next-time片段（XATL），它与联盟逻辑密切相关。 XATL的可满足性问题虽然比ATL复杂度低，但在各种策略博弈和多智能体系统中仍然有很多应用可以用XATL来表示和推理。在本文中，我们提出了 XATL 的解析演算 RXATL 来解决其可满足性问题。该微积分需要将任意 XATL 公式进行多项式时间可计算转换为可等满足的子句范式。微积分本身由一组解析规则和重写规则组成。我们证明了微积分的可靠性，并概述了微积分 RXATL 的完整性证明。此外，我们打算将来将我们的微积分 RXATL 扩展到完整的 ATL。
Computation Tree Logic (CTL) is a branching-time temporal logic whose underlying model of time is a choice of possibilities branching into the future. It has been used in a wide variety of areas in Computer Science and Artificial Intelligence, such as temporal databases, hardware verification, program reasoning, multi-agent systems, and concurrent and distributed systems. In this thesis, firstly we present a refined clausal resolution calculus R�,S CTL for CTL. The calculus requires a polynomial time computable transformation of an arbitrary CTL formula to an equisatisfiable clausal normal form formulated in an extension of CTL with indexed existential path quantifiers. The calculus itself consists of eight step resolution rules, two eventuality resolution rules and two rewrite rules, which can be used as the basis for an EXPTIME decision procedure for the satisfiability problem of CTL. We give a formal semantics for the clausal normal form, establish that the clausal normal form transformation preserves satisfiability, provide proofs for the soundness and completeness of the calculus R�,S CTL, and discuss the complexity of the decision procedure based on R�,S CTL. As R�,S CTL is based on the ideas underlying Bolotov’s clausal resolution calculus for CTL, we provide a comparison between our calculus R�,S CTL and Bolotov’s calculus for CTL in order to show that R�,S CTL improves Bolotov’s calculus in many areas. In particular, our calculus is designed to allow first-order resolution techniques to emulate resolution rules of R�,S CTL so that R�,S CTL can be implemented by reusing any first-order resolution theorem prover. Secondly, we introduce CTL-RP, our implementation of the calculus R�,S CTL. CTL-RP is the first implemented resolution-based theorem prover for CTL. The prover takes an arbitrary CTL formula as input and transforms it into a set of CTL formulae in clausal normal form. Furthermore, in order to use first-order techniques, formulae in clausal normal form are transformed into firstorder formulae, except for those formulae related to eventualities, i.e. formulae containing the eventuality operator 3. To implement step resolution and rewrite rules of the calculus R�,S CTL, we present an approach that uses first-order ordered resolution with selection to emulate the step resolution rules and related proofs. This approach enables us to make use of a first-order theorem prover, which implements the first-order ordered resolution with selection, in order to realise our calculus. Following this approach, CTL-RP utilises the first-order theorem prover SPASS to conduct resolution inferences for CTL and is implemented as a modification of SPASS. In particular, to implement the eventuality resolution rules, CTL-RP augments SPASS with an algorithm, called loop search algorithm for tackling eventualities in CTL. To study the performance of CTL-RP, we have compared CTL-RP with a tableau-based theorem prover for CTL. The experiments show good performance of CTL-RP. i ii ABSTRACT Thirdly, we apply the approach we used to develop R�,S CTL to the development of a clausal resolution calculus for a fragment of Alternating-time Temporal Logic (ATL). ATL is a generalisation and extension of branching-time temporal logic, in which the temporal operators are parameterised by sets of agents. Informally speaking, CTL formulae can be treated as ATL formulae with a single agent. Selective quantification over paths enables ATL to explicitly express coalition abilities, which naturally makes ATL a formalism for specification and verification of open systems and game-like multi-agent systems. In this thesis, we focus on the Next-time fragment of ATL (XATL), which is closely related to Coalition Logic. The satisfiability problem of XATL has lower complexity than ATL but there are still many applications in various strategic games and multi-agent systems that can be represented in and reasoned about in XATL. In this thesis, we present a resolution calculus RXATL for XATL to tackle its satisfiability problem. The calculus requires a polynomial time computable transformation of an arbitrary XATL formula to an equi-satisfiable clausal normal form. The calculus itself consists of a set of resolution rules and rewrite rules. We prove the soundness of the calculus and outline a completeness proof for the calculus RXATL. Also, we intend to extend our calculus RXATL to full ATL in the future.