Krishnendu Chatterjee and Thomas A. Henzinger

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2006-32

April 4, 2006

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~$\Phi$. 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 {\em co-synthesis} problem, where the proponent $A$ consists itself of two independent processes, $A=A_1||A_2$, with specifications $\Phi_1$ and $\Phi_2$, and the goal is to refine both $A_1$ and $A_2$ so that $A_1||A_2||B$ satisfies $\Phi_1\wedge\Phi_2$. For example, if the opponent $B$ is a fair scheduler for the two processes $A_1$ and~$A_2$, and $\Phi_i$ specifies the requirements of mutual exclusion for~$A_i$ (such as mutex, bounded overtaking, and 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 $A_1$ and $A_2$ either collaborating or competing, does not capture desirable solutions. Instead, the proper formulation of co-synthesis is the one where process $A_1$ competes with $A_2$ but not at the price of violating~$\Phi_1$, and vice versa. We call this {\em assume-guarantee synthesis} and show that it can be solved by computing secure-equilibrium strategies. In particular, from mutual-exclusion requirements our assume-guarantee synthesis algorithm automatically computes Peterson's protocol.

---

BibTeX citation:

@techreport{Chatterjee:EECS-2006-32,
    Author= {Chatterjee, Krishnendu and Henzinger, Thomas A.},
    Title= {Assume Guarantee Synthesis},
    Year= {2006},
    Month= {Apr},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-32.html},
    Number= {UCB/EECS-2006-32},
    Abstract= {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~$\Phi$.  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 {\em co-synthesis} problem, where the proponent $A$ consists itself of two independent processes, $A=A_1||A_2$, with specifications $\Phi_1$ and $\Phi_2$, and the goal is to refine both $A_1$ and $A_2$ so that $A_1||A_2||B$ satisfies $\Phi_1\wedge\Phi_2$.  For example, if the opponent $B$ is a fair scheduler for the two processes $A_1$ and~$A_2$, and $\Phi_i$ specifies the requirements of mutual exclusion for~$A_i$ (such as mutex, bounded overtaking, and 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 $A_1$ and $A_2$ either collaborating or competing, does not capture desirable solutions.  Instead, the proper formulation of co-synthesis is the one where process $A_1$ competes with $A_2$ but not at the price of violating~$\Phi_1$, and vice versa. We call this {\em assume-guarantee synthesis} and show that it can be solved by computing secure-equilibrium strategies.  In particular, from mutual-exclusion requirements our assume-guarantee synthesis algorithm automatically computes Peterson's protocol.},
}

EndNote citation:

%0 Report
%A Chatterjee, Krishnendu 
%A Henzinger, Thomas A. 
%T Assume Guarantee Synthesis
%I EECS Department, University of California, Berkeley
%D 2006
%8 April 4
%@ UCB/EECS-2006-32
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-32.html
%F Chatterjee:EECS-2006-32