Time Basic Petri nets are an expressive extension of Petri nets, suitable to model real-time systems. This paper introduces a coverability analysis technique to cope with structurally unbounded Time Basic Petri net models exhibiting non-urgent behavior: i.e., models in which transitions may choose to do not fire and let time pass, even if this could lead to transition disabling. The approach we present exploits the identification of anonymous temporal information, that is the possibility of erasing timestamps associated with specific tokens without compromising the correctness of model's temporal evolution. In particular, we extend the classical Karp-Miller coverability algorithm in two ways: first, we adapt the acceleration function to deal with symbolic states and to identify unboundedness due to time anonymous tokens, second, we employ an aggressive pruning strategy to remove included/covered portions of the reachability tree during exploration.
Coverability analysis of time basic petri nets with non-urgent behavior / M. Camilli, C. Bellettini, L. Capra, M. Monga - In: Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), 2016 18th International Symposium on[s.l] : IEEE, 2016. - ISBN 9781509057078. - pp. 165-172 (( Intervento presentato al 18. convegno SYNASC tenutosi a Timisoara nel 2016.
|Titolo:||Coverability analysis of time basic petri nets with non-urgent behavior|
CAMILLI, MATTEO (Primo)
BELLETTINI, CARLO NICOLA MARIA (Secondo)
CAPRA, LORENZO (Penultimo)
MONGA, MATTIA (Ultimo)
|Parole Chiave:||coverability analysis; infinite-states systems; reachability problems; real-time systems; symbolic state space exploration; Time Basic Petri nets; time constraints|
|Settore Scientifico Disciplinare:||Settore INF/01 - Informatica|
|Data di pubblicazione:||2016|
|Digital Object Identifier (DOI):||http://dx.doi.org/10.1109/SYNASC.2016.036|
|Tipologia:||Book Part (author)|
|Appare nelle tipologie:||03 - Contributo in volume|