Advertisement

Automata Theory and Model Checking

  • Orna Kupferman
Chapter

Abstract

We study automata on infinite words and their applications in system specification and verification. We first introduce Büchi automata and survey their closure properties, expressive power, and determinization. We then introduce additional acceptance conditions and the model of alternating automata. We compare the different classes of automata in terms of expressive power and succinctness, and describe decision problems for them. Finally, we describe the automata-theoretic approach to system specification and verification.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. In: Proc. 38th IEEE Symp. on Foundations of Computer Science, pp. 100–109 (1997) Google Scholar
  2. 2.
    Armoni, R., Fix, L., Flaisher, A., Gerth, R., Ginsburg, B., Kanza, T., Landver, A., Mador-Haim, S., Singerman, E., Tiemeyer, A., Vardi, M.Y., Zbar, Y.: The ForSpec temporal logic: a new temporal property-specification logic. In: Proc. 8th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 2280, pp. 196–211. Springer, Heidelberg (2002) zbMATHGoogle Scholar
  3. 3.
    Boker, U., Kupferman, O., Rosenberg, A.: Alternation removal in Büchi automata. In: Proc. 37th Int. Colloq. on Automata, Languages, and Programming, vol. 6199, pp. 76–87 (2010) CrossRefGoogle Scholar
  4. 4.
    Boker, U., Kupferman, O., Steinitz, A.: Parityzing Rabin and Streett. In: Proc. 30th Conf. on Foundations of Software Technology and Theoretical Computer Science, pp. 412–423 (2010) zbMATHGoogle Scholar
  5. 5.
    Breuers, S., Löding, C., Olschewski, J.: Improved Ramsey-based Büchi complementation. In: Proc. 15th Int. Conf. on Foundations of Software Science and Computation Structures. LNCS, vol. 7213, pp. 150–164. Springer, Heidelberg (2012) Google Scholar
  6. 6.
    Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. Int. Congress on Logic, Method, and Philosophy of Science. 1960, pp. 1–12. Stanford University Press, Stanford (1962) Google Scholar
  7. 7.
    Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. J. Assoc. Comput. Mach. 28(1), 114–133 (1981) MathSciNetCrossRefGoogle Scholar
  8. 8.
    Choueka, Y.: Theories of automata on \(\omega\)-tapes: a simplified approach. J. Comput. Syst. Sci. 8, 117–141 (1974) MathSciNetCrossRefGoogle Scholar
  9. 9.
    Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model checker. Int. J. Softw. Tools Technol. Transf. 2(4), 410–425 (2000) CrossRefGoogle Scholar
  10. 10.
    Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. MIT Press/McGraw-Hill, Cambridge/New York (1990) zbMATHGoogle Scholar
  11. 11.
    Couvreur, J.-M.: On-the-fly verification of linear temporal logic. In: World Congress on Formal Methods. LNCS, vol. 1708, pp. 253–271. Springer, Heidelberg (1999) zbMATHGoogle Scholar
  12. 12.
    Emerson, E.A., Jutla, C.: The complexity of tree automata and logics of programs. In: Proc. 29th IEEE Symp. on Foundations of Computer Science, pp. 328–337 (1988) Google Scholar
  13. 13.
    Emerson, E.A., Jutla, C.: Tree automata, \(\mu\)-calculus and determinacy. In: Proc. 32nd IEEE Symp. on Foundations of Computer Science, pp. 368–377 (1991) Google Scholar
  14. 14.
    Emerson, E.A., Lei, C.-L.: Modalities for model checking: branching time logic strikes back. In: Proc. 12th ACM Symp. on Principles of Programming Languages, pp. 84–96 (1985) Google Scholar
  15. 15.
    Emerson, E.A., Lei, C.-L.: Temporal model checking under generalized fairness constraints. In: Proc. 18th Hawaii Int. Conf. on System Sciences. Western Periodicals Company, North Hollywood (1985) Google Scholar
  16. 16.
    Emerson, E.A., Lei, C.-L.: Modalities for model checking: branching time logic strikes back. Sci. Comput. Program. 8, 275–306 (1987) MathSciNetCrossRefGoogle Scholar
  17. 17.
    Fogarty, S., Kupferman, O., Vardi, M.Y., Wilke, T.: Unifying Büchi complementation constructions. In: Proc. 20th Annual Conf. of the European Association for Computer Science Logic, pp. 248–263 (2011) Google Scholar
  18. 18.
    Friedgut, E., Kupferman, O., Vardi, M.Y.: Büchi complementation made tighter. Int. J. Found. Comput. Sci. 17(4), 851–868 (2006) CrossRefGoogle Scholar
  19. 19.
    Fritz, C.: Constructing Büchi automata from linear temporal logic using simulation relations for alternating Büchi automata. In: Proc. 8th Int. Conf. on Implementation and Application of Automata. LNCS, vol. 2759, pp. 35–48. Springer, Heidelberg (2003) CrossRefGoogle Scholar
  20. 20.
    Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Proc. 13th Int. Conf. on Computer Aided Verification. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001) CrossRefGoogle Scholar
  21. 21.
    Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Dembiski, P., Sredniawa, M. (eds.) Protocol Specification, Testing, and Verification, pp. 3–18. Chapman & Hall, London (1995) Google Scholar
  22. 22.
    Giannakopoulou, D., Lerda, F.: From states to transitions: improving translation of LTL formulae to Büchi automata. In: Proc. 22nd International Conference on Formal Techniques for Networked and Distributed Systems. LNCS, vol. 2529, pp. 308–326. Springer, Heidelberg (2002) Google Scholar
  23. 23.
    Godefroid, P., Wolper, P.: A partial approach to model checking. Inf. Comput. 110(2), 305–326 (1994) MathSciNetCrossRefGoogle Scholar
  24. 24.
    Hardin, R.H., Har’el, Z., Kurshan, R.P.: COSPAN. In: Proc. 8th Int. Conf. on Computer Aided Verification. LNCS, vol. 1102, pp. 423–427. Springer, Heidelberg (1996) CrossRefGoogle Scholar
  25. 25.
    Henzinger, M., Telle, J.A.: Faster algorithms for the nonemptiness of Streett automata and for communication protocol pruning. In: Proc. 5th Scandinavian Workshop on Algorithm Theory. LNCS, vol. 1097, pp. 10–20. Springer, Heidelberg (1996) Google Scholar
  26. 26.
    Henzinger, T.A., Kupferman, O., Vardi, M.Y.: A space-efficient on-the-fly algorithm for real-time model checking. In: Proc. 7th Int. Conf. on Concurrency Theory. LNCS, vol. 1119, pp. 514–529. Springer, Heidelberg (1996) Google Scholar
  27. 27.
    Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997) CrossRefGoogle Scholar
  28. 28.
    Immerman, N.: Nondeterministic space is closed under complement. Inf. Comput. 17, 935–938 (1988) zbMATHGoogle Scholar
  29. 29.
    Jurdzinski, M.: Small progress measures for solving parity games. In: Proc. 17th Symp. on Theoretical Aspects of Computer Science. LNCS, vol. 1770, pp. 290–301. Springer, Heidelberg (2000) Google Scholar
  30. 30.
    Kähler, D., Wilke, T.: Complementation, disambiguation, and determinization of Büchi automata unified. In: Proc. 35th Int. Colloq. on Automata, Languages, and Programming. LNCS, vol. 5126, pp. 724–735. Springer, Heidelberg (2008) CrossRefGoogle Scholar
  31. 31.
    Katz, S., Peled, D.: Interleaving set temporal logic. Theor. Comput. Sci. 75(3), 263–287 (1990) MathSciNetCrossRefGoogle Scholar
  32. 32.
    King, V., Kupferman, O., Vardi, M.Y.: On the complexity of parity word automata. In: Proc. 4th Int. Conf. on Foundations of Software Science and Computation Structures. LNCS, vol. 2030, pp. 276–286. Springer, Heidelberg (2001) CrossRefGoogle Scholar
  33. 33.
    Klarlund, N.: Progress measures for complementation of \(\omega\)-automata with applications to temporal logic. In: Proc. 32nd IEEE Symp. on Foundations of Computer Science, pp. 358–367 (1991) Google Scholar
  34. 34.
    Kretínský, J., Esparza, J.: Deterministic automata for the (F, G)-fragment of LTL. In: Proc. 24th Int. Conf. on Computer Aided Verification. LNCS, vol. 7358, pp. 7–22. Springer, Heidelberg (2012) CrossRefGoogle Scholar
  35. 35.
    Krishnan, S.C., Puri, A., Brayton, R.K.: Deterministic \(\omega\)-automata vis-a-vis deterministic Büchi automata. In: Algorithms and Computations. LNCS, vol. 834, pp. 378–386. Springer, Heidelberg (1994) CrossRefGoogle Scholar
  36. 36.
    Kupferman, O.: Avoiding determinization. In: Proc. 21st IEEE Symp. on Logic in Computer Science, pp. 243–254 (2006) Google Scholar
  37. 37.
    Kupferman, O.: Sanity checks in formal verification. In: Proc. 17th Int. Conf. on Concurrency Theory. LNCS, vol. 4137, pp. 37–51. Springer, Heidelberg (2006) Google Scholar
  38. 38.
    Kupferman, O., Morgenstern, G., Murano, A.: Typeness for \(\omega\)-regular automata. Int. J. Found. Comput. Sci. 17(4), 869–884 (2006) MathSciNetCrossRefGoogle Scholar
  39. 39.
    Kupferman, O., Piterman, N., Vardi, M.Y.: Extended temporal logic revisited. In: Proc. 12th Int. Conf. on Concurrency Theory. LNCS, vol. 2154, pp. 519–535 (2001) Google Scholar
  40. 40.
    Kupferman, O., Piterman, N., Vardi, M.Y.: Model checking linear properties of prefix-recognizable systems. In: Proc. 14th Int. Conf. on Computer Aided Verification. LNCS, vol. 2404, pp. 371–385. Springer, Heidelberg (2002) CrossRefGoogle Scholar
  41. 41.
    Kupferman, O., Vardi, M.Y.: On the complexity of branching modular model checking. In: Proc. 6th Int. Conf. on Concurrency Theory. LNCS, vol. 962, pp. 408–422. Springer, Heidelberg (1995) Google Scholar
  42. 42.
    Kupferman, O., Vardi, M.Y.: Verification of fair transition systems. In: Proc. 8th Int. Conf. on Computer Aided Verification. LNCS, vol. 1102, pp. 372–382. Springer, Heidelberg (1996) CrossRefGoogle Scholar
  43. 43.
    Kupferman, O., Vardi, M.Y.: An automata-theoretic approach to reasoning about infinite-state systems. In: Proc. 12th Int. Conf. on Computer Aided Verification. LNCS, vol. 1855, pp. 36–52. Springer, Heidelberg (2000) CrossRefGoogle Scholar
  44. 44.
    Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Trans. Comput. Log. 2(2), 408–429 (2001) MathSciNetCrossRefGoogle Scholar
  45. 45.
    Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Proc. 46th IEEE Symp. on Foundations of Computer Science, pp. 531–540 (2005) Google Scholar
  46. 46.
    Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM 47(2), 312–360 (2000) MathSciNetCrossRefGoogle Scholar
  47. 47.
    Kurshan, R.P.: Complementing deterministic Büchi automata in polynomial time. J. Comput. Syst. Sci. 35, 59–71 (1987) CrossRefGoogle Scholar
  48. 48.
    Kurshan, R.P.: Computer Aided Verification of Coordinating Processes. Princeton University Press, Princeton (1994) zbMATHGoogle Scholar
  49. 49.
    Landweber, L.H.: Decision problems for \(\omega\)-automata. Math. Syst. Theory 3, 376–384 (1969) MathSciNetCrossRefGoogle Scholar
  50. 50.
    Löding, C.: Optimal bounds for the transformation of omega-automata. In: Proc. 19th Conf. on Foundations of Software Technology and Theoretical Computer Science. LNCS, vol. 1738, pp. 97–109 (1999) CrossRefGoogle Scholar
  51. 51.
    Maler, O., Staiger, L.: On syntactic congruences for \(\omega\)-languages. Theor. Comput. Sci. 183(1), 93–112 (1997) MathSciNetCrossRefGoogle Scholar
  52. 52.
    McNaughton, R.: Testing and generating infinite sequences by a finite automaton. Inf. Control 9, 521–530 (1966) MathSciNetCrossRefGoogle Scholar
  53. 53.
    Meyer, A.R., Stockmeyer, L.J.: The equivalence problem for regular expressions with squaring requires exponential time. In: Proc. 13th IEEE Symp. on Switching and Automata Theory, pp. 125–129 (1972) Google Scholar
  54. 54.
    Michel, M.: Complementation is More Difficult with Automata on Infinite Words. CNET, Paris (1988) Google Scholar
  55. 55.
    Miyano, S., Hayashi, T.: Alternating finite automata on \(\omega\)-words. Theor. Comput. Sci. 32, 321–330 (1984) MathSciNetCrossRefGoogle Scholar
  56. 56.
    Muller, D.E., Saoudi, A., Schupp, P.E.: Alternating automata, the weak monadic theory of the tree and its complexity. In: Proc. 13th Int. Colloq. on Automata, Languages, and Programming. LNCS, vol. 226, pp. 275–283. Springer, Heidelberg (1986) CrossRefGoogle Scholar
  57. 57.
    Muller, D.E., Schupp, P.E.: Alternating automata on infinite trees. In: Automata on Infinite Words. LNCS, vol. 192, pp. 100–107. Springer, Heidelberg (1985) CrossRefGoogle Scholar
  58. 58.
    Muller, D.E., Schupp, P.E.: Simulating alternating tree automata by nondeterministic automata: new results and new proofs of theorems of Rabin, McNaughton and Safra. Theor. Comput. Sci. 141, 69–107 (1995) MathSciNetCrossRefGoogle Scholar
  59. 59.
    Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. Log. Methods Comput. Sci. 3(3), 5 (2007) CrossRefGoogle Scholar
  60. 60.
    Pnueli, A., Zaks, A.: On the merits of temporal testers. In: 25 Years of Model Checking. LNCS, vol. 5000, pp. 172–195. Springer, Heidelberg (2008) CrossRefGoogle Scholar
  61. 61.
    Rabin, M.O.: Decidability of second order theories and automata on infinite trees. Trans. Am. Math. Soc. 141, 1–35 (1969) MathSciNetzbMATHGoogle Scholar
  62. 62.
    Rabin, M.O.: Decidable theories. In: Barwise, J. (ed.) Handbook of Mathematical Logic, pp. 595–629. North-Holland, Amsterdam (1977) CrossRefGoogle Scholar
  63. 63.
    Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM J. Res. Dev. 3, 115–125 (1959) MathSciNetCrossRefGoogle Scholar
  64. 64.
    Safra, S.: On the complexity of \(\omega\)-automata. In: Proc. 29th IEEE Symp. on Foundations of Computer Science, pp. 319–327 (1988) Google Scholar
  65. 65.
    Safra, S., Vardi, M.Y.: On \(\omega\)-automata and temporal logic. In: Proc. 21st ACM Symp. on Theory of Computing, pp. 127–137 (1989) Google Scholar
  66. 66.
    Schewe, S.: Büchi complementation made tight. In: Proc. 26th Symp. on Theoretical Aspects of Computer Science. LIPIcs, vol. 3, pp. 661–672. Schloss Dagstuhl—Leibniz-Zentrum fuer Informatik, Wadern (2009) Google Scholar
  67. 67.
    Schewe, S.: Tighter bounds for the determinisation of Büchi automata. In: Proc. 12th Int. Conf. on Foundations of Software Science and Computation Structures. LNCS, vol. 5504, pp. 167–181. Springer, Heidelberg (2009) Google Scholar
  68. 68.
    Schewe, S.: Beyond hyper-minimisation—minimising DBAs and DPAs is NP-complete. In: Proc. 30th Conf. on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), vol. 8, pp. 400–411 (2010) Google Scholar
  69. 69.
    Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logic. J. ACM 32, 733–749 (1985) MathSciNetCrossRefGoogle Scholar
  70. 70.
    Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for Büchi automata with applications to temporal logic. Theor. Comput. Sci. 49, 217–237 (1987) CrossRefGoogle Scholar
  71. 71.
    Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae. In: Proc. 12th Int. Conf. on Computer Aided Verification. LNCS, vol. 1855, pp. 248–263. Springer, Heidelberg (2000) CrossRefGoogle Scholar
  72. 72.
    Synopsys: Assertion-based verification (2003) Google Scholar
  73. 73.
    Tarjan, R.E.: Depth first search and linear graph algorithms. SIAM J. Comput. 1(2), 146–160 (1972) MathSciNetCrossRefGoogle Scholar
  74. 74.
    Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, pp. 133–191 (1990) Google Scholar
  75. 75.
    Valmari, A.: A stubborn attack on state explosion. Form. Methods Syst. Des. 1, 297–322 (1992) CrossRefGoogle Scholar
  76. 76.
    Vardi, M.Y., Wolper, P.: Automata-theoretic techniques for modal logics of programs. J. Comput. Syst. Sci. 32(2), 182–221 (1986) MathSciNetCrossRefGoogle Scholar
  77. 77.
    Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1–37 (1994) MathSciNetCrossRefGoogle Scholar
  78. 78.
    Willems, B., Wolper, P.: Partial-order methods for model checking: from linear time to branching time. In: Proc. 11th IEEE Symp. on Logic in Computer Science, pp. 294–303 (1996) CrossRefGoogle Scholar
  79. 79.
    Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths. In: Proc. 24th IEEE Symp. on Foundations of Computer Science, pp. 185–194 (1983) Google Scholar
  80. 80.
    Yan, Q.: Lower bounds for complementation of \(\omega\)-automata via the full automata technique. In: Proc. 33rd Int. Colloq. on Automata, Languages, and Programming. LNCS, vol. 4052, pp. 589–600. Springer, Heidelberg (2006) CrossRefGoogle Scholar
  81. 81.
    Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci. 200(1–2), 135–183 (1998) MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Hebrew UniversityJerusalemIsrael

Personalised recommendations