# 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://www2.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}, 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