Efficient State-Based Analysis by Introducing Bags in Petri Nets Color Domains

Serge Haddad 1 Fabrice Kordon 2 Laure Petrucci Jean-François Pradat-Peyre 2 Nicolas Trèves
1 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
2 MoVe - Modélisation et Vérification
LIP6 - Laboratoire d'Informatique de Paris 6
Abstract : The use of high-level nets, such as coloured Petri nets, is very convenient for modelling complex controllable systems in order to have a compact, readable and structured specification. However, when coming to the analysis phase, using too elaboratc types becomes a burden. A good trade-off between expressivene and analy is capabilities is then to have only imple types, which is achieved with symmetric nels. These latter nels enjoy the possibility of generating a symbolic reachability gralph, which is much smallcr than the whole state space and still allows for exhaustive analysis. In this paper, we extend the symmetric net model with bags on arcs. Hence, variables can be bags of tokens,leading to more flexible models. We show that symmetric nets with bags also allow for applying the symbolic reachability graph technique with application to deadlock detection and more generally for safety properties.
Type de document :
Communication dans un congrès
28th American Control Conference (ACC'09), Jun 2009, Saint Louis, MO, United States. IEEE, Proceedings of the 28th American Control Conference (ACC'09), pp.5018-5025, 2009, 〈10.1109/ACC.2009.5160020〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00772677
Contributeur : Stefan Haar <>
Soumis le : jeudi 10 janvier 2013 - 23:03:36
Dernière modification le : vendredi 31 août 2018 - 09:25:57

Lien texte intégral

Identifiants

Collections

Citation

Serge Haddad, Fabrice Kordon, Laure Petrucci, Jean-François Pradat-Peyre, Nicolas Trèves. Efficient State-Based Analysis by Introducing Bags in Petri Nets Color Domains. 28th American Control Conference (ACC'09), Jun 2009, Saint Louis, MO, United States. IEEE, Proceedings of the 28th American Control Conference (ACC'09), pp.5018-5025, 2009, 〈10.1109/ACC.2009.5160020〉. 〈hal-00772677〉

Partager

Métriques

Consultations de la notice

332