CISPA
Browse
cispa_all_3676.pdf (803.37 kB)

Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory

Download (803.37 kB)
conference contribution
posted on 2023-11-29, 18:20 authored by Bernd FinkbeinerBernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, Ernst-Rüdiger Olderog
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.

History

Preferred Citation

Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch and Ernst-Rüdiger Olderog. Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory. In: Annual Conference on Computer Science Logic (CSL). 2022.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

Annual Conference on Computer Science Logic (CSL)

Legacy Posted Date

2022-05-07

Open Access Type

  • Green

BibTeX

@inproceedings{cispa_all_3676, title = "Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory", author = "Finkbeiner, Bernd and Gieseking, Manuel and Hecking-Harbusch, Jesko and Olderog, Ernst-Rüdiger", booktitle="{Annual Conference on Computer Science Logic (CSL)}", year="2022", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC