English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

In the synthesis of distributed systems, we automate the development ofdistributed programs and hardware by automatically deriving correctimplementations from formal specifications. For synchronous distributedsystems, the synthesis problem is well known to be undecidable. Forasynchronous systems, the boundary between decidable and undecidable synthesisproblems is a long-standing open question. We study the problem in the settingof Petri games, a framework for distributed systems where asynchronousprocesses are equipped with causal memory. Petri games extend Petri nets with adistinction between system places and environment places. The components of adistributed system are the players of the game, represented as tokens thatexchange information during each synchronization. Previous decidability resultsfor this model are limited to local winning conditions, i.e., conditions thatonly refer to individual components. In this paper, we consider global winningconditions such as mutual exclusion, i.e., conditions that refer to the stateof all components. We provide decidability and undecidability results forglobal winning conditions. First, we prove for winning conditions given as badmarkings that it is decidable whether a winning strategy for the system playersexists in Petri games with a bounded number of system players and oneenvironment player. Second, we prove for winning conditions that refer to bothgood and bad markings that it is undecidable whether a winning strategy for thesystem players exists in Petri games with at least two system players and oneenvironment player. Our results thus show that, on the one hand, it is indeedpossible to use global safety specifications like mutual exclusion in thesynthesis of distributed systems. However, on the other hand, adding globalliveness specifications results in an undecidable synthesis problem for almostall Petri games.

Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory (Full Version)