Electrical Engineering
      and Computer Sciences

Electrical Engineering and Computer Sciences

COLLEGE OF ENGINEERING

UC Berkeley

Assume Guarantee Synthesis

Krishnendu Chatterjee and Thomas A. Henzinger

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2006-32
April 4, 2006

http://www.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-32.pdf

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},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2006},
    Month = {Apr},
    URL = {http://www.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://www.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-32.html
%F Chatterjee:EECS-2006-32