Citation
Krishnendu Chatterjee, Tom Henzinger. "Assume-guarantee Synthesis". TACAS, March, 2007.

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 ɸ. 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 ɸ₁ and ɸ₂, and the goal is to refine both A and A2 so that A1||A2||B satisfies ɸ₁ ^ ɸ₂. For example, if the opponent B is a fair scheduler for the two processes A1 and A2, and ɸ_i specifies the requirements of mutual exclusion for Ai (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 ɸ₁, 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.

Electronic downloads

• main.ps · application/postscript · 427 kbytes
• Chatterjee_Henzinger_assume-guarantee-synthesis_TACAS2007.pdf · application/pdf · 200 kbytes. (pdf version of main.ps)

• HTML

  Krishnendu Chatterjee, Tom Henzinger. <a
  href="http://chess.eecs.berkeley.edu/pubs/240.html"
  >Assume-guarantee Synthesis</a>, TACAS, March, 2007.

• Plain text

  Krishnendu Chatterjee, Tom Henzinger. "Assume-guarantee
  Synthesis". TACAS, March, 2007.

• BibTeX

  @inproceedings{ChatterjeeHenzinger07_AssumeguaranteeSynthesis,
      author = {Krishnendu Chatterjee and Tom Henzinger},
      title = {Assume-guarantee Synthesis},
      booktitle = {TACAS},
      month = {March},
      year = {2007},
      abstract = {The classical synthesis problem for reactive
                systems asks, given a proponent process
                <code>A</code> and an opponent process
                <code>B</code>, to refine <code>A</code> so that
                the closed-loop system <code>A||B</code> satisfies
                a given specification ɸ. The solution of this
                problem requires the computation of a winning
                strategy for proponent <code>A</code> in a game
                against opponent <code>B</code>. We define and
                study the <i>co-synthesis</i> problem, where the
                proponent <code>A</code> consists itself of two
                independent processes,
                <code>A=A<sub>1</sub>||A<sub>2</sub></code>, with
                specifications ɸ<sub>1</sub> and ɸ<sub>2</sub>,
                and the goal is to refine both <code>A</code> and
                <code>A<sub>2</sub></code> so that
                <code>A<sub>1</sub>||A<sub>2</sub>||B</code>
                satisfies ɸ<sub>1</sub> ^ ɸ<sub>2</sub></code>.
                For example, if the opponent <code>B</code> is a
                fair scheduler for the two processes
                <code>A<sub>1</sub></code> and
                <code>A<sub>2</sub></code>, and
                ɸ<sub>i</sub></code> specifies the requirements
                of mutual exclusion for <code>A<sub>i</sub></code>
                (e.g., starvation freedom), then the co-synthesis
                problem asks for the automatic synthesis of a
                mutual-exclusion protocol. <p>We show that
                co-synthesis defined classically, with the
                processes <code>A<sub>1</sub></code> and
                <code>A<sub>2</sub></code> either collaborating or
                competing, does not capture desirable solutions.
                Instead, the proper formulation of co-synthesis is
                the one where process <code>A<sub>1</sub></code>
                competes with <code>A<sub>2</sub></code> but not
                at the price of violating ɸ<sub>1</sub>, and vice
                versa. We call this <i> assume-guarantee
                synthesis</i> 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.},
      URL = {http://chess.eecs.berkeley.edu/pubs/240.html}
  }
  

Posted by Krishnendu Chatterjee, PhD on 13 May 2007.
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.