Abstract
The automatic synthesis of programs from their specifications has been a dream of many researchers for decades. If we restrict to open finite-state reactive systems, the specification is often presented as an ATL or LTL formula interpreted over a finite-state game. The required program is then a strategy for winning this game. A theoretically optimal solution to this problem was proposed by Pnueli and Rosner, but has never given good results in practice. This is due to the 2EXPTIME-complete complexity of the problem, and the intricate nature of Pnueli and Rosner’s solution. A key difficulty in their procedure is the determinisation of Büchi automata. In this paper we look at an alternative approach which avoids determinisation, using instead a procedure that is amenable to symbolic methods. Using an implementation based on the BDD package CuDD, we demonstrate its scalability in a number of examples. Furthermore, we show a class of problems for which our algorithm is singly exponential. Our solution, however, is not complete; we prove a condition which guarantees completeness and argue by empirical evidence that examples for which it is not complete are rare enough to make our solution a useful tool.
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
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. Journal of the ACM 49(5), 672–713 (2002)
Alur, R., La Torre, S.: Deterministic generators and games for LTL fragments. ACM Transactions on Computational Logic 5(1), 1–25 (2004)
SMV 10-11-02p1 (November 2002), http://www-cad.eecs.berkeley.edu/~kenmcmil/smv/
Clarke, E., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 415–427. Springer, Heidelberg (1994)
CuDD: Colorado university decision diagram package, release 2.30 (February 2001), http://vlsi.colorado.edu/~fabio/CUDD/
Emerson, E.A.: Handbook of Theoretical Computer Science. In: chapter Temporal and Modal Logic, vol. B, pp. 995–1072. Elsevier, Amsterdam (1990)
Emerson, E.A., Lei, C.: Efficient model checking in fragments of the propositional model mu-calculus. In: IEEE Symposium on Logic in Computer Science, pp. 267–278 (June 1986)
Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002)
Kremer, S., Raskin, J.-F.: A game-based verification of non-repudiation and fair exchange protocols. Journal Of Computer Security 11(3), 399–429 (2003)
Kupferman, O., Vardi, M.Y.: Module checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 75–86. Springer, Heidelberg (1996)
Löding, C.: Optimal bounds for the transformation of ω-automata. In: Pandu Rangan, C., Raman, V., Sarukkai, S. (eds.) FST TCS 1999. LNCS, vol. 1738, pp. 97–109. Springer, Heidelberg (1999)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings Of 16th ACM Symposium On Principles Of Programming Languages, pp. 179–190 (1989)
Rosner, R.: Modular Synthesis of Reactive Systems. PhD thesis, Weizmann Institute of Science, Rehovot, Israel (1992)
Safra, S.: Complexity of Automata on Infinite Objects. PhD thesis, The Weizmann Institute of Science, Rehovot, Israel (March 1989)
Schneider, K.: Improving automata generation for linear temporal logic by considering the automaton hierarchy. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, p. 39. Springer, Heidelberg (2001)
Somenzi, F., Ravi, K., Bloem, R.: Analysis of symbolic scc hull algorithms. In: Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design, pp. 88–105. Springer, Heidelberg (2002)
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)
Thomas, W.: Handbook of Theoretical Computer Science. In: chapter Automata on Infinite Objects, vol. B, pp. 133–192. Elsevier, Amsterdam (1990)
Thomas, W.: On the synthesis of strategies in infinite games. In: Symposium on Theoretical Aspects of Computer Science, pp. 1–13 (1995)
Wallmeier, N., Hütten, P., Thomas, W.: Symbolic synthesis of finite-state controllers for request-response specifications. In: Ibarra, O.H., Dang, Z. (eds.) CIAA 2003. LNCS, vol. 2759, pp. 11–22. Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Harding, A., Ryan, M., Schobbens, PY. (2005). A New Algorithm for Strategy Synthesis in LTL Games. In: Halbwachs, N., Zuck, L.D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2005. Lecture Notes in Computer Science, vol 3440. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31980-1_31
Download citation
DOI: https://doi.org/10.1007/978-3-540-31980-1_31
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25333-4
Online ISBN: 978-3-540-31980-1
eBook Packages: Computer ScienceComputer Science (R0)