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

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F09%3A00038053" target="_blank" >RIV/00216224:14330/09:00038053 - isvavai.cz</a>

Nalezeny alternativní kódy

RIV/00216224:14330/09:00067166

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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 oftimed-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.

Název v anglickém jazyce

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

Popis výsledku anglicky

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 oftimed-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.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/1M0545" target="_blank" >1M0545: Institut Teoretické Informatiky</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2009

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Proceedings of 11th International Conference on Formal Engineering Methods (ICFEM'09), pages 698-716 , volume 5885 of LNCS, Springer-Verlag, 2009.

ISBN

978-3-642-10372-8

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

18

Strana od-do

—

Název nakladatele

Springer Verlag

Místo vydání

Netherlands

Místo konání akce

Netherlands

Datum konání akce

1. 1. 2009

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—