An Efficient Translation of Timed-Arc Petri Nets to Networks of Timed Automata
An Efficient Translation of Timed-Arc Petri Nets to Networks of Timed Automata
复制标题
时控弧 Petri 网到时控自动机网络的高效转换
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Jiri Srba
中科院分区：
文献类型：
--
作者：
Joakim Byg;K. Y. Jørgensen;Jiri Srba
最近证明，具有读取ARC的界定定时ARC Petri网等效于定时自动机网络，尽管Petri Net模型无法表达紧急行为，并且所描述的相互翻译效率相当低。我们提出了具有不变的定时ARC Petri网的扩展，以实施紧迫性和运输弧线以概括读取ARCS。我们还描述了从扩展的定时2培养皿网模型到定时自动机网络的一种新颖的翻译。该翻译是在工具Tapaal中实现的，并将Uppaal用作验证引擎。我们的实验证实了翻译的效率，在某些情况下，翻译模型的验证速度明显快于天然Uppaal模型。
Bounded timed-arc Petri nets with read-arcs were recently proven equivalent to networks of timed automata, though the Petri net model cannot express urgent behaviour and the described mutual translations are rather inefficient. We propose an extension of timed-arc Petri nets with invariants to enforce urgency and with transport arcs to generalise the read-arcs. We also describe a novel translation from the extended timed-arc Petri net model to networks of timed automata. The translation is implemented in the tool TAPAAL and it uses UPPAAL as the verification engine. Our experiments confirm the efficiency of the translation and in some cases the translated models verify significantly faster than the native UPPAAL models do.