Symbolic vs. Bounded Synthesis for Petri Games

TL;DR

This paper compares symbolic and bounded synthesis methods for Petri games, analyzing their effectiveness and efficiency through experimental benchmarks including manufacturing and workflow scenarios.

Contribution

It introduces a prototype implementation of bounded synthesis for Petri games and compares it with the symbolic approach in the ADAM tool.

Findings

Bounded synthesis shows promising results on certain benchmarks.

Symbolic approach efficiently handles larger state spaces.

Experimental comparison highlights strengths and limitations of both methods.

Abstract

Petri games are a multiplayer game model for the automatic synthesis of distributed systems. We compare two fundamentally different approaches for solving Petri games. The symbolic approach decides the existence of a winning strategy via a reduction to a two-player game over a finite graph, which in turn is solved by a fixed point iteration based on binary decision diagrams (BDDs). The bounded synthesis approach encodes the existence of a winning strategy, up to a given bound on the size of the strategy, as a quantified Boolean formula (QBF). In this paper, we report on initial experience with a prototype implementation of the bounded synthesis approach. We compare bounded synthesis to the existing implementation of the symbolic approach in the synthesis tool ADAM. We present experimental results on a collection of benchmarks, including one new benchmark family, modeling manufacturing and workflow scenarios with multiple concurrent processes.