不动点逻辑中的模型构造与推演系统的完备性
文献类型：学位论文
| 作者 | 屈楠 |
| 学位类别 | 博士 |
| 答辩日期 | 2012-05-31 |
| 授予单位 | 中国科学院研究生院 |
| 授予地点 | 北京 |
| 导师 | 柳欣欣 |
| 关键词 | mu-演算 可满足性 模型构造 公理系统 完备性 |
| 学位专业 | 计算机理论基础 |
| 中文摘要 | 与$LTL$、$CTL$以及$PDL$等较简单的时序与模态逻辑相比，$\mu$-演算由于含有不动点算子，拥有非常强大的表达能力，因而付出的代价是其可满足性的判定、模型的构造 以及对应公理系统的完备性都较为复杂。本文主要利用两种不同的方法，来研究$\mu$-演算的这些问题。 首先，本文使用基于正规模型(canonic model)的方法尝试证明D. Kozen提出的$\mu$-演算上的一个公理系统$K\mu$的完备性。这一方法的基本思想，是利用称之为极大协调集 的公式集合作为状态来构造模型。其中极大协调集是指在某个公式的Fisher-Ladner闭包上极大的且无法由$K\mu$推导出矛盾的公式集合。这一方法的要点在于证明极大协调集作为 正规模型的状态，满足其中的每一个公式。因此不可满足的公式一定不能存在于任何极大协调集中，因而可以被$K\mu$证明等价于假。本文指出直接使用这一方法对于 $\mu$-演算中的公式全体是不能奏效的，但是可以在其满足连续性的公式上奏效。 其次，本文使用基于tableau的方法来构造$\mu$-演算公式的模型。Tableau方法作为一种非常强大的技术，已经广泛地用于逻辑系统的可满足性判定与模型构造之中。本文 基于\cite{Jungteerapanich09,Walukiewicz93}的工作，提出了一种较为简单的Tableau系统。在这一系统中，可满足公式可以构造出成功的tableau，而不可满足的公式不存在 成功的tableau。根据一个公式的成功tableau，可以直接地提取出这个公式的模型，并且模型的规模被tableau的规模约束。本文给出了$\mu$-演算公式的最小模型相对于公式 规模函数的一个上界与一个下界。 本文还附带了一个对于CCS的推广。这一推广与CCS最根本的区别在于其允许一对多的树状迁移。本文给出了树进程的语法定义、操作语义及其上的互模拟关系，并给出了一个可 靠且完备的推理系统来证明其上的互模拟关系。 |
| 英文摘要 | Comparing with some easier temporal logic or modal logic such as $LTL$, $CTL$ or $PDL$, the $\mu$-calculus is very powerful in expressiveness, since the syntax contains fixed-point construction. The price paid is that the decidability of satisfiability, model construction and the completeness of its inference system become more complex. In this thesis, two different method are used to analyze these question. First, a method based on the canonic model is launched to try to prove the completeness of D. Kozon's axiomatization. The basic idea is to use the so called maximum consistent sets as states to construct a model. Here a maximum consistent set is a maximum set upon the Fisher-Ladner closure which can not deduce to contradiction within $K\mu$. The key point of this method is to prove that a maximum consistent set as a state of the canonic model satisfies every formula in it. Then a formula which can never be satisfied must equivalent to false in the deduction system $K\mu$. In this thesis, it is pointed out that the method can only work on a subset of formulae which are continuous instead of the entire $\mu$-calculus. Second, in this thesis a method based on tableau is used to construct models for formulae. Tableau method, as a powerful technique, has been applied widely in the area about decidability and model checking. Based on \cite{Jungteerapanich09,Walukiewicz93}, a simpler system is given. In this system, a formula is satisfiable if and only if there is a successful tableau for it. A model can be restracted straightforward from a successful tableau, and the size of model is bounded by the size of tableau. An upper bound and a lower bound are given. In this thesis we also present an extension of CCS. The extension differs from the original version in that tree-like transitions are allowed. The syntax, operational semantic and bisimulaion are defined with a sound and complete inference system. |
| 学科主题 | 计算机科学技术基础学科 |
| 语种 | 英语 |
| 公开日期 | 2012-07-06 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/14554]  |
| 专题 | 软件研究所_计算机科学国家重点实验室 _学位论文 |
| 推荐引用方式 GB/T 7714 | 屈楠. 不动点逻辑中的模型构造与推演系统的完备性[D]. 北京. 中国科学院研究生院. 2012. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。