Equivalence of Petri Games
Jesko Hecking-Harbusch
Petri games represent games between the system and the environment which are distributed over several independent components, respectively. Independent components of the system model that decisions can be based on incomplete information, whereas each independent component of the environment represents one source of non-determinism. Information is gathered locally and only exchanged upon synchronization among components. The goal of Petri games is to synthesize a strategy for the system which satisfies the winning condition for every non-deterministic behavior of the environment.
Petri games are an extension of Petri nets. Bisimilarity defines an equivalence relation on Petri nets among other modeling formalisms. It defines two Petri nets as bisimilar if a bisimulation exists between the nets. The bisimulation includes pairs of markings of two Petri nets. For every pair, all possible transitions in one net can be simulated in the other net such that the following markings are again related and vice versa. This allows us to view bisimilar Petri nets as interchangeable.
In this Master’s thesis, bisimilarity of Petri games is defined. This equivalence relation allows the translation of strategies between bisimilar Petri games which makes the games interchangeable. We extend the standard bisimulation between Petri nets to incorporate the extended expressiveness of Petri games. The bisimulation handles the possibly infinite history of Petri games in a finite manner.
Master Thesis.