# Symbolic vs. Bounded Synthesis for Petri Games

@inproceedings{Finkbeiner2017SymbolicVB, title={Symbolic vs. Bounded Synthesis for Petri Games}, author={Bernd Finkbeiner and Manuel Gieseking and Jesko Hecking-Harbusch and Ernst-R{\"u}diger Olderog}, booktitle={SYNT@CAV}, year={2017} }

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… Expand

#### Topics from this paper

#### 8 Citations

High-Level Representation of Benchmark Families for Petri Games

- Computer Science
- ArXiv
- 2019

A new possibility to represent benchmark families for the distributed synthesis problem modeled with Petri games is introduced that enables the user to specify an entire benchmark family as one parameterized high-level net. Expand

Translating Asynchronous Games for Distributed Synthesis (Full Version)

- Computer Science, Mathematics
- ArXiv
- 2019

This paper provides the first formal connection between control games and Petri games and establishes the equivalence of the two game models based on weak bisimulations between their strategies, and shows that a game of one type can be translated into an equivalent game of the other type. Expand

Solving high-level Petri games

- Computer Science
- Acta Informatica
- 2020

This paper presents a new solving technique for a subclass of high-level Petri games with a single uncontrollable player, a bounded number of controllable players, and a local safety objective and exploits symmetries in the high- level Petri game. Expand

Synthesis in Distributed Environments

- Computer Science
- FSTTCS
- 2017

This paper shows that the synthesis problem in distributed environments can be solved in polynomial time for nets with up to two environment tokens, and model such environments as a team of players and keep track of the information known to each individual player. Expand

Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory

- Computer Science
- ArXiv
- 2021

This paper proves for winning conditions given as bad markings that it is decidable whether a winning strategy for the system players exists in Petri games with a bounded number of system players and one environment player, and provides decidability and undecidability results for global winning conditions. Expand

A Web Interface for Petri Nets with Transits and Petri Games

- Computer Science
- TACAS
- 2021

A web interface is presented that allows an intuitive, visual definition of Petri nets with transits and Petri games and the corresponding model checking and synthesis problems are solved directly on a server. Expand

Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems

- Computer Science
- ATVA
- 2019

This work identifies true concurrency in synthesis of asynchronous distributed systems represented as Petri games by identifying when several interleavings can be subsumed by one true concurrent trace. Expand

Solving QBF by Abstraction

- Mathematics, Computer Science
- GandALF
- 2018

A recursive counterexample guided abstraction and refinement algorithm (CEGAR) for solving and certifying QBFs that exploits structural reasoning on the formula level and how to derive an efficient certification extraction method on top of the algorithm is presented. Expand

#### References

SHOWING 1-10 OF 20 REFERENCES

Bounded Synthesis for Petri Games

- Computer Science
- Correct System Design
- 2015

A new technique for finding winning strategies for the system players based on the bounded synthesis approach, which can focus the search towards small solutions while still eventually finding every finite winning strategy. Expand

Petri Games: Synthesis of Distributed Systems with Causal Memory

- Computer Science
- GandALF
- 2014

It is shown that for Petri games with a single environment player and an arbitrary bounded number of system players, deciding the existence of a safety strategy for the system players is EXPTIME-complete. Expand

Solving QBF by Abstraction

- Mathematics, Computer Science
- GandALF
- 2018

A recursive counterexample guided abstraction and refinement algorithm (CEGAR) for solving and certifying QBFs that exploits structural reasoning on the formula level and how to derive an efficient certification extraction method on top of the algorithm is presented. Expand

Bounded synthesis

- Computer Science
- International Journal on Software Tools for Technology Transfer
- 2012

This article introduces the bounded synthesis approach, which makes it possible to traverse this immense search space in a structured manner and demonstrates that bounded synthesis solves many synthesis problems that were previously considered intractable. Expand

Adam: Causality-Based Synthesis of Distributed Systems

- Computer Science
- CAV
- 2015

Adam is a tool for the automatic synthesis of distributed systems with multiple concurrent processes that implements the first symbolic game solving algorithm for Petri games. Expand

Synthesizing distributed systems

- Computer Science
- Proceedings 16th Annual IEEE Symposium on Logic in Computer Science
- 2001

A significant extension of the result that results on multi-player games imply that the synthesis problem for linear specifications is undecidable for general architectures, and is nonelementary decidable for hierarchical architectures. Expand

Uniform distributed synthesis

- Computer Science
- 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05)
- 2005

Information forks, a comprehensive criterion that characterizes all architectures with an undecidable synthesis problem, is defined and it can be determined in O(n/sup 2//spl middot/v) time whether the synthesis problem is decidable. Expand

Non-prenex QBF Solving Using Abstraction

- Mathematics, Computer Science
- SAT
- 2016

A modified algorithm is presented that lifts the restriction on prenex quantifiers and handles tree-shaped quantifier hierarchies where different branches can be solved independently and exploits this property by solving independent branches in parallel. Expand

Distributed reactive systems are hard to synthesize

- Computer Science, Mathematics
- Proceedings [1990] 31st Annual Symposium on Foundations of Computer Science
- 1990

It is shown that the problem of realizing a given propositional specification over a given architecture is undecidable, and it is nonelementarily decidable for the very restricted class of hierarchical architectures. Expand

Counterexample-guided abstraction refinement

- Computer Science
- 10th International Symposium on Temporal Representation and Reasoning, 2003 and Fourth International Conference on Temporal Logic. Proceedings.
- 2003

Counterexample-guided abstraction refinement is an automatic abstraction method where the key step is to extract information from false negatives ("spurious counterexamples") due to over-approximation. Expand