Generating Concurrency-preserving Petri Games
Sanny Schmitt
Petri games represent a multiplayer game model used to synthesize distributed systems. In these games, each token either belongs to the team of system players or to the team of environment players, and moves independently between the places of an underlying Petri net. While doing so, each player collects local information in form of his causal past. This information is exchanged between two or more players whenever they synchronize on joint transitions.
During the course of a game, the numbers of players might change due to the generation or consumption of a player. Petri games that do not change the number of players are called concurreny-preserving. Because Petri games are used to model and synthesize distributed systems, it is desirable to know the maximal number of processes a priori. Furthermore, there exists algorithms based on Petri games that require the number of players to stay the same.
In this thesis, we present an algorithm that makes Petri games concurrency-preserving if the Petri game matches a certain form. Furthermore, the transformed game preserves the flow and causality of the original game. It is also shown that the winning strategy for the extended game is the same as in the original game.
Bachelor Thesis.