Petri games have been introduced as a multi-player game model representing causal memory to address the synthesis of distributed systems. For Petri games with one environment player and an arbitrary bounded number of system players, deciding the existence of a safety strategy is EXPTIME-complete [1]. This result forms the basis of the tool ADAM that implements an algorithm for the synthesis of distributed controllers from Petri games [2]. To evaluate the tool, it has been checked on a series of parameterized benchmarks from manufacturing and workflow scenarios [2,3].
In this talk, we introduce a new possibility to represent benchmark families for the distributed synthesis problem modeled with Petri games. It enables the user to specify an entire benchmark family as one parameterized high-level net. We describe example benchmark families from [2,3] as a high-level version of a Petri game and exhibit an instantiation yielding a concrete safe Petri game. This is a joint work with Manuel Gieseking.
[1] B. Finkbeiner & E.-R. Olderog (GandALF 2014, Inform. Comput. 2017): Petri Games: Synthesis of Distributed Systems with Causal Memory. [2] B. Finkbeiner, M. Gieseking, & E.-R. Olderog (CAV 2015): ADAM: Causality-Based Synthesis of Distributed Systems. [3] B. Finkbeiner, M. Gieseking, J. Hecking-Harbusch, & E.-R. Olderog (SYNT 2017): Symbolic vs. Bounded Synthesis for Petri Games