论文部分内容阅读
与LTL、CTL以及PDL等较简单的时序与模态逻辑相比,μ-演算由于含有不动点算子,拥有非常强大的表达能力,因而付出的代价是其可满足性的判定、模型的构造以及对应公理系统的完备性都较为复杂。本文主要利用两种不同的方法,来研究μ-演算的这些问题。
首先,本文使用基于正规模型(canonicmodel)的方法尝试证明D.Kozen提出的μ-演算上的一个公理系统Kμ的完备性。这一方法的基本思想,是利用称之为极大协调集的公式集合作为状态来构造模型。其中极大协调集是指在某个公式的Fisher-Ladner闭包上极大的且无法由Kμ推导出矛盾的公式集合。这一方法的要点在于证明极大协调集作为正规模型的状态,满足其中的每一个公式。因此不可满足的公式一定不能存在于任何极大协调集中,因而可以被Kμ证明等价于假。本文指出直接使用这一方法对于μ-演算中的公式全体是不能奏效的,但是可以在其满足连续性的公式上奏效。
其次,本文使用基于tableau的方法来构造μ-演算公式的模型。Tableau方法作为一种非常强大的技术,已经广泛地用于逻辑系统的可满足性判定与模型构造之中。本文基于[33,34]的工作,提出了一种较为简单的Tableau系统。在这一系统中,可满足公式可以构造出成功的tableau,而不可满足的公式不存在成功的tableau。根据一个公式的成功tableau,可以直接地提取出这个公式的模型,并且模型的规模被tableau的规模约束。本文给出了μ-演算公式的最小模型相对于公式规模函数的一个上界与一个下界。
本文还附带了一个对于CCS的推广。这一推广与CCS最根本的区别在于其允许一对多的树状迁移。本文给出了树进程的语法定义、操作语义及其上的互模拟关系,并给出了一个可靠且完备的推理系统来证明其上的互模拟关系。