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
2 MoVe - Modélisation et Vérification

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.

Domaines: Autre [cs.OH]

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⟩