Petri Games: Synthesis of Distributed Systems with Causal Memory
arXiv:1406.1069 · doi:10.4204/EPTCS.161.19
Abstract
We present a new multiplayer game model for the interaction and the flow of information in a distributed system. The players are tokens on a Petri net. As long as the players move in independent parts of the net, they do not know of each other; when they synchronize at a joint transition, each player gets informed of the causal history of the other player. We show that for Petri games with a single environment player and an arbitrary bounded number of system players, deciding the existence of a safety strategy for the system players is EXPTIME-complete.
In Proceedings GandALF 2014, arXiv:1408.5560