Bounded Synthesis for Petri Games

Abstract. Petri games, introduced in recent joint work with ErnstR¨udiger 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.

• Type: Journal
• Year: 2015
• Where: BIRTHDAY
• Authors: Bernd Finkbeiner
• Keywords: Applied Computing, BIRTHDAY 2015