Petri Games: A Semantic and Algorithmic Approach for the Efficient Synthesis of Distributed Reactive Systems
- Principal Investigator: Bernd Finkbeiner and Ernst-Rüdiger Olderog
- Scientific Assistant: Manuel Gieseking and Jesko Hecking-Harbusch
- Funding: DFG research grant
- Funding Period: since 2018
The reactive synthesis problem considers a specification of a reactive system and asks for an implementation that satisfies the specification for all possible behaviors of the system’s environment. A particularly interesting version of the problem, with huge potential for practical applications, is the synthesis of distributed systems, consisting of multiple concurrent processes. However, most results on the synthesis problem for distributed systems are negative. In two well-studied settings, the Pnueli/Rosner model and Zielonka’s asynchronous automata, distributed synthesis has extremely high complexity (nonelementary) or is even undecidable. The goal of this project is to develop a new setting for the synthesis of distributed systems where the synthesis problem can be solved with affordable cost, and that is, at the same time, sufficiently powerful to express the synthesis problems of realistic distributed systems.
Our setting is based on Petri games, a game-theoretic extension of Petri nets. In previous work, we have shown that synthesis problems for distributed systems from manufacturing and workflow scenarios can be modeled as Petri games. We have also shown that under certain restrictions, the winning strategy of a Petri game, which corresponds to a distributed implementation, can be determined efficiently. The goal of our project is achieved by extending Petri games to a full framework for the synthesis of distributed systems. The work targets both the semantic foundations of Petri games and efficient algorithms for solving Petri games. The new semantic concepts will make Petri games more expressive and more compact, and thus applicable to realistic distributed systems. The new algorithms will generalize the existing algorithms, incorporating, in particular, the new semantic concepts, while maintaining affordable complexity. We will evaluate our approach on two realistic application areas that are out of reach for synthesis today: smart factories and automated access control systems in large buildings.
Overall, this project will develop the first practical synthesis approach for distributed systems, including the necessary models, algorithms, and tools.
This is a joint project with the Univerity of Oldenburg.
- Model Checking Branching Properties on Petri Nets with Transits
Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, and Ernst-Rüdiger Olderog. ATVA 2020
- AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL
Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, and Ernst-Rüdiger Olderog. CAV 2020
- Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems
Jesko Hecking-Harbusch and Niklas Metzger. ATVA 2019
- Model Checking Data Flows in Concurrent Network Updates
Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, and Ernst-Rüdiger Olderog. ATVA 2019
- Translating Asynchronous Games for Distributed Synthesis
Raven Beutner, Bernd Finkbeiner, and Jesko Hecking-Harbusch. CONCUR 2019
- High-Level Representation of Benchmark Families for Petri Games
Manuel Gieseking and Ernst-Rüdiger Olderog. arXiv
- Symbolic vs. Bounded Synthesis for Petri Games
Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, and Ernst-Rüdiger Olderog. SYNT 2017
- ADAM: Causality-Based Synthesis of Distributed Systems
Bernd Finkbeiner, Manuel Gieseking, and Ernst-Rüdiger Olderog. CAV 2015
- Petri Games: Synthesis of Distributed Systems with Causal Memory
Bernd Finkbeiner and Ernst-Rüdiger Olderog. Information and Computation 253