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

• Applicants: Professor Dr. Bernd Finkbeiner; Professor Dr. Ernst-Rüdiger Olderog
• Subject Area: Theoretical Computer Science
• Term: from 2018 to 2022
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 392735815

• Final Report Year: 2022

Final Report Abstract

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 project was 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. The setting in this project are Petri games, a game-theoretic extension of Petri nets. We achieved the following results: • We increased the expressiveness of the game model for the distributed synthesis by extending the memory model to forgetful places and by introducing new winning objectives beyond safety on the unbounded local data flow of the components up to LTL specifications. • With high-level Petri games, we introduced a modeling language for the distributed synthesis problem that can succinctly represent complete benchmark families and ease the development of algorithms exploiting the symmetries in the system. • We established a formal correspondence between the synthesis approach for distributed systems using Zielonka’s asynchronous automata and the approach using Petri games such that decidable results can be translated between the models. • We introduced synthesis algorithms with affordable complexity for subclasses of Petri games with global safety objectives and Petri games with transits with local unbounded data flow specifications. • We developed bounded synthesis algorithms as an alternative, semi-decidable approach to the synthesis problem for Petri games. • We developed and implemented model checking algorithms for Petri nets with transits and Flow-CTL∗. • We provide tool support for the introduced concepts. • As application areas for (high-level) Petri games we reinforced manufacturing and workflow scenarios. For Petri nets with transits we introduced as new application areas softwaredefined networks and access control in physical spaces.

Publications

• Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems. Lecture Notes in Computer Science, 369-386. Springer International Publishing.
  Hecking-Harbusch, Jesko & Metzger, Niklas O.
  
• Model Checking Data Flows in Concurrent Network Updates. Lecture Notes in Computer Science, 515-533. Springer International Publishing.
  Finkbeiner, Bernd; Gieseking, Manuel; Hecking-Harbusch, Jesko & Olderog, Ernst-Rüdiger
  
• Translating Asynchronous Games for Distributed Synthesis. In: 30th International Conference on Concurrency Theory, CONCUR 2019, August 27-30, 2019, Amsterdam, the Netherlands. 2019
  R. Beutner, B. Finkbeiner & J. Hecking-Harbusch
  
• AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL. Lecture Notes in Computer Science, 64-76. Springer International Publishing.
  Finkbeiner, Bernd; Gieseking, Manuel; Hecking-Harbusch, Jesko & Olderog, Ernst-Rüdiger
  
• Model Checking Branching Properties on Petri Nets with Transits. Lecture Notes in Computer Science, 394-410. Springer International Publishing.
  Finkbeiner, Bernd; Gieseking, Manuel; Hecking-Harbusch, Jesko & Olderog, Ernst-Rüdiger
  
• Solving high-level Petri games. Acta Informatica, 57(3-5), 591-626.
  Gieseking, Manuel; Olderog, Ernst-Rüdiger & Würdemann, Nick
  
• A Web Interface for Petri Nets with Transits and Petri Games. Lecture Notes in Computer Science, 381-388. Springer International Publishing.
  Gieseking, Manuel; Hecking-Harbusch, Jesko & Yanich, Ann
  
• Canonical Representations for Direct Generation of Strategies in High-Level Petri Games. Lecture Notes in Computer Science, 95-117. Springer International Publishing.
  Gieseking, Manuel & Würdemann, Nick
  
• Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory. In: 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference)
  B. Finkbeiner, M. Gieseking, J. Hecking-Harbusch & E.-R. Olderog