Petri Games: A Semantic and Algorithmic Approach for the Efficient Synthesis of Distributed Reactive Systems

Project Description

Project Goals

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 University of Oldenburg.

Related Publications