2014/11/17 by Roderick Bloem, Bloem, Roderick, Krishnendu Chatterjee +5
Computer Science · #Advanced Software Engineering Methodologies #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1411.4604
openalex publication_date 2014/11/17 · openalex created_date 2025/10/24 · openalex updated_date 2026/07/28
Synthesis of program parts is very useful for concurrent systems. However,\nmost synthesis approaches do not support common design tasks, like modifying a\nsingle process without having to re-synthesize or verify the whole system.\nAssume-guarantee synthesis (AGS) provides robustness against modifications of\nsystem parts, but thus far has been limited to the perfect information setting.\nThis means that local variables cannot be hidden from other processes, which\nrenders synthesis results cumbersome or even impossible to realize. We resolve\nthis shortcoming by defining AGS in a partial information setting. We analyze\nthe complexity and decidability in different settings, showing that the problem\nhas a high worst-case complexity and is undecidable in many interesting cases.\nBased on these observations, we present a pragmatic algorithm based on bounded\nsynthesis, and demonstrate its practical applicability on several examples.\n