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