%0 Journal Article
%T Model Checking of Timed Colored Petri Nets with Inhibitor Arcs<br>带抑制弧的时延着色Petri网模型检测技术
%A YANG Nian-hua
%A YU Hui-qun
%A SUN Hua
%A <br>杨年华
%A 虞慧群
%A 孙华
%J 计算机科学
%D 2011
%I 
%X 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.
%K Timed colored Petri net
%K Inhibitor arc
%K Timed automaton
%K Collision mediation
%K Model checking<br>时延着色Petri网，抑制弧，时间自动机，冲突调解，模型检测
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=64A12D73428C8B8DBFB978D04DFEB3C1&aid=E5BD50857AD31F16AB97FE5B9AC1F23C&yid=9377ED8094509821&vid=16D8618C6164A3ED&iid=CA4FD0336C81A37A&sid=C5F8B8CB20F1B3D8&eid=5BC9492E1D772407&journal_id=1002-137X&journal_name=计算机科学&referenced_num=0&reference_num=21