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

Joakim Byg, Kenneth Yrke Jørgensen, Jiri Srba

Publikation: Bidrag til tidsskriftKonferenceartikel i tidsskriftForskningpeer review

16 Citationer (Scopus)

Abstrakt

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.
OriginalsprogEngelsk
BogserieLecture Notes in Computer Science
Vol/bind5885
Sider (fra-til)698-716
Antal sider18
ISSN0302-9743
DOI
StatusUdgivet - 2009
Begivenhed11th International Conference on Formal Engineering Methods (ICFEM'09) - Rio de Janeiro, Brasilien
Varighed: 8 dec. 200911 dec. 2009
Konferencens nummer: 11

Konference

Konference11th International Conference on Formal Engineering Methods (ICFEM'09)
Nummer11
LandBrasilien
ByRio de Janeiro
Periode08/12/200911/12/2009

Bibliografisk note

Titel:
11th International Conference on Formal Engineering Methods (ICFEM'09)

Oversat titel:


Oversat undertitel:


Forlag:
Springer

ISBN (Trykt):
978-3-642-10372-8

ISBN (Elektronisk):


Publikationsserier:
Lecture Notes in Computer Science, Lecture Notes in Comptuer Science, 0302-9743, 1611-3349, 5885

Emneord

  • timed-arc Petri nets
  • verification

Fingeraftryk Dyk ned i forskningsemnerne om 'An Efficient Translation of Timed-Arc Petri Nets to Networks of Timed Automata'. Sammen danner de et unikt fingeraftryk.

Citationsformater