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 parallel to 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 co-synthesis problem, where the proponent A consists itself of two independent processes, A = A(1)parallel to 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)parallel to A(2)parallel to B satisfies Phi(1) boolean AND 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) (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 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, competes with A(2) but not at the price of violating Phi(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.
This research was supported in part by the Swiss National Science Foundation and by the NSF grants CCR-0225610 and CCR-0234690.
261 - 275
TACAS: Tools and Algorithms for the Construction and Analysis of Systems
Chatterjee K, Henzinger TA. Assume-guarantee synthesis. In: Vol 4424. Springer; 2007:261-275. doi:10.1007/978-3-540-71209-1_21
Chatterjee, K., & Henzinger, T. A. (2007). Assume-guarantee synthesis (Vol. 4424, pp. 261–275). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Springer. https://doi.org/10.1007/978-3-540-71209-1_21
Chatterjee, Krishnendu, and Thomas A Henzinger. “Assume-Guarantee Synthesis,” 4424:261–75. Springer, 2007. https://doi.org/10.1007/978-3-540-71209-1_21.
K. Chatterjee and T. A. Henzinger, “Assume-guarantee synthesis,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, 2007, vol. 4424, pp. 261–275.
Chatterjee K, Henzinger TA. 2007. Assume-guarantee synthesis. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 4424, 261–275.
Chatterjee, Krishnendu, and Thomas A. Henzinger. Assume-Guarantee Synthesis. Vol. 4424, Springer, 2007, pp. 261–75, doi:10.1007/978-3-540-71209-1_21.