Symbolic vs. Bounded Synthesis for Petri Games

Bernd Finkbeiner
(Saarland University)
Manuel Gieseking
(University of Oldenburg)
Jesko Hecking-Harbusch
(Saarland University)
Ernst-Rüdiger Olderog
(University of Oldenburg)

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.

In Dana Fisman and Swen Jacobs: Proceedings Sixth Workshop on Synthesis (SYNT 2017), Heidelberg, Germany, 22nd July 2017, Electronic Proceedings in Theoretical Computer Science 260, pp. 23–43.
Published: 28th November 2017.

ArXived at: http://dx.doi.org/10.4204/EPTCS.260.5 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org