带抑制弧的时延着色Petri网模型检测技术

计算机科学 ›› 2011, Vol. 38 ›› Issue (1): 170-176.

带抑制弧的时延着色Petri网模型检测技术

杨年华,虞慧群,孙华

(华东理工大学计算机科学与工程系上海200237);(上海市计算机软件评测重点实验室上海201112)

出版日期:2018-11-16 发布日期:2018-11-16
基金资助:
本文受国家自然科学基金(60473055,60773094)，上海市曙光计划(07SG32)资助。

Model Checking of Timed Colored Petri Nets with Inhibitor Arcs

YANG Nian-hua,YU Hui-qun,SUN Hua

Online:2018-11-16 Published:2018-11-16

摘要/Abstract

摘要： 带抑制弧的时延着色Petri网(Timed Colored Petri Nets with Inhibitor Arcs,TCPNIA)是一种描述实时嵌入式系统的模型。给出了从TCPNIA到时间自动机的结构化转换算法，以利用变迁冲突调解机制保证TCPNIA模型和转换后的时间自动机模型语义等价；并给出了语义等价的证明和算法复杂度分析。层次化方法被用来提高模型检测的时间与空间效率。通过实际案例展示了该技术的应用和可行性。

关键词: 时延着色Petri网，抑制弧，时间自动机，冲突调解，模型检测

Abstract: TCPNIA(Timed Colored Petri Nets with Inhibitor Arcs,TCPNIA) is a model for specifying embedded systerns. This paper proposed a structural transformation method from TCPNIA to TA(Timed Automata,TA). A collision mediation mechanism was introduced to ensure the semantics equivalence between TCPNIA and the transferred counter-part. I}he semantics equivalence was proved. The complexity of the transformation algorithm was analyzed. Hierarchical method was utilized to improve time and space efficiency in model checking. A case study shows the applicability and feasibility of the technique.

Key words: Timed colored Petri net, Inhibitor arc, Timed automaton, Collision mediation, Model checking

杨年华,虞慧群,孙华. 带抑制弧的时延着色Petri网模型检测技术[J]. 计算机科学, 2011, 38(1): 170-176. https://doi.org/

YANG Nian-hua,YU Hui-qun,SUN Hua. Model Checking of Timed Colored Petri Nets with Inhibitor Arcs[J]. Computer Science, 2011, 38(1): 170-176. https://doi.org/

参考文献

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed