Project Details
Projekt
Petri Games: A Semantic and Algorithmic Approach for the Efficient Synthesis of Distributed Reactive Systems
Subject Area
Theoretical Computer Science
Term
from 2018 to 2022
Project identifier
Deutsche Forschungsgemeinschaft (DFG) - Project number 392735815
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 the proposed 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 proposed 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 the proposed project is achieved by extending Petri games to a full framework for the synthesis of distributed systems. The proposed 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. We expect that our synthesis approach will have impact beyond the immediate synthesis community into areas such as semantics, distributed systems design, and autonomous systems.
DFG Programme
Research Grants
