论文部分内容阅读
论文包括两部分内容,第一部分通过定义分解互模拟这个概念,对规范的(normed)上下文无关进程上的互模拟做了更为简单的有限刻画,并且对我们定义的分解互模拟这个概念进行了博弈刻画。第二部分对模态μ演算上的可满足性问题进行了博弈刻画,对可满足性公式可以进行模型构建,对不可满足公式可以生成反例。而且我们尝试设计了一种基于我们定义的可满足性博弈(Satisfiability Game)的对一类模态μ演算公式的模型检测算法。