compositional verification of liveness property in inhibitor-arc connections of petri net systems

ISCAS OpenIR

	compositional verification of liveness property in inhibitor-arc connections of petri net systems
	Pu Fei
	2012
发表期刊	Journal of Software
ISSN	1796217X
卷号	7 期号:3 页码:499-507
摘要	Petri net systems synthesis can construct large systems without the requirement of reachability analysis so that it can reduce the high complexity of analyzing global system. In a synthesis process, such good properties of subsystems as liveness and deadlock-freeness etc, must be preserved in synthesized system. This paper focusses on liveness preservation in inhibitor-arc connection operations. The systems dynamic, concurrent behavior relation i.e. concurrent language relation in inhibitor-arc connections is stressed studied. The corresponding language relation formula is present and proved, and it can be applied to determine liveness of synthesized system in inhibitor-arc connection operations. Furthermore, some criteria are introduced, which are necessary and sufficient for liveness, to determine the liveness of global system by the same ones of local systems. Finally, some examples are given, illustrating the effectiveness of the proposed approach in modeling and analyzing of large systems. © 2012 ACADEMY PUBLISHER.
收录类别	ei
部门归属	(1) College of Computer and Information Engineering, Zhejiang Gongshang University, Hangzhou, China; (2) State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China
语种	英语
内容类型	期刊论文
URI标识	http://ir.iscas.ac.cn/handle/311060/14713
专题	中国科学院软件研究所
推荐引用方式 GB/T 7714	Pu Fei. compositional verification of liveness property in inhibitor-arc connections of petri net systems[J]. Journal of Software,2012,7(3):499-507.
APA	Pu Fei.(2012).compositional verification of liveness property in inhibitor-arc connections of petri net systems.Journal of Software,7(3),499-507.
MLA	Pu Fei."compositional verification of liveness property in inhibitor-arc connections of petri net systems".Journal of Software 7.3(2012):499-507.

条目包含的文件
文件名称/大小	文献类型	版本类型	开放类型	使用许可
5808-15274-1-PB.pdf（716KB）			开放获取	使用许可	请求全文