Petri Games: Synthesis of Distributed Systems with Causal Memory

TL;DR

This paper introduces Petri games, a model for distributed system synthesis that captures causal memory through Petri nets, and proves the EXPTIME-completeness of safety strategy existence in certain cases.

Contribution

It proposes a novel game-theoretic model for distributed systems with causal memory and analyzes its computational complexity.

Findings

Deciding safety strategies is EXPTIME-complete for Petri games with one environment and bounded system players.

The model captures causal information flow via synchronization in Petri nets.

Provides a formal framework for synthesis of distributed systems with causal memory.

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.