Abstract
In automated synthesis, we transform a specification into a system that is guaranteed to satisfy the specification. In spite of the rich theory developed for system synthesis, little of this theory has been reduced to practice. This is in contrast with model-checking theory, which has led to industrial development and use of formal verification tools. We see two main reasons for the lack of practical impact of synthesis. The first is algorithmic: synthesis involves determinization of automata on infinite words, and a solution of parity games with highly complex state spaces; both problems have been notoriously resistant to efficient implementation. The second is methodological: current theory of synthesis assumes a single comprehensive specification. In practice, however, the specification is composed of a set of properties, which is typically evolving – properties may be added, deleted, or modified.
In this work we address both issues. We extend the Safraless synthesis algorithm of Kupferman and Vardi so that it handles LTL formulas by translating them to nondeterministic generalized Büchi automata. This leads to an exponential improvement in the complexity of the algorithm. Technically, our algorithm reduces the synthesis problem to the emptiness problem of a nondeterministic Büchi tree automaton \({\cal A}\). The generation of \({\cal A}\) avoids determinization, avoids the parity acceptance condition, and is based on an analysis of runs of universal generalized co-Büchi tree automata. The clean and simple structure of \({\cal A}\) enables optimizations and a symbolic implementation. In addition, it makes it possible to use information gathered during the synthesis process of properties in the process of synthesizing their conjunction.
A full version with full proofs can be downloaded from www.cs.huji.ac.il/~ornak/cav06.pdf.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abadi, M., Lamport, L., Wolper, P.: Realizable and unrealizable concurrent program specifications. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol. 372, pp. 1–17. Springer, Heidelberg (1989)
Althoff, C.S., Thomas, W., Wallmeier, N.: Observations on determinization of büchi automata. In: Farré, J., Litovsky, I., Schmitz, S. (eds.) CIAA 2005. LNCS, vol. 3845, pp. 262–272. Springer, Heidelberg (2006)
Choueka, Y.: Theories of automata on ω-tapes: A simplified approach. JCSS 8, 117–141 (1974)
Church, A.: Logic, arithmetics, and automata. In: ICM 1962, pp. 23–35 (1963)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Dill, D.L.: Trace theory for automatic hierarchical verification of speed independent circuits. MIT Press, Cambridge (1989)
Elgaard, J., Klarlund, N., Möller, A.: Mona 1.x: new techniques for WS1S and WS2S. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 516–520. Springer, Heidelberg (1998)
Emerson, E.A.: Automata, tableaux, and temporal logics. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol. 193, pp. 79–87. Springer, Heidelberg (1985)
Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Protocol Specification, Testing, and Verification, pp. 3–18 (1995)
Grädel, E., Thomas, W., Wilke, T.: Automata, Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002)
Gurumurthy, S., Kupferman, O., Somenzi, F., Vardi, M.Y.: On complementing nondeterministic Büchi automata. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 96–110. Springer, Heidelberg (2003)
Harding, A., Ryan, M., Schobbens, P.Y.: A new algorithm for strategy synthesis in ltl games. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 477–492. Springer, Heidelberg (2005)
JurzińSki, M.: Small progress measures for solving parity games. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 290–301. Springer, Heidelberg (2000)
Kupferman, O., Vardi, M.Y.: From complementation to certification. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 591–606. Springer, Heidelberg (2004)
Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: 46th FOCS (2005)
Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: 12th POPL, pp. 97–107 (1985)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1992)
Miyano, S., Hayashi, T.: Alternating finite automata on ω-words. TCS 32, 321–330 (1984)
Mostowski, A.W.: Regular expressions for infinite trees and a standard form of automata. In: Skowron, A. (ed.) SCT 1984. LNCS, vol. 208, pp. 157–168. Springer, Heidelberg (1985)
Muller, D.E., Saoudi, A., Schupp, P.E.: Alternating automata, the weak monadic theory of the tree and its complexity. In: Kott, L. (ed.) ICALP 1986. LNCS, vol. 226. Springer, Heidelberg (1986)
Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. In: 25th LICS (to appear, 2006)
Piterman, N., Pnueli, A., Saar, Y.: Design synthesis in action: Solving a 2exptime-complete problem in n 3. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 364–380. Springer, Heidelberg (2005)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: 16th POPL, pp. 179–190 (1989)
Rabin, M.O.: Weakly definable relations and special automata. In: Symp. Math. Logic and Foundations of Set Theory, pp. 1–23 (1970)
Rabin, M.O.: Automata on infinite objects and Church’s problem. In: AMS (1972)
Rosner, R.: Modular Synthesis of Reactive Systems. PhD thesis, Weizmann Institute of Science (1992)
Safra, S.: On the complexity of ω-automata. In: 29th FOCS, pp. 319–327 (1988)
Safra, S.: Exponential determinization for ω-automata with strong-fairness acceptance condition. In: 24th STOC (1992)
Tasiran, S., Hojati, R., Brayton, R.K.: Language containment using non-deterministic omega-automata. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol. 987, pp. 261–277. Springer, Heidelberg (1995)
Vardi, M.Y., Wolper, P.: Automata-theoretic techniques for modal logics of programs. JCSS 32(2), 182–221 (1986)
Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. IC 115(1), 1–37 (1994)
Yang, J., Seger, C.J.H.: Introduction to generalized symbolic trajectory evaluation. In: 19th DAC, pp. 360–367. IEEE, Los Alamitos (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kupferman, O., Piterman, N., Vardi, M.Y. (2006). Safraless Compositional Synthesis. In: Ball, T., Jones, R.B. (eds) Computer Aided Verification. CAV 2006. Lecture Notes in Computer Science, vol 4144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11817963_6
Download citation
DOI: https://doi.org/10.1007/11817963_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37406-0
Online ISBN: 978-3-540-37411-4
eBook Packages: Computer ScienceComputer Science (R0)