Skip to main content
SpringerLink
Log in

From Logic to Games

  • Conference paper
FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2005)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 3821))

  • 719 Accesses

Abstract

The occasion of 25th jubilee of FSTCS gives an opportunity to look a bit further back then one normally would. In this presentation we will look at some developments in what is called formal verification. In the seventies logics occupied a principal place: Hoare logic [43], algorithmic logic [38], dynamic logic [41, 42], linear time temporal logic [55]. With a notable exception of the last one, these formalisms included programs into syntax of the logic with an idea to reduce verification to validity checking. Temporal logic was the first to advocate externalization of modeling of programs and passing from validity checking to model checking. Since the eighties, this view became predominant, and we have seen a proliferation of logical systems. We have learned that game based methods not only are very useful but also permit to abstract from irrelevant details of logical formalisms. At present games themselves take place of specification formalisms.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Bernadsky, M., Madhusudan, P.: Optimal reachability for weighted timed games. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 122–133. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  2. Alur, R., Madhusudan, P.: Decision problems for timed automata: A survey. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 1–24. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  3. Arnold, A.: The mu-calculus alternation-depth hierarchy is strict on binary trees. RAIRO–Theoretical Informatics and Applications 33, 329–339 (1999)

    Article  MATH  Google Scholar 

  4. Arnold, A., Niwiski, D.: The Rudiments of the Mu-Calculus. In: Studies in Logic, vol. 146, North-Holand, Amsterdam (2001)

    Google Scholar 

  5. Arnold, A., Santocanale, L.: Ambiguous classes in the games mu-calculus hierarchy. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 70–86. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  6. Arnold, A., Vincent, A., Walukiewicz, I.: Games for synthesis of controllers with partial observation. Theoretical Computer Science 303(1), 7–34 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  7. Asarin, E., Maler, O., Pnueli, A., Sifakis, J.: Contrloller synthesis for timed automata. In: Proc. IFAC Symp. System Structure and Control, pp. 469–474 (1998)

    Google Scholar 

  8. Berwanger, D., Grädel, E.: Entanglement - a measure for the complexity of directed graphs with applications to logic and games. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol. 3452, pp. 209–223. Springer, Heidelberg (2004)

    Google Scholar 

  9. Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Applications to model checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997)

    Google Scholar 

  10. Bouajjani, A., Mueller-Olm, M., Touili, T.: Regular symbolic analysis of dynamic networks of pushdown systems. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 473–487. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  11. Bouquet, A., Serre, O., Walukiewicz, I.: Pushdown games with the unboundedness and regular conditions. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 88–99. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  12. Bouyer, P., Cassez, F., Fleury, E., Larsen, K.G.: Optimal strategies in priced timed game automata. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 148–160. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  13. Bouyer, P., D’Souza, D., Madhusudan, P., Petit, A.: Timed control with partial observability. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 180–192. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  14. Bradfield, J.: The modal mu-calculus alternation hierarchy is strict. Theoretical. Computer Science 195, 133–153 (1997)

    MathSciNet  Google Scholar 

  15. Bradfield, J.: Fixpoint alternation: Arithmetic, transition systems, and the binary tree. RAIRO–Theoretical Informatics and Applications 33, 341–356 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  16. Büchi, J.R.: On the decision method in restricted second-order arithmetic. In: Proc. Internat. Congr. on Logic, Methodology and Philosophy of Science, pp. 1–11. Stanford Univ. Press, Stanford (1960)

    Google Scholar 

  17. Buchi, J.R.: State strategies for games in Fσδ ∩ Gδσ. Journal of Symbolic Logic 48, 1171–1198 (1983)

    Article  MathSciNet  Google Scholar 

  18. Cachat, T.: Symbolic strategy synthesis for games on pushdown graphs. In: Widmayer, P., et al. (eds.) ICALP 2002. LNCS, vol. 2380, pp. 704–715. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  19. Cachat, T.: Uniform solution of parity games on prefix-recognizable graphs. In: Kucera, A., Mayr, R. (eds.) Proceedings of the 4th International Workshop on Verification of Infinite-State Systems. Electronic Notes in Theoretical Computer Science, vol. 68, Elsevier Science Publishers, Amsterdam (2002)

    Google Scholar 

  20. Cassandras, C.G., Lafortune, S.: Introduction to Discrete Event Systems. Kluwer Academic Publishers, Dordrecht (1999)

    MATH  Google Scholar 

  21. Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 66–80. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  22. Cassez, F., Henzinger, T., Raskin, J.: A comparison of control problems for timed and hybrid systems. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol. 2289, pp. 134–148. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  23. Chandra, K., Kozen, D.C., Stockmeyer, L.J.: Alternation. Journal of the Association of Computing Machinery 28(1), 114–133 (1981)

    MATH  MathSciNet  Google Scholar 

  24. Chatterjee, K.: Two-player nonzero-sum omega-regular games. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 413–427. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  25. Clarke, E., Emerson, E.: 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 (1981)

    Chapter  Google Scholar 

  26. Colcombet, T., Niwiński, D.: On the positional determinacy of edge–labeled games (2004) (submitted)

    Google Scholar 

  27. Courcelle, B., Weil, P.: The recognizability of sets of graphs is a robust property. Theoretical Computer Science (to appear), http://www.labri.fr/Perso/~weil/publications/

  28. de Alfaro, L.: Quantitative verification and control via the mu-calculus. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 102–126. Springer, Heidelberg (2003)

    Google Scholar 

  29. de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: The element of surprise in timed games. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 142–156. Springer, Heidelberg (2003)

    Google Scholar 

  30. Demri, S., Laroussinie, F., Schnoebelen, P.: A parametric analysis of the state exposion problem in model checking. In: Alt, H., Ferreira, A. (eds.) STACS 2002. LNCS, vol. 2285, pp. 620–631. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  31. D’Souza, D., Madhusudan, P.: Timed control synthesis for external specifications. In: Alt, H., Ferreira, A. (eds.) STACS 2002. LNCS, vol. 2285, pp. 571–582. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  32. Dziembowski, S., Jurdzinski, M., Walukiewicz, I.: How much memory is needed to win infinite games. In: LICS, pp. 99–110 (1997)

    Google Scholar 

  33. Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy. In: Proc. FOCS 1991, pp. 368–377 (1991)

    Google Scholar 

  34. Esparza, J., Podelski, A.: Efficient algorithms for pre star and post star on interprocedural parallel flow graphs. In: POPL 2000: Principles of Programming Languages (2000)

    Google Scholar 

  35. Finkbeiner, B., Schewe, S.: Uniform distributed synthesis. In: LICS 2005 (2005)

    Google Scholar 

  36. Gimbert, H.: Parity and explosion games on context-free graphs. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 56–70. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  37. Gimbert, H., Zielonka, W.: When can you play positionally? In: Fiala, J., Koubek, V., Kratochvíl, J. (eds.) MFCS 2004. LNCS, vol. 3153, pp. 686–697. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  38. Mirkowska, G., Salwicki, A.: Algorithmic Logic. D.Reidel PWN (1987)

    Google Scholar 

  39. Grädel, E., Walukiewicz, I.: Positional determinacy of infnite games (2004) (submitted)

    Google Scholar 

  40. Gurevich, Y., Harrington, L.: Trees, automata and games. In: 14th ACM Symp. on Theory of Computations, pp. 60–65 (1982)

    Google Scholar 

  41. Harel, D.: Dynamic logic. In: Handbook of Philosophical Logic vol. II, pp. 497–604. D.Reidel Publishing Company (1984)

    Google Scholar 

  42. Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)

    MATH  Google Scholar 

  43. Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12, 576–585 (1969)

    Article  MATH  Google Scholar 

  44. Hoffman, A., Karp, R.: On nonterminating stochastic games. Management Science 12, 369–370 (1966)

    Article  MathSciNet  Google Scholar 

  45. Aehlig, C.-H.L.O.K., de Miranda, J.G.: The monadic second order theory of trees given by arbitrary level-two recursion schemes is decidable. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 39–54. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  46. Kamp, H.: Tense Logic and the Theory of Linear Order. PhD thesis, University of California (1968)

    Google Scholar 

  47. Knapik, T., Niwinski, D., Urzyczyn, P., Walukiewicz, I.: Unsafe grammars and panic automata. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1450–1461. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  48. Kozen, D.: Results on the propositional mu-calculus. Theoretical Computer Science 27, 333–354 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  49. Kumar, R., Garg, V.K.: Modeling and control of logical discrete event systems. Kluwer Academic Pub., Dordrecht (1995)

    MATH  Google Scholar 

  50. Kupferman, O., Vardi, M.: An automata-theoretic approach to reasoning about infinite-state systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 36–52. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  51. Kupferman, O., Vardi, M.: Synthesizing distributed systems. In: Proc. 16th IEEE Symp. on Logic in Computer Science (2001)

    Google Scholar 

  52. Lamport, L.: sometime is sometimes not never – on the temporal logic of programs. In: POPL 1980, pp. 174–185 (1980)

    Google Scholar 

  53. Madhusudan, P.: Control and Synthesis of Open Reactive Systems. Ph.D thesis, University of Madras (2001)

    Google Scholar 

  54. Madhusudan, P., Thiagarajan, P.: A decidable class of asynchronous distributed controllers. In: Brim, L., et al. (eds.) CONCUR 2002. LNCS, vol. 2421, p. 145. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  55. Manna, Z., Pnueli, A.: Verification of the concurrent programs: the temporal framework. In: Boyer, R., Moore, J. (eds.) The Correctness Problem in Computer Scince, pp. 215–273. Academic Press, London (1981)

    Google Scholar 

  56. Martin, D.: Borel determinacy. Ann. Math. 102, 363–371 (1975)

    Article  Google Scholar 

  57. Martin, D.: The determinacy of Blackwell games. The Journal of Symbolic Logic 63(4), 1565–1581 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  58. McNaughton, R.: Infinite games played on finite graphs. Ann. Pure and Applied Logic 65, 149–184 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  59. Mohalik, S., Walukiewicz, I.: Distributed games. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 338–351. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  60. Mostowski, 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 (1984)

    Google Scholar 

  61. Mostowski, W.: Games with forbidden positions. Technical Report 78, University of Gdansk (1991)

    Google Scholar 

  62. Muller, D., Schupp, P.: The theory of ends, pushdown automata and secondorder logic. Theoretical Computer Science 37, 51–75 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  63. Muller, D., Schupp, P.: Alternating automata on infinite trees. Theoretical. Computer Science 54, 267–276 (1987)

    MATH  MathSciNet  Google Scholar 

  64. Niwiński, D.: On fixed-point clones. In: Kott, L. (ed.) ICALP 1986. LNCS, vol. 226, pp. 464–473. Springer, Heidelberg (1986)

    Google Scholar 

  65. Niwiński, D., Walukiewicz, I.: Relating hierarchies of word and tree automata. In: Meinel, C., Morvan, M. (eds.) STACS 1998. LNCS, vol. 1373, Springer, Heidelberg (1998)

    Google Scholar 

  66. Niwiński, D., Walukiewicz, I.: A gap property of deterministic tree languages. Theoretical Computer Science 303(1), 215–231 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  67. Niwiński, D., Walukiewicz, I.: Deciding nondeterministic hierarchy of deterministic tree automata. Electr. Notes Theor. Comput. Sci. 123, 195–208 (2005)

    Article  Google Scholar 

  68. Obdrzalek, J.: Fast mu-calculus model checking when tree-width is bounded. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 80–92. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  69. Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. ACM POPL, pp. 179–190 (1989)

    Google Scholar 

  70. Rabin, M.: Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc. 141, 1–35 (1969)

    MATH  MathSciNet  Google Scholar 

  71. Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM Journal of Research and Development, 114–125 (1959); Reprinted in Sequential machines (editor E. F. Moore), Addison-Wesley, Reading, Massachusetts, pp. 63-91 (1964)

    Google Scholar 

  72. Ramadge, P.J.G., Wonham, W.M.: The control of discrete event systems. Proceedings of the IEEE 77(2), 81–98 (1989)

    Article  Google Scholar 

  73. Rudie, K., Wonham, W.: Think globally, act locally: Decentralized supervisory control. IEEE Trans. on Automat. Control 37(11), 1692–1708 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  74. Serre, O.: Note on winning positions on pushdown games with ω-regular conditions. Information Processing Letters 85, 285–291 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  75. Serre, O.: Games with winning conditions of high Borel complexity. In: Díaz, J., et al. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 1150–1162. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  76. Stirling, C.: Modal and Temporal Properties of Processes. Texts in Computer Science. Springer, Heidelberg (2001)

    Google Scholar 

  77. Streett, R.S., Emerson, E.A.: The propositional mu-calculus is elementary. In: Paredaens, J. (ed.) ICALP 1984. LNCS, vol. 172, pp. 465–472. Springer, Heidelberg (1984)

    Google Scholar 

  78. Streett, R.S., Emerson, E.A.: An automata theoretic procedure for the propositional mu-calculus. Information and Computation 81, 249–264 (1989)

    Article  MATH  MathSciNet  Google Scholar 

  79. Thomas, W.: Logic for computer science: The engineering challenge. In: Wilhelm, R. (ed.) Informatics: 10 Years Back, 10 Years Ahead. LNCS, vol. 2000, pp. 257–267. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  80. Urbański, T.: On deciding if deterministic Rabin language is in Büchi class. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 663–674. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  81. Vardi, M.Y., Wolper, P.: Automata theoretic techniques for modal logics of programs. In: Sixteenth ACM Symposium on the Theoretical Computer Science (1984)

    Google Scholar 

  82. Wagner, K.: Eine topologische Charakterisierung einiger Klassen regulärer Folgenmengen. J. Inf. Process. Cybern. EIK 13, 473–487 (1977)

    MATH  Google Scholar 

  83. Walukiewicz, I.: Pushdown processes: Games and model checking. Information and Computation 164(2), 234–263 (2001)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CNRS, LaBRI, Université Bordeaux-1, 351, Cours de la Libération, 33 405, Talence, France

    Igor Walukiewicz

Authors
  1. Igor Walukiewicz
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. National Institute of Advanced Studies, Indian Institute of Science Campus, 560012, Bangalore, India

    Sundar Sarukkai

  2. Department of Comp. Sc. & Engg., Indian Institute of Technology Delhi, 110016, New Delhi, India

    Sandeep Sen

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Walukiewicz, I. (2005). From Logic to Games. In: Sarukkai, S., Sen, S. (eds) FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2005. Lecture Notes in Computer Science, vol 3821. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11590156_5

Download citation

  • DOI: https://doi.org/10.1007/11590156_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-30495-1

  • Online ISBN: 978-3-540-32419-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation