Verification of Liveness Properties on Closed Timed-Arc Petri Nets

Mathias Andersen, Heine G. Larsen, Jiri Srba, Mathias Sørensen, Jakob Haahr Taankvist

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

15 Citationer (Scopus)

Abstract

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.
OriginalsprogEngelsk
TitelMathematical and Engineering Methods in Computer Science : 8th International Doctoral Workshop, MEMICS 2012, Znojmo, Czech Republic, October 25-28, 2012, Revised Selected Papers
Antal sider13
Vol/bind7721
UdgivelsesstedNetherlands
ForlagSpringer Publishing Company
Publikationsdato2013
Sider69-81
ISBN (Trykt)978-3-642-36044-2
ISBN (Elektronisk)978-3-642-36046-6
DOI
StatusUdgivet - 2013
Begivenhed8th International Doctoral Workshop on Mathematical and Engineering Methods in Computer Science - Znojmo, Tjekkiet
Varighed: 25 okt. 201228 okt. 2012
Konferencens nummer: 8

Workshop

Workshop8th International Doctoral Workshop on Mathematical and Engineering Methods in Computer Science
Nummer8
Land/OmrådeTjekkiet
ByZnojmo
Periode25/10/201228/10/2012
NavnLecture Notes in Computer Science
ISSN0302-9743

Fingeraftryk

Dyk ned i forskningsemnerne om 'Verification of Liveness Properties on Closed Timed-Arc Petri Nets'. Sammen danner de et unikt fingeraftryk.

Citationsformater