进程代数与时序逻辑是并发理论中应用最为广泛的两类规范系统,其中进程代数支持组合式的规范,而时序逻辑便于描述与验证系统的抽象性质。近来,Gerald Luttgen等人将二者进行结合,提出了逻辑标记转换系统以及该系统下进程项之间的精化关系——LLTS预备模拟关系。逻辑标记转换系统将操作式与逻辑式的规范结合到了统一的框架中,在通常的标记转换系统的基础上引入了进程之间的合取,并以协调性谓词标记由合取所产生的不协调进程,因而在支持组合式推理的同时还具有较强的表达能力。本文在充分考虑LLTS预备模拟相对于协调性谓词以及发散敏感的特性基础上,给出了判定不同逻辑标记转换系统之间是否具有LLTS预备模拟关系的算法,主要工作包括如下方面:1.引入划分对及其稳定性的定义,证明稳定划分对与LLTS预备模拟关系之间的等价性。基于该等价性,将判定不同逻辑标记转换系统之间LLTS预备模拟关系的问题转化为求解“最粗划分”问题,给出求解最粗划分的算子?,并证明其正确性。2.从更加一般化的角度看待LLTS预备模拟关系,提出与LLTS预备模拟关系等价的泛化预备模拟的定义,并证明了这一等价性。进而基于此定义,提出相应的划分对泛化稳定性以及最粗泛化稳定精化的概念,并证明了泛化稳定划分对与泛化预备模拟之间存在对应性。3.将划分对的泛化稳定性细分为“划分稳定性”与“关系稳定性”,并给出满足划分稳定性的等价条件,从而给出相对高效的划分对稳定性判别方法,并由此给出判定LLTS预备模拟的算法ERS,证明了该算法的正确性,并讨论了其时间及空间的复杂度。