Efficient state-based analysis by introducing bags in Petri nets color domains

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 elaborate types becomes a burden. A good trade-off between expressiveness and analysis capabilities is then to have only simple types, which is achieved with symmetric nets. These latter nets enjoy the possibility of generating a symbolic reachability graph, which is much smaller 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.