生成诊断公式的有限状态进程等价验证
Data(s) |
2010
|
---|---|
Resumo |
分析有限状态进程互模拟等价判定技术,探讨了诊断公式的生成问题。给出了将有限状态进程转化为带标号的迁移系统,修改了Paige和Trajan求解最粗划分的算法,使其适用于带标号的迁移系统。给出生成Hennessy-Milner逻辑描述的诊断公式的算法,当两个进程不能互模拟时,产生两个诊断公式。算法的时间复杂度为O(mlogn),空间复杂度为O(m+n)。 |
Identificador | |
Idioma(s) |
中文 |
Fonte |
李明.生成诊断公式的有限状态进程等价验证,计算机工程与设计,2010,31(2):344-347 |
Palavras-Chave | #互模拟 #形式验证 #带标号的迁移系统 #有限状态进程 #Hennessy-Milner逻辑 |
Tipo |
期刊论文 |