Assume-Guarantee Synthesis

Krishnendu Chatterjee and Thomas A. Henzinger

The classical synthesis problem for reactive systems asks, given a proponent process A and an opponent process B, to refine A so that the closed-loop system A||B satisfies a given specification p. The solution of this problem requires the computation of a winning strategy for proponent A in a game against opponent B. We define and study the co-synthesis problem, where the proponent A consists itself of two independent processes, A=A1||A2, with specifications p1and p2, and the goal is to refine both A1 and A2 so that A1||A2||B satisfies p1∧p2. For example, if the opponent B is a fair scheduler for the two processes A1 and A2, and p-i specifies the requirements of mutual exclusion for A-i (e.g., starvation freedom), then the co-synthesis problem asks for the automatic synthesis of a mutual-exclusion protocol.

We show that co-synthesis defined classically, with the processes A1 and A2 either collaborating or competing, does not capture desirable solutions. Instead, the proper formulation of co-synthesis is the one where process A1 competes with A2 but not at the price of violating p1, and vice versa. We call this assume-guarantee synthesis and show that it can be solved by computing secure-equilibrium strategies. In particular, from mutual-exclusion requirements the assume-guarantee synthesis algorithm automatically computes Peterson's protocol.

Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science 4424, Springer, 2007, pp. 261-275.

Download inofficial, sometimes updated PostScript / PDF document. © 2007 Springer.