Verification of Liveness Properties on Closed Timed-Arc Petri Nets
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F13%3A00067580" target="_blank" >RIV/00216224:14330/13:00067580 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1007/978-3-642-36046-6_8" target="_blank" >http://dx.doi.org/10.1007/978-3-642-36046-6_8</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-642-36046-6_8" target="_blank" >10.1007/978-3-642-36046-6_8</a>
Alternative languages
Result language
angličtina
Original language name
Verification of Liveness Properties on Closed Timed-Arc Petri Nets
Original language description
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 inthe 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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/LG13010" target="_blank" >LG13010: Czech Republic representation in the European Research Consortium for Informatics and Mathematics (ERCIM)</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2013
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Proceedings of Mathematical and Engineering Methods in Computer Science (MEMICS'12)
ISBN
9783642360442
ISSN
0302-9743
e-ISSN
—
Number of pages
13
Pages from-to
69-81
Publisher name
Springer
Place of publication
Netherlands
Event location
Znojmo
Event date
Jan 1, 2012
Type of event by nationality
EUR - Evropská akce
UT code for WoS article
—