Concurrent bisimulations in Petri nets (Q2639636)

Bisimulations defined in terms of execution sequences cannot distinguish between a concurrent system and its sequential simulation. The authors consider a model of concurrency, Petri nets, which display concurrency in an explicit way, and introduce a concept of bisimulation, fully concurrent bisimulation or FC-bisimulation, that is stronger than ordinary bisimulation, is equivalent to ordinary bisimulation in the sequential case, and, under some conditions, is preserved by refinement of atomic actions. For net systems sequential bisimulation is defined in terms of a relation which puts states into correspondence, among which the initial ones, such that the visible evolutions of them are the same and lead to correspondent states. Equivalently, this bisimulation can be defined in terms of simple transitions or in terms of occurrence sequences. The failure of sequential bisimulation (as well as of bisimulations considering general step sequences instead of interleavings) in the case of systems containing concurrent actions suggests generalizations based on partial orderings, i.e. on sets of processes. A first proposal is concurrent bisimulation which puts states into correspondence, among which the initial ones, such that visible concurrent evolutions of them are order isomorphic and lead to correspondent states. This bisimulation, which is similar to CCS pomset bisimulation, does not withstand a refinement. Finally, FC-bisimulation is defined requiring that there is a relation between processes such that initial processes are related, related processes have order isomorphic abstractions and any extension of a process \(\pi\) is related to an extension of a process related to \(\pi\). The resulting notion corresponds to BS-bisimulation introduced for behaviour structures and to history peserving bisimulation defined for event structures. FC-bisimulation implies concurrent bisimulation and the above mentioned bisimulation definitions collapse for sequential systems. Besides properties preserved also by sequential bisimulations (like liveness of any visible operation and generated language), FC- bisimulation preserves the absence of auto-concurrency and auto- concurrent actions. For other properties, one may wonder whether for any system which does not enjoy the property there is one which has it. So the authors prove that for a system without auto-concurrency there exists one which is strict. Finally, FC-bisimulation is shown to be a congruence for many kinds of refinement and under some conditions on nets.