模态逻辑公式为见证的互模拟等价判定

判定两个进程是否具有某种等价关系，是形式化验证的重要组成部分，很多种等价关系被定义出来以满足不同的验证需求，强互模拟等价和分支互模拟等价是其中两个重要的两种等价关系。强互模拟等价可以用HML(Hennessy-Milner Logic)逻辑刻画，分支互模 拟等价可以用HMLU(HML with Until)等逻辑刻画。两个模型不能强互模拟等价或者分支互模拟等价时，存在一个作为见证的相应逻辑描述的公式，该公式只能被其中一个模型满足，称之为诊断公式。诊断公式的意义在于有助于分析理解模型为什么不具有相应的等价关系，给出诊断公式是对判定算法有意义的扩充。修改后的PT(Paige-Tarjan)算法可以用于计算有限状态进程之间的强互模 拟等价关系，修改后的GV(Groote-Vaandrager)算法可以用于计算分支互模拟，对它们相应的扩充可以为不能强互模拟等价或分支互模拟等价的进程生成诊断公式。 主要工作如下：分析为强互模拟等价和分支互模拟等价生成诊断公式的方法。设计处理有限状态进程表达式并将其转化为标号迁移系统的算法。扩展PT 算法，使其适用于标号迁移系统，并在判定强互模拟等价的过程中为不能强互模拟的进程生成HML 描述的诊断公式。扩展GV 算法，使其能够在判定标号迁移系统上分支互模拟的同时，为不能分支互模拟的进程生成HMLU 描述的诊断公式。