Search Results

Documents authored by Olderog, Ernst-Rüdiger

Document
DOI: 10.4230/LIPIcs.CSL.2022.20
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}
}
Document
DOI: 10.4230/DagSemRep.144
Semantics of Concurrent Systems - Foundations and Applications (Dagstuhl Seminar 9619)

Authors: Manfred Droste, Ernst-Rüdiger Olderog, Bernhard Steffen, and Glynn Winskel

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Manfred Droste, Ernst-Rüdiger Olderog, Bernhard Steffen, and Glynn Winskel. Semantics of Concurrent Systems - Foundations and Applications (Dagstuhl Seminar 9619). Dagstuhl Seminar Report 144, pp. 1-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1996)

Copy BibTex To Clipboard

@TechReport{droste_et_al:DagSemRep.144,
  author =	{Droste, Manfred and Olderog, Ernst-R\"{u}diger and Steffen, Bernhard and Winskel, Glynn},
  title =	{{Semantics of Concurrent Systems - Foundations and Applications (Dagstuhl Seminar 9619)}},
  pages =	{1--18},
  ISSN =	{1619-0203},
  year =	{1996},
  type = 	{Dagstuhl Seminar Report},
  number =	{144},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.144},
  URN =		{urn:nbn:de:0030-drops-150310},
  doi =		{10.4230/DagSemRep.144},
}
Document
DOI: 10.4230/DagSemRep.9
Concurrent Systems: Semantics, Specification, and Synthesis (Dagstuhl Seminar 9111)

Authors: Manfred Broy, Peter Deussen, Ernst-Rüdiger Olderog, and Willem-Paul de Roever

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Manfred Broy, Peter Deussen, Ernst-Rüdiger Olderog, and Willem-Paul de Roever. Concurrent Systems: Semantics, Specification, and Synthesis (Dagstuhl Seminar 9111). Dagstuhl Seminar Report 9, pp. 1-20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1991)

Copy BibTex To Clipboard

@TechReport{broy_et_al:DagSemRep.9,
  author =	{Broy, Manfred and Deussen, Peter and Olderog, Ernst-R\"{u}diger and de Roever, Willem-Paul},
  title =	{{Concurrent Systems: Semantics, Specification, and Synthesis (Dagstuhl Seminar 9111)}},
  pages =	{1--20},
  ISSN =	{1619-0203},
  year =	{1991},
  type = 	{Dagstuhl Seminar Report},
  number =	{9},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.9},
  URN =		{urn:nbn:de:0030-drops-148970},
  doi =		{10.4230/DagSemRep.9},
}
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact