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