Skip to Main content Skip to Navigation
Conference papers

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], Inria Saclay - Ile de France
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.
Document type :
Conference papers
Complete list of metadata
Contributor : Stefan Haar <>
Submitted on : Thursday, January 10, 2013 - 11:03:36 PM
Last modification on : Tuesday, March 30, 2021 - 12:12:04 PM

Links full text



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. pp.5018-5025, ⟨10.1109/ACC.2009.5160020⟩. ⟨hal-00772677⟩



Record views