中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 计算机科学国家重点实验室  > 学位论文
Subject: 计算机科学技术基础学科
Title:
不动点逻辑中的模型构造与推演系统的完备性
Author: 屈楠
Issued Date: 2012-05-31
Supervisor: 柳欣欣
Major: 计算机理论基础
Degree Grantor: 中国科学院研究生院
Place of Degree Grantor: 北京
Degree Level: 博士
Keyword: mu-演算 ; 可满足性 ; 模型构造 ; 公理系统 ; 完备性
Abstract: 与$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最根本的区别在于其允许一对多的树状迁移。本文给出了树进程的语法定义、操作语义及其上的互模拟关系,并给出了一个可
靠且完备的推理系统来证明其上的互模拟关系。
English Abstract: 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.
Language: 英语
Content Type: 学位论文
URI: http://ir.iscas.ac.cn/handle/311060/14554
Appears in Collections:计算机科学国家重点实验室 _学位论文

Files in This Item:
File Name/ File Size Content Type Version Access License
Finalversion.pdf(835KB)----限制开放 联系获取全文

Recommended Citation:
屈楠. 不动点逻辑中的模型构造与推演系统的完备性[D]. 北京. 中国科学院研究生院. 2012-05-31.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[屈楠]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[屈楠]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2019  中国科学院软件研究所 - Feedback
Powered by CSpace