Bounded Synthesis for Petri Games

Bernd Finkbeiner

Petri games, introduced in recent joint work with Ernst-RĂ¼diger Olderog, are an extension of Petri nets for the causality-based synthesis of distributed systems. In a Petri game, each token is a player in a multiplayer game, played between the “environment” and “system” teams. In this paper, we propose a new technique for finding winning strategies for the system players based on the bounded synthesis approach. In bounded synthesis, we limit the size of the strategy. By incrementally increasing the bound, we can focus the search towards small solutions while still eventually finding every finite winning strategy.

Symposium in Honour of Ernst-RĂ¼diger Olderog on the Occasion of His 60th Birthday (Correct System Design 2015).

(pdf) (bib)