Interval Abstraction Refinement for Model Checking of 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%2F14%3A00080035" target="_blank" >RIV/00216224:14330/14:00080035 - isvavai.cz</a>
Result on the web
<a href="http://link.springer.com/chapter/10.1007%2F978-3-319-10512-3_17" target="_blank" >http://link.springer.com/chapter/10.1007%2F978-3-319-10512-3_17</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-319-10512-3_17" target="_blank" >10.1007/978-3-319-10512-3_17</a>
Alternative languages
Result language
angličtina
Original language name
Interval Abstraction Refinement for Model Checking of Timed-Arc Petri Nets
Original language description
State-space explosion is a major obstacle in verification of time-critical distributed systems. An important factor with a negative influence on the tractability of the analysis is the size of constants that clocks are compared to. This problem is particularly accented in explicit state-space exploration techniques. We suggest an approximation method for reducing the size of constants present in the model. The proposed method is developed for Timed-Arc Petri Nets and creates an under-approximation or anover-approximation of the model behaviour. The verification of approximated Petri net models can be considerably faster but it does not in general guarantee conclusive answers. We implement the algorithms within the open-source model checker TAPAAL anddemonstrate on a number of experiments that our approximation techniques often result in a significant speed-up of the verification.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
—
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2014
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 the 12th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'14)
ISBN
9783319105116
ISSN
0302-9743
e-ISSN
—
Number of pages
15
Pages from-to
237-251
Publisher name
Springer-Verlag
Place of publication
Nizozemsko
Event location
Italie
Event date
Jan 1, 2014
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—