(Un)Decidability Bounds of the Synthesis Problem for Petri Games

TL;DR

This paper investigates the computational complexity of synthesizing distributed systems modeled as Petri games, establishing NP-completeness for two players and undecidability for six or more players under safety conditions.

Contribution

It provides the first complexity bounds for Petri game synthesis, showing NP-completeness for two players and undecidability for six or more players, advancing understanding of their computational limits.

Findings

NP-complete for two-player Petri games with global safety

Solvable within nondeterministic exponential time for up to 4 players

Undecidable for Petri games with at least 6 players under local safety

Abstract

Petri games are a multi-player game model for the automatic synthesis of distributed systems, where the players are represented as tokens on a Petri net and are grouped into environment players and system players. 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 entire causal history of the other players. We show that the synthesis problem for two-player Petri games under a global safety condition is NP-complete and it can be solved within a non-deterministic exponential upper bound in the case of up to 4 players. Furthermore, we show the undecidability of the synthesis problem for Petri games with at least 6 players under a local safety condition.