Advertisement

A New Algorithm for Strategy Synthesis in LTL Games

  • Aidan Harding
  • Mark Ryan
  • Pierre-Yves Schobbens
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3440)

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.

Keywords

Model Check Mutual Exclusion Linear Temporal Logic Winning Strategy Strategy Synthesis 
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

  1. 1.
    Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. Journal of the ACM 49(5), 672–713 (2002)CrossRefMathSciNetGoogle Scholar
  2. 2.
    Alur, R., La Torre, S.: Deterministic generators and games for LTL fragments. ACM Transactions on Computational Logic 5(1), 1–25 (2004)CrossRefMathSciNetGoogle Scholar
  3. 3.
    SMV 10-11-02p1 (November 2002), http://www-cad.eecs.berkeley.edu/~kenmcmil/smv/
  4. 4.
    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)Google Scholar
  5. 5.
    CuDD: Colorado university decision diagram package, release 2.30 (February 2001), http://vlsi.colorado.edu/~fabio/CUDD/
  6. 6.
    Emerson, E.A.: Handbook of Theoretical Computer Science. In: chapter Temporal and Modal Logic, vol. B, pp. 995–1072. Elsevier, Amsterdam (1990)Google Scholar
  7. 7.
    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)Google Scholar
  8. 8.
    Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002)Google Scholar
  9. 9.
    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)Google Scholar
  10. 10.
    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)Google Scholar
  11. 11.
    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)CrossRefGoogle Scholar
  12. 12.
    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)Google Scholar
  13. 13.
    Rosner, R.: Modular Synthesis of Reactive Systems. PhD thesis, Weizmann Institute of Science, Rehovot, Israel (1992)Google Scholar
  14. 14.
    Safra, S.: Complexity of Automata on Infinite Objects. PhD thesis, The Weizmann Institute of Science, Rehovot, Israel (March 1989)Google Scholar
  15. 15.
    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)CrossRefGoogle Scholar
  16. 16.
    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)CrossRefGoogle Scholar
  17. 17.
    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)Google Scholar
  18. 18.
    Thomas, W.: Handbook of Theoretical Computer Science. In: chapter Automata on Infinite Objects, vol. B, pp. 133–192. Elsevier, Amsterdam (1990)Google Scholar
  19. 19.
    Thomas, W.: On the synthesis of strategies in infinite games. In: Symposium on Theoretical Aspects of Computer Science, pp. 1–13 (1995)Google Scholar
  20. 20.
    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)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Aidan Harding
    • 1
  • Mark Ryan
    • 1
  • Pierre-Yves Schobbens
    • 2
  1. 1.School of Computer ScienceThe University of BirminghamEdgbaston, BirminghamUK
  2. 2.Institut d’InformatiqueFacultés Universitaires de NamurNamurBelgium

Personalised recommendations