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

摘要

Luttgen et al. combined process algebras and temporal logics to propose the notion of logic labeled transi-tion system (LLTS) and corresponding refinement relation:LLTS ready simulation. To give a method to determine LLTS ready simulation between different states, based on the concept of partition pair, this paper brings a notion of stable partition pair which is isomorphic to LLTS ready simulation, and proposes the coarsest partition problem of generalization relation, then proves the equivalence between this notion and the LLTS ready simulation quotient. From this equivalence, this paper presents a calculus ρ to determine LLTS ready simulation relation between two logic labeled transition systems, and gives the correctness of this calculus. Finally, this paper presents a realistic example to show how this calculus operates.%Luttgen等人将进程代数与时序逻辑相结合，提出了逻辑标记转换系统（logic labeled transition system， LLTS）以及相应的精化关系——LLTS预备模拟。为给出判定LLTS预备模拟关系的具体方法，从划分对概念出发，给出了与LLTS预备模拟之间构成同构的稳定划分对定义，并提出了与判定LLTS预备模拟商集对应的一般化关系最粗划分问题，证明了二者之间具有等价性。由此作为理论基础，给出了一个判定两个逻辑标记转换系统之间是否具有LLTS预备模拟关系的算子ρ，并验证了该算子的正确性，并以实例演示了该算子的具体操作步骤。