Technical Reports

A List by Author: Joakim Byg

e-mail:

joakim.byg(a)gmail.com

An Efficient Translation of Timed-Arc Petri Nets to Networks of Timed Automata

by Joakim Byg, Kenneth Yrke Joergensen, Jiøí Srba, A full version of the paper presented at ICFEM`09. October 2009, 29 pages.

FIMU-RS-2009-06. Available as Postscript, PDF.

Abstract:

Bounded timed-arc Petri nets with read-arcs were recently proven equivalent to net- works of timed automata, though the Petri net model cannot express urgent be- haviour 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 trans- lation 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.