论文部分内容阅读
分析有限状态进程互模拟等价判定技术，探讨了诊断公式的生成问题。给出了将有限状态进程转化为带标号的迁移系统，修改了Paige和Trajan求解最粗划分的算法，使其适用于带标号的迁移系统。给出生成Hennessy—Milner逻辑描述的诊断公式的算法，当两个进程不能互模拟时，产生两个诊断公式。算法的时间复杂度为O（mlogn），空间复杂度为0（m＋n）。