面向传值进程的一阶模态逻辑的可判定性与模型检测

	面向传值进程的一阶模态逻辑的可判定性与模型检测
	薛锐; 林惠民
	2003
发表期刊	中国科学E辑
ISSN	1006-9275
卷号	33 期号:2 页码:97-110
摘要	对于面向传值进程的Hennesssy-Milner逻辑的一阶扩充HML(FO)，给出了基于带赋值的符号迁移图的语义解释。证明了HML(FO)的子逻辑HML(FO^2)是满足性可判定的，并且讨论了判定的复杂性。最后给出了传值进程关于HML(FO^2)的模型检测的可判定性结果。
收录类别	wanfang,cscd
关键词	一阶模态逻辑可判定性模型检测传值进程
部门归属	计算机科学国家重点实验室
资助者	National Natural Science Foundation of China; Public Administration and Civil Service Bureau of Macau SAR; Companhia de Telecomunicacoes de Macau S.A.R.L.; Macau SAR Government Tourist Office
语种	中文
内容类型	期刊论文
URI标识	http://ir.iscas.ac.cn/handle/311060/4474
专题	基础软件与系统重点实验室
推荐引用方式 GB/T 7714	薛锐,林惠民. 面向传值进程的一阶模态逻辑的可判定性与模型检测[J]. 中国科学E辑,2003,33(2):97-110.
APA	薛锐,&林惠民.(2003).面向传值进程的一阶模态逻辑的可判定性与模型检测.中国科学E辑,33(2),97-110.
MLA	薛锐,et al."面向传值进程的一阶模态逻辑的可判定性与模型检测".中国科学E辑 33.2(2003):97-110.