*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 *p1*and *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.