论文部分内容阅读
本文中,我们首先简要总结一下代数、逻辑和博弈(或游戏)这三种作为描述抽象模型的方法各自所具有的特点,并且主要介绍Ehrenfeucht-Fra(l|¨)ss(?)游戏及其变体。然后我们将回顾一些重要的行为等价(或进程等价)关系以及它们的逻辑刻画,还包括由Rob J.Van Glabbeek提出的thelinear/branching time hierarchy。本文的核心内容是游戏阶层(game hierarchy),我们先给出一个游戏模板和一组游戏规则,通过它们之间不同的组合可以定义不同的游戏,而且每一个在the linear/branching timehierarchy中的等价关系都能找到一个上述的游戏来刻画。我们将以严格度来组织这些游戏,从而得到一个游戏阶层,其中的每一个游戏都对应了一种行为等价关系的游戏刻画。这种从游戏角度给出的阶层比the linear/branching time hierarchy更加细致。该项工作已发表在国际会议APLAS 2008上。本文的最后一部分将使用组合游戏来刻画行为等价关系。我们先定义两个基础的游戏以及四种组合运算,通过若干个基础游戏的不同组合方法,我们同样可以定义由游戏模板所定义的游戏,因此也能用来刻画行为等价关系。组合游戏的刻画方法比游戏模板更为细致,而且更加接近等价性检测算法的设计。