Model Checking of Timed Colored Petri Nets with Inhibitor Arcs
带抑制弧的时延着色Petri网模型检测技术

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.