逻辑标记转换系统下预备模拟与稳定划分

来源：计算机科学与探索杂志2015年第7期北京时间：

作者：朱文涛

单位：南京航空航天大学 计算机科学与技术学院，南京 210016

摘要：Luttgen等人将进程代数与时序逻辑相结合，提出了逻辑标记转换系统（logic labeled transition system，LLTS）以及相应的精化关系——LLTS预备模拟。为给出判定LLTS预备模拟关系的具体方法，从划分对概念出发，给出了与LLTS预备模拟之间构成同构的稳定划分对定义，并提出了与判定LLTS预备模拟商集对应的一般化关系最粗划分问题，证明了二者之间具有等价性。由此作为理论基础，给出了一个判定两个逻辑标记转换系统之间是否具有LLTS预备模拟关系的算子ρ，并验证了该算子的正确性，并以实例演示了该算子的具体操作步骤。

关键词：逻辑标记转换系统,预备模拟,划分对,划分精化问题