Unified bisimulation applied to incremental abstraction of Petri nets

Abstract Bisimulation is a powerful abstraction method, which can be used to perform model reduction, especially for modular transition systems. A unified formulation of strong, weak, stutter, and branching bisimulation is presented. For branching bisimulation an extended relation is shown to coincide with the original branching bisimulation when the largest relations (equivalence relations) are considered. A block transition based description that is more natural from a model reduction perspective is also shown to be equivalent to the original relation based bisimulations. All bisimulation formulations are based on general transition system models, which means that systems both including state and transition labels are handled in a unified way. An incremental abstraction based on divergence sensitive branching bisimulation is then formulated and applied to Petri nets. The strength of the proposed method is demonstrated especially for Petri nets, combining both analytical and computational abstraction.