Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information

TL;DR

This paper extends assume-guarantee synthesis to partial information settings in concurrent reactive programs, addressing limitations of previous perfect information approaches and providing a practical bounded synthesis algorithm.

Contribution

It introduces a new partial information framework for AGS, analyzes its complexity and decidability, and offers a pragmatic bounded synthesis algorithm for real-world applications.

Findings

AGS is undecidable in many cases under partial information.

The proposed bounded synthesis algorithm is practically applicable.

Complexity analysis reveals high worst-case difficulty.

Abstract

Synthesis of program parts is very useful for concurrent systems. However, most synthesis approaches do not support common design tasks, like modifying a single process without having to re-synthesize or verify the whole system. Assume-guarantee synthesis (AGS) provides robustness against modifications of system parts, but thus far has been limited to the perfect information setting. This means that local variables cannot be hidden from other processes, which renders synthesis results cumbersome or even impossible to realize. We resolve this shortcoming by defining AGS in a partial information setting. We analyze the complexity and decidability in different settings, showing that the problem has a high worst-case complexity and is undecidable in many interesting cases. Based on these observations, we present a pragmatic algorithm based on bounded synthesis, and demonstrate its practical applicability on several examples.