|
 
|
[BBc13] Reducing interleaving semantics redundancy in reachability analysis of time Petri nets
Revue Internationale avec comité de lecture : Journal ACM Transactions in Embedded Computing Systems (TECS) , vol. 12(1), pp. 1-24, 2013Mots clés: Enumerative analysis, time Petri nets, state space explosion, interleaving semantics, reachability analysis
Résumé:
The main problem of verification techniques based on exploration of (reachable) state space is the state explosion problem.
In timed models, abstract states reached by different interleavings of the same set of transitions are, in general, different and their union is not necessarily an abstract state. To attenuate this state explosion, it would be interesting to reduce the redundancy caused by the interleaving semantics by agglomerating all these abstract states whenever their union is an abstract state.
This article considers the time Petri net model and establishes some sufficient conditions that ensure that this union is an abstract state. In addition, it proposes a procedure to compute this union without computing beforehand intermediate abstract states. Finally, it shows how to use this result to improve the reachability analysis.
Commentaires:
http://dl.acm.org/citation.cfm?doid=2406336.2406343
Equipe:
sys
BibTeX
| @article { | |||
| BBc13, | |||
| title | = | "{Reducing interleaving semantics redundancy in reachability analysis of time Petri nets}", | |
| author | = | "H. Boucheneb and K. Barkaoui", | |
| journal | = | "ACM Transactions in Embedded Computing Systems (TECS) ", | |
| year | = | 2013, | |
| volume | = | 12, | |
| number | = | 1, | |
| pages | = | "1-24", | |
| note | = | "{http://dl.acm.org/citation.cfm?doid=2406336.2406343}", | |
| } | |||
