{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:08:38Z","timestamp":1770278918984,"version":"3.49.0"},"publisher-location":"Cham","reference-count":81,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319105741","type":"print"},{"value":"9783319105758","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-10575-8_4","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T08:05:28Z","timestamp":1526630728000},"page":"107-151","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":25,"title":["Automata Theory and Model Checking"],"prefix":"10.1007","author":[{"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"key":"4_CR1","first-page":"100","volume-title":"Proc. 38th IEEE Symp. on Foundations of Computer Science","author":"R. Alur","year":"1997","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. In: Proc. 38th IEEE Symp. on Foundations of Computer Science, pp.\u00a0100\u2013109 (1997)"},{"key":"4_CR2","series-title":"LNCS","first-page":"196","volume-title":"Proc. 8th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Armoni","year":"2002","unstructured":"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\u00a0new temporal property-specification logic. In: Proc. 8th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol.\u00a02280, pp.\u00a0196\u2013211. Springer, Heidelberg (2002)"},{"key":"4_CR3","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-642-14162-1_7","volume-title":"Proc. 37th Int. Colloq. on Automata, Languages, and Programming","author":"U. Boker","year":"2010","unstructured":"Boker, U., Kupferman, O., Rosenberg, A.: Alternation removal in B\u00fcchi automata. In: Proc. 37th Int. Colloq. on Automata, Languages, and Programming, vol.\u00a06199, pp.\u00a076\u201387 (2010)"},{"key":"4_CR4","first-page":"412","volume-title":"Proc. 30th Conf. on Foundations of Software Technology and Theoretical Computer Science","author":"U. Boker","year":"2010","unstructured":"Boker, U., Kupferman, O., Steinitz, A.: Parityzing Rabin and Streett. In: Proc. 30th Conf. on Foundations of Software Technology and Theoretical Computer Science, pp.\u00a0412\u2013423 (2010)"},{"key":"4_CR5","series-title":"LNCS","first-page":"150","volume-title":"Proc. 15th Int. Conf. on Foundations of Software Science and Computation Structures","author":"S. Breuers","year":"2012","unstructured":"Breuers, S., L\u00f6ding, C., Olschewski, J.: Improved Ramsey-based B\u00fcchi complementation. In: Proc. 15th Int. Conf. on Foundations of Software Science and Computation Structures. LNCS, vol.\u00a07213, pp.\u00a0150\u2013164. Springer, Heidelberg (2012)"},{"key":"4_CR6","first-page":"1","volume-title":"Proc. Int. Congress on Logic, Method, and Philosophy of Science. 1960","author":"J.R. B\u00fcchi","year":"1962","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. Int. Congress on Logic, Method, and Philosophy of Science. 1960, pp.\u00a01\u201312. Stanford University Press, Stanford (1962)"},{"issue":"1","key":"4_CR7","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"A.K. Chandra","year":"1981","unstructured":"Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. J. Assoc. Comput. Mach. 28(1), 114\u2013133 (1981)","journal-title":"J. Assoc. Comput. Mach."},{"key":"4_CR8","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0022-0000(74)80051-6","volume":"8","author":"Y. Choueka","year":"1974","unstructured":"Choueka, Y.: Theories of automata on \u03c9$\\omega$-tapes: a simplified approach. J. Comput. Syst. Sci. 8, 117\u2013141 (1974)","journal-title":"J. Comput. Syst. Sci."},{"issue":"4","key":"4_CR9","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A. Cimatti","year":"2000","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model checker. Int. J. Softw. Tools Technol. Transf. 2(4), 410\u2013425 (2000)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"4_CR10","volume-title":"Introduction to Algorithms","author":"T.H. Cormen","year":"1990","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. MIT Press\/McGraw-Hill, Cambridge\/New York (1990)"},{"key":"4_CR11","series-title":"LNCS","first-page":"253","volume-title":"World Congress on Formal Methods","author":"J.-M. Couvreur","year":"1999","unstructured":"Couvreur, J.-M.: On-the-fly verification of linear temporal logic. In: World Congress on Formal Methods. LNCS, vol.\u00a01708, pp.\u00a0253\u2013271. Springer, Heidelberg (1999)"},{"key":"4_CR12","first-page":"328","volume-title":"Proc. 29th IEEE Symp. on Foundations of Computer Science","author":"E.A. Emerson","year":"1988","unstructured":"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.\u00a0328\u2013337 (1988)"},{"key":"4_CR13","first-page":"368","volume-title":"Proc. 32nd IEEE Symp. on Foundations of Computer Science","author":"E.A. Emerson","year":"1991","unstructured":"Emerson, E.A., Jutla, C.: Tree automata, \u03bc$\\mu$-calculus and determinacy. In: Proc. 32nd IEEE Symp. on Foundations of Computer Science, pp.\u00a0368\u2013377 (1991)"},{"key":"4_CR14","first-page":"84","volume-title":"Proc. 12th ACM Symp. on Principles of Programming Languages","author":"E.A. Emerson","year":"1985","unstructured":"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.\u00a084\u201396 (1985)"},{"key":"4_CR15","volume-title":"Proc. 18th Hawaii Int. Conf. on System Sciences","author":"E.A. Emerson","year":"1985","unstructured":"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)"},{"key":"4_CR16","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"E.A. Emerson","year":"1987","unstructured":"Emerson, E.A., Lei, C.-L.: Modalities for model checking: branching time logic strikes back. Sci. Comput. Program. 8, 275\u2013306 (1987)","journal-title":"Sci. Comput. Program."},{"key":"4_CR17","first-page":"248","volume-title":"Proc. 20th Annual Conf. of the European Association for Computer Science Logic","author":"S. Fogarty","year":"2011","unstructured":"Fogarty, S., Kupferman, O., Vardi, M.Y., Wilke, T.: Unifying B\u00fcchi complementation constructions. In: Proc. 20th Annual Conf. of the European Association for Computer Science Logic, pp.\u00a0248\u2013263 (2011)"},{"issue":"4","key":"4_CR18","doi-asserted-by":"publisher","first-page":"851","DOI":"10.1142\/S0129054106004145","volume":"17","author":"E. Friedgut","year":"2006","unstructured":"Friedgut, E., Kupferman, O., Vardi, M.Y.: B\u00fcchi complementation made tighter. Int. J. Found. Comput. Sci. 17(4), 851\u2013868 (2006)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"4_CR19","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/3-540-45089-0_5","volume-title":"Proc. 8th Int. Conf. on Implementation and Application of Automata","author":"C. Fritz","year":"2003","unstructured":"Fritz, C.: Constructing B\u00fcchi automata from linear temporal logic using simulation relations for alternating B\u00fcchi automata. In: Proc. 8th Int. Conf. on Implementation and Application of Automata. LNCS, vol.\u00a02759, pp.\u00a035\u201348. Springer, Heidelberg (2003)"},{"key":"4_CR20","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Proc. 13th Int. Conf. on Computer Aided Verification","author":"P. Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. In: Proc. 13th Int. Conf. on Computer Aided Verification. LNCS, vol.\u00a02102, pp.\u00a053\u201365. Springer, Heidelberg (2001)"},{"key":"4_CR21","first-page":"3","volume-title":"Protocol Specification, Testing, and Verification","author":"R. Gerth","year":"1995","unstructured":"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.\u00a03\u201318. Chapman & Hall, London (1995)"},{"key":"4_CR22","series-title":"LNCS","first-page":"308","volume-title":"Proc. 22nd International Conference on Formal Techniques for Networked and Distributed Systems","author":"D. Giannakopoulou","year":"2002","unstructured":"Giannakopoulou, D., Lerda, F.: From states to transitions: improving translation of LTL formulae to B\u00fcchi automata. In: Proc. 22nd International Conference on Formal Techniques for Networked and Distributed Systems. LNCS, vol.\u00a02529, pp.\u00a0308\u2013326. Springer, Heidelberg (2002)"},{"issue":"2","key":"4_CR23","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1006\/inco.1994.1035","volume":"110","author":"P. Godefroid","year":"1994","unstructured":"Godefroid, P., Wolper, P.: A partial approach to model checking. Inf. Comput. 110(2), 305\u2013326 (1994)","journal-title":"Inf. Comput."},{"key":"4_CR24","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/3-540-61474-5_94","volume-title":"Proc. 8th Int. Conf. on Computer Aided Verification","author":"R.H. Hardin","year":"1996","unstructured":"Hardin, R.H., Har\u2019el, Z., Kurshan, R.P.: COSPAN. In: Proc. 8th Int. Conf. on Computer Aided Verification. LNCS, vol.\u00a01102, pp.\u00a0423\u2013427. Springer, Heidelberg (1996)"},{"key":"4_CR25","series-title":"LNCS","first-page":"10","volume-title":"Proc. 5th Scandinavian Workshop on Algorithm Theory","author":"M. Henzinger","year":"1996","unstructured":"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.\u00a01097, pp.\u00a010\u201320. Springer, Heidelberg (1996)"},{"key":"4_CR26","series-title":"LNCS","first-page":"514","volume-title":"Proc. 7th Int. Conf. on Concurrency Theory","author":"T.A. Henzinger","year":"1996","unstructured":"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.\u00a01119, pp.\u00a0514\u2013529. Springer, Heidelberg (1996)"},{"issue":"5","key":"4_CR27","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"4_CR28","first-page":"935","volume":"17","author":"N. Immerman","year":"1988","unstructured":"Immerman, N.: Nondeterministic space is closed under complement. Inf. Comput. 17, 935\u2013938 (1988)","journal-title":"Inf. Comput."},{"key":"4_CR29","series-title":"LNCS","first-page":"290","volume-title":"Proc. 17th Symp. on Theoretical Aspects of Computer Science","author":"M. Jurdzinski","year":"2000","unstructured":"Jurdzinski, M.: Small progress measures for solving parity games. In: Proc. 17th Symp. on Theoretical Aspects of Computer Science. LNCS, vol.\u00a01770, pp.\u00a0290\u2013301. Springer, Heidelberg (2000)"},{"key":"4_CR30","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"724","DOI":"10.1007\/978-3-540-70575-8_59","volume-title":"Proc. 35th Int. Colloq. on Automata, Languages, and Programming","author":"D. K\u00e4hler","year":"2008","unstructured":"K\u00e4hler, D., Wilke, T.: Complementation, disambiguation, and determinization of B\u00fcchi automata unified. In: Proc. 35th Int. Colloq. on Automata, Languages, and Programming. LNCS, vol.\u00a05126, pp.\u00a0724\u2013735. Springer, Heidelberg (2008)"},{"issue":"3","key":"4_CR31","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1016\/0304-3975(90)90096-Z","volume":"75","author":"S. Katz","year":"1990","unstructured":"Katz, S., Peled, D.: Interleaving set temporal logic. Theor. Comput. Sci. 75(3), 263\u2013287 (1990)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR32","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/3-540-45315-6_18","volume-title":"Proc. 4th Int. Conf. on Foundations of Software Science and Computation Structures","author":"V. King","year":"2001","unstructured":"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.\u00a02030, pp.\u00a0276\u2013286. Springer, Heidelberg (2001)"},{"key":"4_CR33","first-page":"358","volume-title":"Proc. 32nd IEEE Symp. on Foundations of Computer Science","author":"N. Klarlund","year":"1991","unstructured":"Klarlund, N.: Progress measures for complementation of \u03c9$\\omega$-automata with applications to temporal logic. In: Proc. 32nd IEEE Symp. on Foundations of Computer Science, pp.\u00a0358\u2013367 (1991)"},{"key":"4_CR34","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/978-3-642-31424-7_7","volume-title":"Proc. 24th Int. Conf. on Computer Aided Verification","author":"J. Kret\u00ednsk\u00fd","year":"2012","unstructured":"Kret\u00ednsk\u00fd, J., Esparza, J.: Deterministic automata for the (F, G)-fragment of LTL. In: Proc. 24th Int. Conf. on Computer Aided Verification. LNCS, vol.\u00a07358, pp.\u00a07\u201322. Springer, Heidelberg (2012)"},{"key":"4_CR35","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/3-540-58325-4_202","volume-title":"Algorithms and Computations","author":"S.C. Krishnan","year":"1994","unstructured":"Krishnan, S.C., Puri, A., Brayton, R.K.: Deterministic \u03c9$\\omega$-automata vis-a-vis deterministic B\u00fcchi automata. In: Algorithms and Computations. LNCS, vol.\u00a0834, pp.\u00a0378\u2013386. Springer, Heidelberg (1994)"},{"key":"4_CR36","first-page":"243","volume-title":"Proc. 21st IEEE Symp. on Logic in Computer Science","author":"O. Kupferman","year":"2006","unstructured":"Kupferman, O.: Avoiding determinization. In: Proc. 21st IEEE Symp. on Logic in Computer Science, pp.\u00a0243\u2013254 (2006)"},{"key":"4_CR37","series-title":"LNCS","first-page":"37","volume-title":"Proc. 17th Int. Conf. on Concurrency Theory","author":"O. Kupferman","year":"2006","unstructured":"Kupferman, O.: Sanity checks in formal verification. In: Proc. 17th Int. Conf. on Concurrency Theory. LNCS, vol.\u00a04137, pp.\u00a037\u201351. Springer, Heidelberg (2006)"},{"issue":"4","key":"4_CR38","doi-asserted-by":"publisher","first-page":"869","DOI":"10.1142\/S0129054106004157","volume":"17","author":"O. Kupferman","year":"2006","unstructured":"Kupferman, O., Morgenstern, G., Murano, A.: Typeness for \u03c9$\\omega$-regular automata. Int. J. Found. Comput. Sci. 17(4), 869\u2013884 (2006)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"4_CR39","series-title":"LNCS","first-page":"519","volume-title":"Proc. 12th Int. Conf. on Concurrency Theory","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: Extended temporal logic revisited. In: Proc. 12th Int. Conf. on Concurrency Theory. LNCS, vol.\u00a02154, pp.\u00a0519\u2013535 (2001)"},{"key":"4_CR40","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/3-540-45657-0_31","volume-title":"Proc. 14th Int. Conf. on Computer Aided Verification","author":"O. Kupferman","year":"2002","unstructured":"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.\u00a02404, pp.\u00a0371\u2013385. Springer, Heidelberg (2002)"},{"key":"4_CR41","series-title":"LNCS","first-page":"408","volume-title":"Proc. 6th Int. Conf. on Concurrency Theory","author":"O. Kupferman","year":"1995","unstructured":"Kupferman, O., Vardi, M.Y.: On the complexity of branching modular model checking. In: Proc. 6th Int. Conf. on Concurrency Theory. LNCS, vol.\u00a0962, pp.\u00a0408\u2013422. Springer, Heidelberg (1995)"},{"key":"4_CR42","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/3-540-61474-5_84","volume-title":"Proc. 8th Int. Conf. on Computer Aided Verification","author":"O. Kupferman","year":"1996","unstructured":"Kupferman, O., Vardi, M.Y.: Verification of fair transition systems. In: Proc. 8th Int. Conf. on Computer Aided Verification. LNCS, vol.\u00a01102, pp.\u00a0372\u2013382. Springer, Heidelberg (1996)"},{"key":"4_CR43","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/10722167_7","volume-title":"Proc. 12th Int. Conf. on Computer Aided Verification","author":"O. Kupferman","year":"2000","unstructured":"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.\u00a01855, pp.\u00a036\u201352. Springer, Heidelberg (2000)"},{"issue":"2","key":"4_CR44","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1145\/377978.377993","volume":"2","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Trans. Comput. Log. 2(2), 408\u2013429 (2001)","journal-title":"ACM Trans. Comput. Log."},{"key":"4_CR45","first-page":"531","volume-title":"Proc. 46th IEEE Symp. on Foundations of Computer Science","author":"O. Kupferman","year":"2005","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Proc. 46th IEEE Symp. on Foundations of Computer Science, pp.\u00a0531\u2013540 (2005)"},{"issue":"2","key":"4_CR46","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O. Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM 47(2), 312\u2013360 (2000)","journal-title":"J. ACM"},{"key":"4_CR47","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/0022-0000(87)90036-5","volume":"35","author":"R.P. Kurshan","year":"1987","unstructured":"Kurshan, R.P.: Complementing deterministic B\u00fcchi automata in polynomial time. J. Comput. Syst. Sci. 35, 59\u201371 (1987)","journal-title":"J. Comput. Syst. Sci."},{"key":"4_CR48","volume-title":"Computer Aided Verification of Coordinating Processes","author":"R.P. Kurshan","year":"1994","unstructured":"Kurshan, R.P.: Computer Aided Verification of Coordinating Processes. Princeton University Press, Princeton (1994)"},{"key":"4_CR49","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/BF01691063","volume":"3","author":"L.H. Landweber","year":"1969","unstructured":"Landweber, L.H.: Decision problems for \u03c9$\\omega$-automata. Math. Syst. Theory 3, 376\u2013384 (1969)","journal-title":"Math. Syst. Theory"},{"key":"4_CR50","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/3-540-46691-6_8","volume-title":"Proc. 19th Conf. on Foundations of Software Technology and Theoretical Computer Science","author":"C. L\u00f6ding","year":"1999","unstructured":"L\u00f6ding, C.: Optimal bounds for the transformation of omega-automata. In: Proc. 19th Conf. on Foundations of Software Technology and Theoretical Computer Science. LNCS, vol.\u00a01738, pp.\u00a097\u2013109 (1999)"},{"issue":"1","key":"4_CR51","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/S0304-3975(96)00312-X","volume":"183","author":"O. Maler","year":"1997","unstructured":"Maler, O., Staiger, L.: On syntactic congruences for \u03c9$\\omega$-languages. Theor. Comput. Sci. 183(1), 93\u2013112 (1997)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR52","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1016\/S0019-9958(66)80013-X","volume":"9","author":"R. McNaughton","year":"1966","unstructured":"McNaughton, R.: Testing and generating infinite sequences by a finite automaton. Inf. Control 9, 521\u2013530 (1966)","journal-title":"Inf. Control"},{"key":"4_CR53","first-page":"125","volume-title":"Proc. 13th IEEE Symp. on Switching and Automata Theory","author":"A.R. Meyer","year":"1972","unstructured":"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.\u00a0125\u2013129 (1972)"},{"key":"4_CR54","volume-title":"Complementation is More Difficult with Automata on Infinite Words","author":"M. Michel","year":"1988","unstructured":"Michel, M.: Complementation is More Difficult with Automata on Infinite Words. CNET, Paris (1988)"},{"key":"4_CR55","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0304-3975(84)90049-5","volume":"32","author":"S. Miyano","year":"1984","unstructured":"Miyano, S., Hayashi, T.: Alternating finite automata on \u03c9$\\omega$-words. Theor. Comput. Sci. 32, 321\u2013330 (1984)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR56","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/3-540-16761-7_77","volume-title":"Proc. 13th Int. Colloq. on Automata, Languages, and Programming","author":"D.E. Muller","year":"1986","unstructured":"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.\u00a0226, pp.\u00a0275\u2013283. Springer, Heidelberg (1986)"},{"key":"4_CR57","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/3-540-15641-0_27","volume-title":"Automata on Infinite Words","author":"D.E. Muller","year":"1985","unstructured":"Muller, D.E., Schupp, P.E.: Alternating automata on infinite trees. In: Automata on Infinite Words. LNCS, vol.\u00a0192, pp.\u00a0100\u2013107. Springer, Heidelberg (1985)"},{"key":"4_CR58","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/0304-3975(94)00214-4","volume":"141","author":"D.E. Muller","year":"1995","unstructured":"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\u2013107 (1995)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"4_CR59","doi-asserted-by":"publisher","first-page":"5","DOI":"10.2168\/LMCS-3(3:5)2007","volume":"3","author":"N. Piterman","year":"2007","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. Log. Methods Comput. Sci. 3(3), 5 (2007)","journal-title":"Log. Methods Comput. Sci."},{"key":"4_CR60","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-540-69850-0_11","volume-title":"25 Years of Model Checking","author":"A. Pnueli","year":"2008","unstructured":"Pnueli, A., Zaks, A.: On the merits of temporal testers. In: 25 Years of Model Checking. LNCS, vol.\u00a05000, pp.\u00a0172\u2013195. Springer, Heidelberg (2008)"},{"key":"4_CR61","first-page":"1","volume":"141","author":"M.O. Rabin","year":"1969","unstructured":"Rabin, M.O.: Decidability of second order theories and automata on infinite trees. Trans. Am. Math. Soc. 141, 1\u201335 (1969)","journal-title":"Trans. Am. Math. Soc."},{"key":"4_CR62","doi-asserted-by":"publisher","first-page":"595","DOI":"10.1016\/S0049-237X(08)71116-9","volume-title":"Handbook of Mathematical Logic","author":"M.O. Rabin","year":"1977","unstructured":"Rabin, M.O.: Decidable theories. In: Barwise, J. (ed.) Handbook of Mathematical Logic, pp.\u00a0595\u2013629. North-Holland, Amsterdam (1977)"},{"key":"4_CR63","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1147\/rd.32.0114","volume":"3","author":"M.O. Rabin","year":"1959","unstructured":"Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM J. Res. Dev. 3, 115\u2013125 (1959)","journal-title":"IBM J. Res. Dev."},{"key":"4_CR64","first-page":"319","volume-title":"Proc. 29th IEEE Symp. on Foundations of Computer Science","author":"S. Safra","year":"1988","unstructured":"Safra, S.: On the complexity of \u03c9$\\omega$-automata. In: Proc. 29th IEEE Symp. on Foundations of Computer Science, pp.\u00a0319\u2013327 (1988)"},{"key":"4_CR65","first-page":"127","volume-title":"Proc. 21st ACM Symp. on Theory of Computing","author":"S. Safra","year":"1989","unstructured":"Safra, S., Vardi, M.Y.: On \u03c9$\\omega$-automata and temporal logic. In: Proc. 21st ACM Symp. on Theory of Computing, pp.\u00a0127\u2013137 (1989)"},{"key":"4_CR66","series-title":"LIPIcs","first-page":"661","volume-title":"Proc. 26th Symp. on Theoretical Aspects of Computer Science","author":"S. Schewe","year":"2009","unstructured":"Schewe, S.: B\u00fcchi complementation made tight. In: Proc. 26th Symp. on Theoretical Aspects of Computer Science. LIPIcs, vol.\u00a03, pp.\u00a0661\u2013672. Schloss Dagstuhl\u2014Leibniz-Zentrum fuer Informatik, Wadern (2009)"},{"key":"4_CR67","series-title":"LNCS","first-page":"167","volume-title":"Proc. 12th Int. Conf. on Foundations of Software Science and Computation Structures","author":"S. Schewe","year":"2009","unstructured":"Schewe, S.: Tighter bounds for the determinisation of B\u00fcchi automata. In: Proc. 12th Int. Conf. on Foundations of Software Science and Computation Structures. LNCS, vol.\u00a05504, pp.\u00a0167\u2013181. Springer, Heidelberg (2009)"},{"key":"4_CR68","series-title":"Leibniz International Proceedings in Informatics (LIPIcs)","first-page":"400","volume-title":"Proc. 30th Conf. on Foundations of Software Technology and Theoretical Computer Science","author":"S. Schewe","year":"2010","unstructured":"Schewe, S.: Beyond hyper-minimisation\u2014minimising 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.\u00a08, pp.\u00a0400\u2013411 (2010)"},{"key":"4_CR69","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logic. J. ACM 32, 733\u2013749 (1985)","journal-title":"J. ACM"},{"key":"4_CR70","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"A.P. Sistla","year":"1987","unstructured":"Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for B\u00fcchi automata with applications to temporal logic. Theor. Comput. Sci. 49, 217\u2013237 (1987)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR71","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/10722167_21","volume-title":"Proc. 12th Int. Conf. on Computer Aided Verification","author":"F. Somenzi","year":"2000","unstructured":"Somenzi, F., Bloem, R.: Efficient B\u00fcchi automata from LTL formulae. In: Proc. 12th Int. Conf. on Computer Aided Verification. LNCS, vol.\u00a01855, pp.\u00a0248\u2013263. Springer, Heidelberg (2000)"},{"key":"4_CR72","unstructured":"Synopsys: Assertion-based verification (2003)"},{"issue":"2","key":"4_CR73","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R.E. Tarjan","year":"1972","unstructured":"Tarjan, R.E.: Depth first search and linear graph algorithms. SIAM J. Comput. 1(2), 146\u2013160 (1972)","journal-title":"SIAM J. Comput."},{"key":"4_CR74","first-page":"133","volume-title":"Handbook of Theoretical Computer Science","author":"W. Thomas","year":"1990","unstructured":"Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, pp.\u00a0133\u2013191 (1990)"},{"key":"4_CR75","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/BF00709154","volume":"1","author":"A. Valmari","year":"1992","unstructured":"Valmari, A.: A stubborn attack on state explosion. Form. Methods Syst. Des. 1, 297\u2013322 (1992)","journal-title":"Form. Methods Syst. Des."},{"issue":"2","key":"4_CR76","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1016\/0022-0000(86)90026-7","volume":"32","author":"M.Y. Vardi","year":"1986","unstructured":"Vardi, M.Y., Wolper, P.: Automata-theoretic techniques for modal logics of programs. J. Comput. Syst. Sci. 32(2), 182\u2013221 (1986)","journal-title":"J. Comput. Syst. Sci."},{"issue":"1","key":"4_CR77","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1\u201337 (1994)","journal-title":"Inf. Comput."},{"key":"4_CR78","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1109\/LICS.1996.561357","volume-title":"Proc. 11th IEEE Symp. on Logic in Computer Science","author":"B. Willems","year":"1996","unstructured":"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.\u00a0294\u2013303 (1996)"},{"key":"4_CR79","first-page":"185","volume-title":"Proc. 24th IEEE Symp. on Foundations of Computer Science","author":"P. Wolper","year":"1983","unstructured":"Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths. In: Proc. 24th IEEE Symp. on Foundations of Computer Science, pp.\u00a0185\u2013194 (1983)"},{"key":"4_CR80","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/11787006_50","volume-title":"Proc. 33rd Int. Colloq. on Automata, Languages, and Programming","author":"Q. Yan","year":"2006","unstructured":"Yan, Q.: Lower bounds for complementation of \u03c9$\\omega$-automata via the full automata technique. In: Proc. 33rd Int. Colloq. on Automata, Languages, and Programming. LNCS, vol.\u00a04052, pp.\u00a0589\u2013600. Springer, Heidelberg (2006)"},{"issue":"1\u20132","key":"4_CR81","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/S0304-3975(98)00009-7","volume":"200","author":"W. Zielonka","year":"1998","unstructured":"Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci. 200(1\u20132), 135\u2013183 (1998)","journal-title":"Theor. Comput. Sci."}],"container-title":["Handbook of Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10575-8_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T08:06:52Z","timestamp":1526630812000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10575-8_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319105741","9783319105758"],"references-count":81,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10575-8_4","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}