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 = A 1||A 2, with specifications Φ 1 and Φ 2, and the goal is to refine both A 1 and A 2 so that A 1||A 2||B satisfies Φ 1 ∧ Φ 2. For example, if the opponent B is a fair scheduler for the two processes A 1 and A 2, and Φ 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 1 competes with A 2 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.
This research was supported in part by the Swiss National Science Foundation and by the NSF grants CCR-0225610 and CCR-0234690.
Chapter PDF
References
Alur, R., Henzinger, T.A.: Reactive modules. Formal Methods in System Design 15, 7–48 (1999)
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. Journal of the ACM 49, 672–713 (2002)
Chatterjee, K., Henzinger, T.A.: Semiperfect-information games. In: Ramanujam, R., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 1–18. Springer, Heidelberg (2005)
Chatterjee, K., Henzinger, T.A., Jurdziński, M.: Games with secure equilibria. In: LICS’04, pp. 160–169. IEEE Computer Society Press, Los Alamitos (2004)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)
Gurevich, Y., Harrington, L.: Trees, automata, and games. In: STOC’82, pp. 60–65. ACM Press, New York (1982)
Henzinger, T.A., et al.: Abstract interpretation of game properties. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 220–239. Springer, Heidelberg (2000)
Madhususan, P., Thiagarajan, P.S.: Distributed controller synthesis for local specifications. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 396–407. Springer, Heidelberg (2001)
Mohalik, S., Walukiewicz, I.: Distributed games. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 338–351. Springer, Heidelberg (2003)
Papadimitriou, C.H.: Algorithms, games, and the internet. In: STOC’01, pp. 749–753. ACM Press, New York (2001)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL’89, pp. 179–190. ACM Press, New York (1989)
Ramadge, P.J., Wonham, W.M.: Supervisory control of a class of discrete-event processes. SIAM Journal of Control and Optimization 25, 206–230 (1987)
Reif, J.H.: The complexity of 2-player games of incomplete information. Journal of Computer and System Sciences 29, 274–301 (1984)
Thomas, W.: Languages, automata, and logic. In: Handbook of Formal Languages, vol. 3, pp. 389–455. Springer, Heidelberg (1997)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Chatterjee, K., Henzinger, T.A. (2007). Assume-Guarantee Synthesis. In: Grumberg, O., Huth, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2007. Lecture Notes in Computer Science, vol 4424. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71209-1_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-71209-1_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71208-4
Online ISBN: 978-3-540-71209-1
eBook Packages: Computer ScienceComputer Science (R0)