Canonical Representations for Direct Generation of Strategies in High-level Petri Games (Full Version)

TL;DR

This paper introduces a canonical representation for high-level Petri games that enables direct strategy generation, reducing state space and improving performance in solving distributed system synthesis problems.

Contribution

It presents a novel canonical form for reduced B"uchi games derived from high-level Petri games, facilitating direct strategy translation and enhanced computational efficiency.

Findings

Performance improved for larger state spaces in benchmarks.

Canonical representation enables direct strategy extraction.

Significant state space reduction achieved.

Abstract

Petri games are a multi-player game model for the synthesis problem in distributed systems, i.e., the automatic generation of local controllers. The model represents causal memory of the players, which are tokens on a Petri net and divided into two teams: the controllable system and the uncontrollable environment. For one environment player and a bounded number of system players, the problem of solving Petri games can be reduced to that of solving B\"uchi games. High-level Petri games are a concise representation of ordinary Petri games. Symmetries, derived from a high-level representation, can be exploited to significantly reduce the state space in the corresponding B\"uchi game. We present a new construction for solving high-level Petri games. It involves the definition of a unique, canonical representation of the reduced B\"uchi game. This allows us to translate a strategy in the B\"uchi game directly into a strategy in the Petri game. An implementation applied on six structurally different benchmark families shows in most cases a performance increase for larger state spaces.