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.

翻译：佩特里博弈是一种用于分布式系统自动综合的多玩家博弈模型，其中玩家以佩特里网上的令牌表示，并分为环境玩家和系统玩家。只要玩家在网络独立部分移动，彼此之间便互不知晓；当他们在联合变迁处同步时，每个玩家会获知其他玩家的完整因果历史。我们证明，在全局安全性条件下，双玩家佩特里博弈的综合问题是NP完全的，并且在最多4个玩家的情况下，它可以在非确定性指数上界内求解。此外，我们证明在局部安全性条件下，至少6个玩家的佩特里博弈的综合问题是不可判定的。