Automata theory and model checking. (English) Zbl 1392.68255
Clarke, Edmund M. (ed.) et al., Handbook of model checking. Cham: Springer (ISBN 978-3-319-10574-1/hbk; 978-3-319-10575-8/ebook). 107-151 (2018).
Summary: 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.
For the entire collection see [Zbl 1390.68001].
For the entire collection see [Zbl 1390.68001].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68Q45 | Formal languages and automata |
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) · Zbl 1326.68181 |
| [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) · Zbl 1043.68563 |
| [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) · Zbl 1288.68148 · doi:10.1007/978-3-642-14162-1_7 |
| [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) · Zbl 1245.68120 |
| [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) · Zbl 1352.68126 |
| [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) · Zbl 0147.25103 |
| [7] | 7. Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. J. Assoc. Comput. Mach. 28(1), 114-133 (1981) · Zbl 0473.68043 · doi:10.1145/322234.322243 |
| [8] | 8. Choueka, Y.: Theories of automata on · Zbl 0292.02033 · doi:10.1016/S0022-0000(74)80051-6 |
| [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) · Zbl 1059.68582 · doi:10.1007/s100090050046 |
| [10] | 10. Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. MIT Press/McGraw-Hill, Cambridge/New York (1990) · Zbl 1158.68538 |
| [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) · Zbl 0954.68102 |
| [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) |
| [13] | 13. Emerson, E.A., Jutla, C.: Tree automata, |
| [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) |
| [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) |
| [16] | 16. Emerson, E.A., Lei, C.-L.: Modalities for model checking: branching time logic strikes back. Sci. Comput. Program. 8, 275-306 (1987) · Zbl 0615.68019 · doi:10.1016/0167-6423(87)90036-0 |
| [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) · Zbl 1247.68136 |
| [18] | 18. Friedgut, E., Kupferman, O., Vardi, M.Y.: Büchi complementation made tighter. Int. J. Found. Comput. Sci. 17(4), 851-868 (2006) · Zbl 1096.68081 · doi:10.1142/S0129054106004145 |
| [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) · Zbl 1279.68152 · doi:10.1007/3-540-45089-0_5 |
| [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) · Zbl 0991.68044 · doi:10.1007/3-540-44585-4_6 |
| [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) |
| [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) · Zbl 1037.68553 |
| [23] | 23. Godefroid, P., Wolper, P.: A partial approach to model checking. Inf. Comput. 110(2), 305-326 (1994) · Zbl 0806.68079 · doi:10.1006/inco.1994.1035 |
| [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) · doi:10.1007/3-540-61474-5_94 |
| [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) |
| [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) · Zbl 1514.68168 |
| [27] | 27. Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279-295 (1997) · doi:10.1109/32.588521 |
| [28] | 28. Immerman, N.: Nondeterministic space is closed under complement. Inf. Comput. 17, 935-938 (1988) · Zbl 0668.68056 |
| [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) · Zbl 0962.68111 |
| [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) · Zbl 1153.68032 · doi:10.1007/978-3-540-70575-8_59 |
| [31] | 31. Katz, S., Peled, D.: Interleaving set temporal logic. Theor. Comput. Sci. 75(3), 263-287 (1990) · Zbl 0718.03014 · doi:10.1016/0304-3975(90)90096-Z |
| [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) · Zbl 0978.68077 · doi:10.1007/3-540-45315-6_18 |
| [33] | 33. Klarlund, N.: Progress measures for complementation of · Zbl 1370.68054 |
| [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) · doi:10.1007/978-3-642-31424-7_7 |
| [35] | 35. Krishnan, S.C., Puri, A., Brayton, R.K.: Deterministic · doi:10.1007/3-540-58325-4_202 |
| [36] | 36. Kupferman, O.: Avoiding determinization. In: Proc. 21st IEEE Symp. on Logic in Computer Science, pp. 243-254 (2006) |
| [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) · Zbl 1151.68485 |
| [38] | 38. Kupferman, O., Morgenstern, G., Murano, A.: Typeness for · Zbl 1098.68073 · doi:10.1142/S0129054106004157 |
| [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) · Zbl 1006.68086 |
| [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) · Zbl 1010.68078 · doi:10.1007/3-540-45657-0_31 |
| [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) |
| [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) · doi:10.1007/3-540-61474-5_84 |
| [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) · Zbl 0974.68083 · doi:10.1007/10722167_7 |
| [44] | 44. Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Trans. Comput. Log. 2(2), 408-429 (2001) · Zbl 1171.68551 · doi:10.1145/377978.377993 |
| [45] | 45. Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Proc. 46th IEEE Symp. on Foundations of Computer Science, pp. 531-540 (2005) |
| [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) · Zbl 1133.68376 · doi:10.1145/333979.333987 |
| [47] | 47. Kurshan, R.P.: Complementing deterministic Büchi automata in polynomial time. J. Comput. Syst. Sci. 35, 59-71 (1987) · Zbl 0666.68058 · doi:10.1016/0022-0000(87)90036-5 |
| [48] | 48. Kurshan, R.P.: Computer Aided Verification of Coordinating Processes. Princeton University Press, Princeton (1994) · Zbl 0822.68116 |
| [49] | 49. Landweber, L.H.: Decision problems for · Zbl 0182.02402 · doi:10.1007/BF01691063 |
| [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) · Zbl 0961.68074 · doi:10.1007/3-540-46691-6_8 |
| [51] | 51. Maler, O., Staiger, L.: On syntactic congruences for · Zbl 0911.68145 · doi:10.1016/S0304-3975(96)00312-X |
| [52] | 52. McNaughton, R.: Testing and generating infinite sequences by a finite automaton. Inf. Control 9, 521-530 (1966) · Zbl 0212.33902 · doi:10.1016/S0019-9958(66)80013-X |
| [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) |
| [54] | 54. Michel, M.: Complementation is More Difficult with Automata on Infinite Words. CNET, Paris (1988) |
| [55] | 55. Miyano, S., Hayashi, T.: Alternating finite automata on · Zbl 0544.68042 · doi:10.1016/0304-3975(84)90049-5 |
| [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) · Zbl 0617.03020 · doi:10.1007/3-540-16761-7_77 |
| [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) · Zbl 0608.03004 · doi:10.1007/3-540-15641-0_27 |
| [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) · Zbl 0873.68135 · doi:10.1016/0304-3975(94)00214-4 |
| [59] | 59. Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. Log. Methods Comput. Sci. 3(3), 5 (2007) · Zbl 1125.68067 · doi:10.2168/LMCS-3(3:5)2007 |
| [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) · Zbl 1143.68046 · doi:10.1007/978-3-540-69850-0_11 |
| [61] | 61. Rabin, M.O.: Decidability of second order theories and automata on infinite trees. Trans. Am. Math. Soc. 141, 1-35 (1969) · Zbl 0221.02031 |
| [62] | 62. Rabin, M.O.: Decidable theories. In: Barwise, J. (ed.) Handbook of Mathematical Logic, pp. 595-629. North-Holland, Amsterdam (1977) · doi:10.1016/S0049-237X(08)71116-9 |
| [63] | 63. Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM J. Res. Dev. 3, 115-125 (1959) · Zbl 0158.25404 · doi:10.1147/rd.32.0114 |
| [64] | 64. Safra, S.: On the complexity of · Zbl 1273.91298 |
| [65] | 65. Safra, S., Vardi, M.Y.: On |
| [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) · Zbl 1236.68176 |
| [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) · Zbl 1234.68239 |
| [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) · Zbl 1245.68096 |
| [69] | 69. Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logic. J. ACM 32, 733-749 (1985) · Zbl 0632.68034 · doi:10.1145/3828.3837 |
| [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) · Zbl 0613.03015 · doi:10.1016/0304-3975(87)90008-9 |
| [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) · Zbl 0974.68086 · doi:10.1007/10722167_21 |
| [72] | 72. Synopsys: Assertion-based verification (2003) |
| [73] | 73. Tarjan, R.E.: Depth first search and linear graph algorithms. SIAM J. Comput. 1(2), 146-160 (1972) · Zbl 0251.05107 · doi:10.1137/0201010 |
| [74] | 74. Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, pp. 133-191 (1990) · Zbl 0900.68316 |
| [75] | 75. Valmari, A.: A stubborn attack on state explosion. Form. Methods Syst. Des. 1, 297-322 (1992) · Zbl 0783.68083 · doi:10.1007/BF00709154 |
| [76] | 76. Vardi, M.Y., Wolper, P.: Automata-theoretic techniques for modal logics of programs. J. Comput. Syst. Sci. 32(2), 182-221 (1986) · Zbl 0622.03017 · doi:10.1016/0022-0000(86)90026-7 |
| [77] | 77. Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1-37 (1994) · Zbl 0827.03009 · doi:10.1006/inco.1994.1092 |
| [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) · doi:10.1109/LICS.1996.561357 |
| [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) |
| [80] | 80. Yan, Q.: Lower bounds for complementation of · Zbl 1134.68031 · doi:10.1007/11787006_50 |
| [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) · Zbl 0915.68120 · doi:10.1016/S0304-3975(98)00009-7 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
