Search Results

Documents authored by Gieseking, Manuel


Document
Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory

Authors: Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, and Ernst-Rüdiger Olderog

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)


Abstract
In the synthesis of distributed systems, we automate the development of distributed programs and hardware by automatically deriving correct implementations from formal specifications. For synchronous distributed systems, the synthesis problem is well known to be undecidable. For asynchronous systems, the boundary between decidable and undecidable synthesis problems is a long-standing open question. We study the problem in the setting of Petri games, a framework for distributed systems where asynchronous processes are equipped with causal memory. Petri games extend Petri nets with a distinction between system places and environment places. The components of a distributed system are the players of the game, represented as tokens that exchange information during each synchronization. Previous decidability results for this model are limited to local winning conditions, i.e., conditions that only refer to individual components. In this paper, we consider global winning conditions such as mutual exclusion, i.e., conditions that refer to the state of all components. We provide decidability and undecidability results for global winning conditions. First, we prove for winning conditions given as bad markings that it is decidable whether a winning strategy for the system players exists in Petri games with a bounded number of system players and one environment player. Second, we prove for winning conditions that refer to both good and bad markings that it is undecidable whether a winning strategy for the system players exists in Petri games with at least two system players and one environment player. Our results thus show that, on the one hand, it is indeed possible to use global safety specifications like mutual exclusion in the synthesis of distributed systems. However, on the other hand, adding global liveness specifications results in an undecidable synthesis problem for almost all Petri games.

Cite as

Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, and Ernst-Rüdiger Olderog. Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{finkbeiner_et_al:LIPIcs.CSL.2022.20,
  author =	{Finkbeiner, Bernd and Gieseking, Manuel and Hecking-Harbusch, Jesko and Olderog, Ernst-R\"{u}diger},
  title =	{{Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{20:1--20:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.20},
  URN =		{urn:nbn:de:0030-drops-157400},
  doi =		{10.4230/LIPIcs.CSL.2022.20},
  annote =	{Keywords: Synthesis, distributed systems, reactive systems, Petri games, decidability}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail