Canonical representations for direct generation of strategies in high-level Petri games

DOI10.1007/978-3-030-76983-3_6MaRDI QIDQ2117156zbMATH OpenOpenAlexFDO

Authors Manuel Gieseking, Nick Würdemann

Publication date 21 March 2022

Full work available at URL https://arxiv.org/abs/2112.04476

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Applications of game theory (91A80)

Abstract: Petri games are a multi-player game model for the synthesis of distributed systems with multiple concurrent processes based on Petri nets. The processes are the players in the game represented by the token of the net. The players are divided into two teams: the controllable system and the uncontrollable environment. An individual controller is synthesized for each process based only on their locally available causality-based information. 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 almost all cases a performance increase for larger state spaces.

Recommendations

Cites work

Cited in

(4)

This page was built for publication: Canonical representations for direct generation of strategies in high-level Petri games

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2117156)