生成诊断公式的有限状态进程等价验证

	生成诊断公式的有限状态进程等价验证
	李明
刊名	计算机工程与设计
	2010
卷号	31 期号:2 页码:344-347
关键词	互模拟形式验证带标号的迁移系统有限状态进程 Hennessy-Milner逻辑
ISSN号	1000-7024
其他题名	research of deciding bisimulation equivalence of finite state processes
中文摘要	分析有限状态进程互模拟等价判定技术,探讨了诊断公式的生成问题。给出了将有限状态进程转化为带标号的迁移系统,修改了Paige和Trajan求解最粗划分的算法,使其适用于带标号的迁移系统。给出生成Hennessy-Milner逻辑描述的诊断公式的算法,当两个进程不能互模拟时,产生两个诊断公式。算法的时间复杂度为O(mlogn),空间复杂度为O(m+n)。
语种	中文
公开日期	2011-05-23
内容类型	期刊论文
源URL	[http://124.16.136.157/handle/311060/10014]
专题	软件研究所_人机交互技术与智能信息处理实验室_期刊论文
推荐引用方式 GB/T 7714	李明. 生成诊断公式的有限状态进程等价验证[J]. 计算机工程与设计,2010,31(2):344-347.
APA	李明.(2010).生成诊断公式的有限状态进程等价验证.计算机工程与设计,31(2),344-347.
MLA	李明."生成诊断公式的有限状态进程等价验证".计算机工程与设计 31.2(2010):344-347.