2005 | OriginalPaper | Chapter
Synthesis of Distributed Systems from Knowledge-Based Specifications
Authors : Ron van der Meyden, Thomas Wilke
Published in: CONCUR 2005 – Concurrency Theory
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
We consider the problem of synthesizing protocols in a distributed setting satisfying specifications phrased in the logic of linear time
and
knowledge. On the one hand, we show that synthesis is already undecidable in environments with just two agents, one of which observes every aspect of the system state and one of which observes nothing of it. This falsifies a conjecture of van der Meyden and Vardi from CONCUR’96. On the other hand, we prove that synthesis is decidable in broadcast environments, verifying a conjecture of van der Meyden and Vardi from the same paper, and we show that for specifications that are positive in the knowledge modalities the synthesis problem can be reduced to the same problem for formulas without knowledge modalities. After adapting Pnueli and Rosner’s decidability result on synthesis for linear temporal logic specifications in hierarchical environments, we obtain that, in our setting, synthesis is decidable for specifications positive in the knowledge modalities when restricted to hierarchical environments. We conclude the decidability in hierarchical systems of a property closely related to nondeducibility on strategies, a notion that has been studied in computer security.