Principal investigators: E.-R. Olderog and B. Finkbeiner

Duration: 01.08.2018 – 30.04.2022

Funding: DFG

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.

Research associates: M. Gieseking and J. Hecking-Harbusch