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

Joakim Byg, Kenneth Yrke Jørgensen, Jiri Srba

Research output: Contribution to journalConference article in JournalResearchpeer-review

17 Citations (Scopus)

Abstract

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 trans- lations 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.
Original languageEnglish
Book seriesLecture Notes in Computer Science
Volume5885
Pages (from-to)698-716
Number of pages18
ISSN0302-9743
DOIs
Publication statusPublished - 2009
Event11th International Conference on Formal Engineering Methods (ICFEM'09) - Rio de Janeiro, Brazil
Duration: 8 Dec 200911 Dec 2009
Conference number: 11

Conference

Conference11th International Conference on Formal Engineering Methods (ICFEM'09)
Number11
Country/TerritoryBrazil
CityRio de Janeiro
Period08/12/200911/12/2009

Keywords

  • timed-arc Petri nets
  • verification

Fingerprint

Dive into the research topics of 'An Efficient Translation of Timed-Arc Petri Nets to Networks of Timed Automata'. Together they form a unique fingerprint.

Cite this