A Forward Reachability Algorithm for Bounded Timed-Arc Petri
Nets

J 2012

A Forward Reachability Algorithm for Bounded Timed-Arc Petri Nets

DAVID, Alexandre, Lasse JACOBSEN, Morten JACOBSEN a Jiří SRBA

Základní údaje

Originální název

A Forward Reachability Algorithm for Bounded Timed-Arc Petri Nets

Autoři

DAVID, Alexandre (250 Francie), Lasse JACOBSEN (208 Dánsko), Morten JACOBSEN (208 Dánsko) a Jiří SRBA (203 Česká republika, garant, domácí)

Vydání

Electronic Proceedings of Theoretical Computer Science, Nizozemi, Open Publishing Association, 2012, 2075-2180

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Nizozemské království

Utajení

není předmětem státního či obchodního tajemství

Odkazy

Web

Kód RIV

RIV/00216224:14330/12:00062417

Organizační jednotka

Fakulta informatiky

DOI

http://dx.doi.org/10.4204/EPTCS.102.12

UT WoS

000219766800013

Klíčová slova anglicky

Petri nets; verification; timed systems; reachability

Příznaky

Recenzováno

Změněno: 23. 4. 2013 09:34, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

Timed-arc Petri nets (TAPN) are a well-known time extension of thePetri net model and several translations to networks of timedautomata have been proposed for this model.We present a direct, DBM-basedalgorithm for forward reachability analysis of bounded TAPNs extended with transport arcs, inhibitor arcs and age invariants.We also give a complete proof of its correctness,including reduction techniques based on symmetries and extrapolation.Finally, we augment the algorithm with a novel state-spacereduction technique introducing a monotonic ordering on markings and prove its soundness even in the presence of monotonicity-breaking features like age invariants and inhibitor arcs. We implement the algorithm within the model-checkerTAPAAL and the experimental results document an encouraging performance compared to verification approaches that translate TAPN models to UPPAAL timed automata.

Návaznosti

LA09016, projekt VaV

Název: Účast ČR v European Research Consortium for Informatics and Mathematics (ERCIM) (Akronym: ERCIM)

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Účast ČR v European Research Consortium for Informatics and Mathematics

Citovat

DAVID, Alexandre, Lasse JACOBSEN, Morten JACOBSEN a Jiří SRBA. A Forward Reachability Algorithm for Bounded Timed-Arc Petri Nets. Electronic Proceedings of Theoretical Computer Science. Nizozemi: Open Publishing Association, 2012, roč. 102, č. 1, s. 125-140. ISSN 2075-2180. Dostupné z: https://dx.doi.org/10.4204/EPTCS.102.12.

@article{1079020,
   author = {David, Alexandre and Jacobsen, Lasse and Jacobsen, Morten and Srba, Jiří},
   article_location = {Nizozemi},
   article_number = {1},
   doi = {http://dx.doi.org/10.4204/EPTCS.102.12},
   keywords = {Petri nets; verification; timed systems; reachability},
   language = {eng},
   issn = {2075-2180},
   journal = {Electronic Proceedings of Theoretical Computer Science},
   title = {A Forward Reachability Algorithm for Bounded Timed-Arc Petri Nets},
   url = {http://rvg.web.cse.unsw.edu.au/eptcs/content.cgi?SSV2012},
   volume = {102},
   year = {2012}
}

TY  - JOUR
ID  - 1079020
AU  - David, Alexandre - Jacobsen, Lasse - Jacobsen, Morten - Srba, Jiří
PY  - 2012
TI  - A Forward Reachability Algorithm for Bounded Timed-Arc Petri Nets
JF  - Electronic Proceedings of Theoretical Computer Science
VL  - 102
IS  - 1
SP  - 125-140
EP  - 125-140
PB  - Open Publishing Association
SN  - 20752180
KW  - Petri nets
KW  - verification
KW  - timed systems
KW  - reachability
UR  - http://rvg.web.cse.unsw.edu.au/eptcs/content.cgi?SSV2012
L2  - http://rvg.web.cse.unsw.edu.au/eptcs/content.cgi?SSV2012
N2  - Timed-arc Petri nets (TAPN) are a well-known time extension of thePetri net model and several translations to networks of timedautomata have been proposed for this model.We present a direct, DBM-basedalgorithm for forward reachability analysis of bounded TAPNs extended with transport arcs, inhibitor arcs and age invariants.We also give a complete proof of its correctness,including reduction techniques based on symmetries and extrapolation.Finally, we augment the algorithm with a novel state-spacereduction technique introducing a monotonic ordering on markings and prove its soundness even in the presence of monotonicity-breaking features like age invariants and inhibitor arcs. We implement the algorithm within the model-checkerTAPAAL and the experimental results document an encouraging performance compared to verification approaches that translate TAPN models to UPPAAL timed automata.
ER  -

DAVID, Alexandre, Lasse JACOBSEN, Morten JACOBSEN a Jiří SRBA. A Forward Reachability Algorithm for Bounded Timed-Arc Petri Nets. \textit{Electronic Proceedings of Theoretical Computer Science}. Nizozemi: Open Publishing Association, 2012, roč.~102, č.~1, s.~125-140. ISSN~2075-2180. Dostupné z: https://dx.doi.org/10.4204/EPTCS.102.12.

Podrobný výpis o publikaci