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)

Citation formats

• 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
                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 ɸ1 and ɸ2,
                and the goal is to refine both A and
                A2 so that
                A1||A2||B
                satisfies ɸ1 ^ ɸ2.
                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 ɸ1, 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.},
      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..

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.