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

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BYG Joakim JOERGENSEN Kenneth Yrke SRBA Jiří

Year of publication 2009
Type Article in Proceedings
Conference Proceedings of 11th International Conference on Formal Engineering Methods (ICFEM'09), pages 698-716 , volume 5885 of LNCS, Springer-Verlag, 2009.
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-642-10373-5_36
Field Informatics
Keywords timed-arc Petri nets; verification; timed automata
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.