Coverability analysis of time basic petri nets with non-urgent behavior
Contributo in Atti di convegno
Data di Pubblicazione:
2016
Citazione:
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 [10.1109/SYNASC.2016.036].
Abstract:
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.
Tipologia IRIS:
03 - Contributo in volume
Keywords:
coverability analysis; infinite-states systems; reachability problems; real-time systems; symbolic state space exploration; Time Basic Petri nets; time constraints
Elenco autori:
M. Camilli, C. Bellettini, L. Capra, M. Monga
Link alla scheda completa:
Titolo del libro:
Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), 2016 18th International Symposium on