Verification of Liveness Properties on Closed Timed-Arc Petri
Nets

D 2013

Verification of Liveness Properties on Closed Timed-Arc Petri Nets

ANDERSEN, Mathias; Heine G. LARSEN; Jiří SRBA; Mathias G. SOERENSEN; Jakob H. TAANKVIST et al.

Základní údaje

Originální název

Verification of Liveness Properties on Closed Timed-Arc Petri Nets

Autoři

ANDERSEN, Mathias; Heine G. LARSEN; Jiří SRBA; Mathias G. SOERENSEN a Jakob H. TAANKVIST

Vydání

Netherlands, Proceedings of Mathematical and Engineering Methods in Computer Science (MEMICS'12), od s. 69-81, 13 s. 2013

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

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í

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/13:00067580

Organizační jednotka

Fakulta informatiky

ISBN

978-3-642-36044-2

ISSN

DOI

https://doi.org/10.1007/978-3-642-36046-6_8

Klíčová slova anglicky

timed-arc Petri nets; verification; liveness; discretization

Změněno: 29. 4. 2014 20:09, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

Verification of closed timed models by explicit state-space exploration methods is an alternative to the wide-spread symbolic techniques based on difference bound matrices (DBMs). A few experiments found in the literature confirm that for the reachability analysis of timed automata explicit techniques can compete with DBM-based algorithms, at least for situations where the constants used in the models are relatively small. To the best of our knowledge, the explicit methods have not yet been employed in the verification of liveness properties in Petri net models extended with time. We present an algorithm for liveness analysis of closed Timed-Arc Petri Nets (TAPN) extended with weights, transport arcs, inhibitor arcs and age invariants and prove its correctness. The algorithm computes optimized maximum constants for each place in the net that bound the size of the reachable state-space. We document the efficiency of the algorithm by experiments comparing its performance with the state-of-the-art model checker UPPAAL.

Návaznosti

LG13010, projekt VaV

Název: Zastoupení ČR v European Research Consortium for Informatics and Mathematics (Akronym: ERCIM-CZ)

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

Citovat

ANDERSEN, Mathias; Heine G. LARSEN; Jiří SRBA; Mathias G. SOERENSEN a Jakob H. TAANKVIST. Verification of Liveness Properties on Closed Timed-Arc Petri Nets. In Kucera, A.; Henzinger, Th.A.; Nesetril, J.; Vojnar, T.; Antos, D. Proceedings of Mathematical and Engineering Methods in Computer Science (MEMICS'12). Netherlands: Springer, 2013, s. 69-81. ISBN 978-3-642-36044-2. Dostupné z: https://doi.org/10.1007/978-3-642-36046-6_8.

@inproceedings{1079122,
   author = {Andersen, Mathias and Larsen, Heine G. and Srba, Jiří and Soerensen, Mathias G. and Taankvist, Jakob H.},
   address = {Netherlands},
   booktitle = {Proceedings of Mathematical and Engineering Methods in Computer Science (MEMICS'12)},
   doi = {https://doi.org/10.1007/978-3-642-36046-6_8},
   editor = {Kucera, A.; Henzinger, Th.A.; Nesetril, J.; Vojnar, T.; Antos, D.},
   keywords = {timed-arc Petri nets; verification; liveness; discretization},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Netherlands},
   isbn = {978-3-642-36044-2},
   pages = {69-81},
   publisher = {Springer},
   title = {Verification of Liveness Properties on Closed Timed-Arc Petri Nets},
   year = {2013}
}

TY  - CONF
ID  - 1079122
AU  - Andersen, Mathias - Larsen, Heine G. - Srba, Jiří - Soerensen, Mathias G. - Taankvist, Jakob H.
PY  - 2013
TI  - Verification of Liveness Properties on Closed Timed-Arc Petri Nets
PB  - Springer
CY  - Netherlands
SN  - 9783642360442
KW  - timed-arc Petri nets
KW  - verification
KW  - liveness
KW  - discretization
N2  - Verification of closed timed models by explicit state-space exploration methods is an alternative to the wide-spread symbolic techniques based on difference bound matrices (DBMs). A few experiments found in the literature confirm that for the reachability analysis of timed automata explicit techniques can compete with DBM-based algorithms, at least for situations where the constants used in the models are relatively small. To the best of our knowledge, the explicit methods have not yet been employed in the verification of liveness properties in Petri net models extended with time. We present an algorithm for liveness analysis of closed Timed-Arc Petri Nets (TAPN) extended with weights, transport arcs, inhibitor arcs and age invariants and prove its correctness. The algorithm computes optimized maximum constants for each place in the net that bound the size of the reachable state-space. We document the efficiency of the algorithm by experiments comparing its performance with the state-of-the-art model checker UPPAAL.
ER  -

ANDERSEN, Mathias; Heine G. LARSEN; Jiří SRBA; Mathias G. SOERENSEN a Jakob H. TAANKVIST. Verification of Liveness Properties on Closed Timed-Arc Petri Nets. In Kucera, A.; Henzinger, Th.A.; Nesetril, J.; Vojnar, T.; Antos, D. \textit{Proceedings of Mathematical and Engineering Methods in Computer Science (MEMICS'12)}. Netherlands: Springer, 2013, s.~69-81. ISBN~978-3-642-36044-2. Dostupné z: https://doi.org/10.1007/978-3-642-36046-6\_{}8.

Přehled o publikaci