{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T22:37:45Z","timestamp":1761950265598,"version":"build-2065373602"},"publisher-location":"Berlin, Heidelberg","reference-count":83,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540697350"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-69738-1_10","type":"book-chapter","created":{"date-parts":[[2007,11,12]],"date-time":"2007-11-12T12:58:07Z","timestamp":1194872287000},"page":"137-150","source":"Crossref","is-referenced-by-count":53,"title":["Automata-Theoretic Model Checking Revisited"],"prefix":"10.1007","author":[{"given":"Moshe Y.","family":"Vardi","sequence":"first","affiliation":[]}],"member":"297","reference":[{"unstructured":"Albin, K., et al.: Property specification language reference manual. Technical Report Version 1.1, Accellera (2004)","key":"10_CR1"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","volume-title":"Theory and Applications of Satisfiability Testing","author":"R. Armoni","year":"2005","unstructured":"Armoni, R., et al.: Efficient LTL compilation for SAT-based model checking. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, Springer, Heidelberg (2005)"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46002-0_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Armoni","year":"2002","unstructured":"Armoni, R., et al.: The ForSpec temporal logic: A new temporal property-specification logic. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol.\u00a02280, Springer, Heidelberg (2002)"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11940197_11","volume-title":"Formal Approaches to Software Testing and Runtime Verification","author":"R. Armoni","year":"2006","unstructured":"Armoni, R., Korchemny, D., Tiemeyer, A.: Deterministic dynamic monitors for linear-time assertions. In: Havelund, K., et al. (eds.) Formal Approaches to Software Testing and Runtime Verification. LNCS, vol.\u00a04262, Springer, Heidelberg (2006)"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","first-page":"277","volume-title":"Graph-Theoretic Concepts in Computer Science","author":"J.L. Balc\u00e1zar","year":"1990","unstructured":"Balc\u00e1zar, J.L., Lozano, A.: The complexity of graph problems for succinctly represented graphs. In: Nagl, M. (ed.) WG 1989. LNCS, vol.\u00a0411, pp. 277\u2013285. Springer, Heidelberg (1990)"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/11804192_13","volume-title":"Formal Methods for Components and Objects","author":"J. Barnat","year":"2006","unstructured":"Barnat, J., Brim, L., Cerna, I.: Cluster-based LTL model checking of large systems. In: de Boer, F.S., et al. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 259\u2013279. Springer, Heidelberg (2006)"},{"doi-asserted-by":"crossref","unstructured":"Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. In: Proc. 7th Int\u2019l Workshop on Formal Methods for Industrial Critical Systems, Electr. Notes Theor. Comput. Sci., vol. 66, no. 2 (2002)","key":"10_CR7","DOI":"10.1016\/S1571-0661(04)80410-9"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., et al.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol.\u00a01579, Springer, Heidelberg (1999)"},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Methods in Computer-Aided Design","author":"R. Bloem","year":"2000","unstructured":"Bloem, R., Gabow, H.N., Somenzi, F.: An algorithm for strongly connected component analysis in n logn symbolic steps. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, Springer, Heidelberg (2000)"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48683-6_21","volume-title":"Computer Aided Verification","author":"R. Bloem","year":"1999","unstructured":"Bloem, R., Ravi, K., Somenzi, F.: Efficient decision procedures for model checking of linear time logic properties. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, Springer, Heidelberg (1999)"},{"doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean-function manipulation. IEEE Trans. on Computers\u00a0C-35(8) (1986)","key":"10_CR11","DOI":"10.1109\/TC.1986.1676819"},{"key":"10_CR12","first-page":"1","volume-title":"Proc. International Congress on Logic, Method, and Philosophy of Science 196","author":"J.R. B\u00fcchi","year":"1962","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. International Congress on Logic, Method, and Philosophy of Science 196, pp. 1\u201312. Stanford University Press, Stanford (1962)"},{"issue":"2","key":"10_CR13","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch, J.R., et al.: Symbolic model checking: 1020 states and beyond. Information and Computation\u00a098(2), 142\u2013170 (1992)","journal-title":"Information and Computation"},{"unstructured":"Bustan, D., Fisman, D.: John Havlicek.: Automata construction for psl. Technical report, The Weizmann Institute of Science, Technical Report MCS05-04 (May 2005)","key":"10_CR14"},{"key":"10_CR15","doi-asserted-by":"crossref","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-tapes: A simplified approach. Journal of Computer and System Sciences\u00a08, 117\u2013141 (1974)","journal-title":"Journal of Computer and System Sciences"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., et al.: Nusmv 2: An opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, Springer, Heidelberg (2002)"},{"doi-asserted-by":"crossref","unstructured":"Cimatti, A., Roveri, M., Semprini, S., Tonetta, S.: From psl to nba: A modular symbolic encoding. In: Proc. 6th Int\u2019l Conf. on Formal Methods in Computer-Aided design (2006)","key":"10_CR17","DOI":"10.1109\/FMCAD.2006.19"},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Methods in Computer-Aided Design","author":"A. Cimatti","year":"2004","unstructured":"Cimatti, A., Roveri, M., Sheridan, D.: Bounded verification of past ltl. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, Springer, Heidelberg (2004)"},{"issue":"1","key":"10_CR19","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1023\/A:1008615614281","volume":"10","author":"E.M. Clarke","year":"1997","unstructured":"Clarke, E.M., Grumberg, O., Hamaguchi, K.: Another look at ltl model checking. Formal Methods in System Design\u00a010(1), 47\u201371 (1997)","journal-title":"Formal Methods in System Design"},{"issue":"2","key":"10_CR20","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems\u00a08(2), 244\u2013263 (1986)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10_CR21","first-page":"415","volume-title":"Computer Aided Verification, Proc. 6th International Conference, Stanford, California, USA, June 21-23","author":"E.M. Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. In: Computer Aided Verification, Proc. 6th International Conference, Stanford, California, USA, June 21-23, pp. 415\u2013427. Springer, New York (1994)"},{"key":"10_CR22","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"10_CR23","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1109\/6.499951","volume":"33","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Kurshan, R.P.: Computer aided verification. IEEE Spectrum\u00a033, 61\u201367 (1986)","journal-title":"IEEE Spectrum"},{"key":"10_CR24","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"E.M. Clarke","year":"1996","unstructured":"Clarke, E.M., Wing, J.M.: Formal methods: State of the art and future directions. ACM Computing Surveys\u00a028, 626\u2013643 (1996)","journal-title":"ACM Computing Surveys"},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"F. Copty","year":"2001","unstructured":"Copty, F., et al.: Benefits of bounded model checking at an industrial setting. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, Springer, Heidelberg (2001)"},{"key":"10_CR26","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 and McGraw-Hill, Cambridge (1990)"},{"key":"10_CR27","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"Courcoubetis, C., et al.: Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design\u00a01, 275\u2013288 (1992)","journal-title":"Formal Methods in System Design"},{"doi-asserted-by":"crossref","unstructured":"Couvreur, J-M.: On-the-fly verification of linear temporal logic. In: Proc. World Congress on Formal Methods, pp. 253\u2013271 (1999)","key":"10_CR28","DOI":"10.1007\/3-540-48119-2_16"},{"key":"10_CR29","series-title":"Lecture Notes in Computer Science","volume-title":"Model Checking Software","author":"J.M. Couvreur","year":"2005","unstructured":"Couvreur, J.M., Duret-Lutz, A., Poitrenaud, D.: On-the-fly emptiness checks for generalized B\u00fcchi automata. In: Godefroid, P. (ed.) Model Checking Software. LNCS, vol.\u00a03639, Springer, Heidelberg (2005)"},{"key":"10_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48683-6_23","volume-title":"Computer Aided Verification","author":"N. Daniele","year":"1999","unstructured":"Daniele, N., Guinchiglia, F., Vardi, M.Y.: Improved automata generation for linear temporal logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, Springer, Heidelberg (1999)"},{"key":"10_CR31","first-page":"76","volume-title":"Proc. 12th Int\u2019l Workshop on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems","author":"A. Duret-Lutz","year":"2004","unstructured":"Duret-Lutz, A., Poitrenaud, D.: Spot: An extensible model checking library using transition-based generalized b\u00fcchi automata. In: Proc. 12th Int\u2019l Workshop on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems, pp. 76\u201383. IEEE Computer Society Press, Los Alamitos (2004)"},{"key":"10_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/3-540-10003-2_69","volume-title":"Automata, Languages and Programming","author":"E.A. Emerson","year":"1980","unstructured":"Emerson, E.A., Clarke, E.M.: Characterizing correctness properties of parallel programs using fixpoints. In: de Bakker, J.W., van Leeuwen, J. (eds.) Automata, Languages and Programming. LNCS, vol.\u00a085, pp. 169\u2013181. Springer, Heidelberg (1980)"},{"unstructured":"Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional \u03bc-calculus. In: Proc. 1st Symp. on Logic in Computer Science, pp. 267\u2013278, Cambridge (June 1986)","key":"10_CR33"},{"key":"10_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/3-540-44618-4_13","volume-title":"CONCUR 2000 - Concurrency Theory","author":"K. Etessami","year":"2000","unstructured":"Etessami, K., Holzmann, G.J.: Optimizing B\u00fcchi automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 153\u2013167. Springer, Heidelberg (2000)"},{"key":"10_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/3-540-45319-9_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Fisler","year":"2001","unstructured":"Fisler, K., et al.: Is there a best symbolic cycle-detection algorithm? In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031, pp. 420\u2013434. Springer, Heidelberg (2001)"},{"issue":"4","key":"10_CR36","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\u2019l J. of Foundations of Computer Science\u00a017(4), 851\u2013867 (2006)","journal-title":"Int\u2019l J. of Foundations of Computer Science"},{"key":"10_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/3-540-45089-0_5","volume-title":"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 bchi automata. In: Ibarra, O.H., Dang, Z. (eds.) CIAA 2003. LNCS, vol.\u00a02759, pp. 35\u201348. Springer, Heidelberg (2003)"},{"key":"10_CR38","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"728","DOI":"10.1007\/11591191_50","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C. Fritz","year":"2005","unstructured":"Fritz, C.: Concepts of automata construction from LTL. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol.\u00a03835, pp. 728\u2013742. Springer, Heidelberg (2005)"},{"key":"10_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P. Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to b\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 53\u201365. Springer, Heidelberg (2001)"},{"key":"10_CR40","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Geldenhuys","year":"2004","unstructured":"Geldenhuys, J., Valmari, A.: Tarjan\u2019s algorithm makes on-the-fly LTL verification more efficient. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, Springer, Heidelberg (2004)"},{"unstructured":"Gentilini, R., Piazza, C., Policriti, A.: Computing strongly connected components in a linear number of symbolic steps. In: 14th ACM-SIAM Symposium on Discrete Algorithms, Baltimore, Maryland, pp. 573\u2013582 (2003)","key":"10_CR41"},{"key":"10_CR42","first-page":"3","volume-title":"Protocol Specification, Testing, and Verification","author":"R. Gerth","year":"1995","unstructured":"Gerth, R., et al.: Simple on-the-fly automatic verification of linear temporal logic. In: Dembiski, P., Sredniawa, M. (eds.) Protocol Specification, Testing, and Verification, pp. 3\u201318. Chapman and Hall, Boca Raton (1995)"},{"key":"10_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/3-540-36135-9_20","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2002","author":"D. Giannakopoulou","year":"2002","unstructured":"Giannakopoulou, D., Lerda, F.: From states to transitions: Improving translation of LTL formulae to b\u00fcchi automata. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol.\u00a02529, pp. 308\u2013326. Springer, Heidelberg (2002)"},{"unstructured":"Godefroid, P., Holzmann, G.J.: On the verification of temporal properties. In: Proc. 13th Int. Conf on Protocol Specification Testing and Verification, pp. 109\u2013124 (1993)","key":"10_CR44"},{"key":"10_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_51","volume-title":"Computer Aided Verification","author":"S. Gurumurthy","year":"2002","unstructured":"Gurumurthy, S., Bloem, R., Somenzi, F.: Fair simulation minimization. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, Springer, Heidelberg (2002)"},{"key":"10_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1007\/978-3-540-39724-3_10","volume-title":"Correct Hardware Design and Verification Methods","author":"S. Gurumurthy","year":"2003","unstructured":"Gurumurthy, S., et al.: On complementing nondeterministic B\u00fcchi automata. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 96\u2013110. Springer, Heidelberg (2003)"},{"key":"10_CR47","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"R.H. Hardin","year":"1996","unstructured":"Hardin, R.H., Har\u2019el, Z., Kurshan, R.P.: COSPAN. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, Springer, Heidelberg (1996)"},{"key":"10_CR48","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1023\/A:1008727508722","volume":"18","author":"R.H. Hardin","year":"2001","unstructured":"Hardin, R.H., et al.: A new heuristic for bad cycle detection using BDDs. Formal Methods in System Design\u00a018, 131\u2013140 (2001)","journal-title":"Formal Methods in System Design"},{"issue":"5","key":"10_CR49","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. on Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. on Software Engineering"},{"doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Peled, D., Yannakakis, M.: On nested depth-first search. In: Proc. 2nd Spin Workshop on The Spin Verification System, pp. 23\u201332. Amer. Math. Soc. (1996)","key":"10_CR50","DOI":"10.1090\/dimacs\/032\/03"},{"issue":"3","key":"10_CR51","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal methods in System Design\u00a019(3), 291\u2013314 (2001)","journal-title":"Formal methods in System Design"},{"issue":"2","key":"10_CR52","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. on Computational Logic\u00a02(2), 408\u2013429 (2001)","journal-title":"ACM Trans. on Computational Logic"},{"key":"10_CR53","first-page":"591","volume":"305","author":"O. Kupferman","year":"2005","unstructured":"Kupferman, O., Vardi, M.Y.: From complementation to certification. Theoretical Computer Science\u00a0305, 591\u2013606 (2005)","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"10_CR54","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1145\/1055686.1055689","volume":"6","author":"O. Kupferman","year":"2005","unstructured":"Kupferman, O., Vardi, M.Y.: From linear time to branching time. ACM Trans. on Computational Logic\u00a06(2\u00a06(2), 273\u2013294 (2005)","journal-title":"ACM Trans. on Computational Logic\u00a06(2"},{"doi-asserted-by":"crossref","unstructured":"Kurshan, R.P.: Computer Aided Verification of Coordinating Processes. Princeton Univ. Press (1994)","key":"10_CR55","DOI":"10.1515\/9781400864041"},{"doi-asserted-by":"crossref","unstructured":"Kurshan, R.P.: Formal verification in a commercial setting. In: Proc. Conf. on Design Automation (DAC\u201897), vol.\u00a034, pp. 258\u2013262 (1997)","key":"10_CR56","DOI":"10.1145\/266021.266089"},{"key":"10_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"380","DOI":"10.1007\/978-3-540-30579-8_25","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T. Latvala","year":"2005","unstructured":"Latvala, T., et al.: Simple is better: Efficient bounded model checking for past ltl. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 380\u2013395. Springer, Heidelberg (2005)"},{"key":"10_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/3-540-46691-6_8","volume-title":"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: Pandu Rangan, C., Raman, V., Ramanujam, R. (eds.) Foundations of Software Technology and Theoretical Computer Science. LNCS, vol.\u00a01738, pp. 97\u2013109. Springer, Heidelberg (1999)"},{"key":"10_CR59","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Norwell (1993)"},{"key":"10_CR60","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)"},{"doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proc. 18th IEEE Symp. on Foundation of Computer Science, pp. 46\u201357 (1977)","key":"10_CR61","DOI":"10.1109\/SFCS.1977.32"},{"key":"10_CR62","first-page":"46","volume-title":"Proc. 18th IEEE Symp. on Foundation of Computer Science","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proc. 18th IEEE Symp. on Foundation of Computer Science, pp. 46\u201357. IEEE Computer Society Press, Los Alamitos (1977)"},{"key":"10_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"J.P. Queille","year":"1982","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in Cesar. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) International Symposium on Programming. LNCS, vol.\u00a0137, pp. 337\u2013351. Springer, Heidelberg (1982)"},{"key":"10_CR64","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 Journal of Research and Development\u00a03, 115\u2013125 (1959)","journal-title":"IBM Journal of Research and Development"},{"doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of \u03c9-automata. In: Proc. 29th IEEE Symp. on Foundations of Computer Science, pp. 319\u2013327, White Plains (October 1988)","key":"10_CR65","DOI":"10.1109\/SFCS.1988.21948"},{"key":"10_CR66","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Schwoon","year":"2005","unstructured":"Schwoon, S., Esparza, J.: A note on on-the-fly verification algorithms. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, Springer, Heidelberg (2005)"},{"key":"10_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"126","DOI":"10.1007\/978-3-540-39724-3_12","volume-title":"Correct Hardware Design and Verification Methods","author":"R. Sebastiani","year":"2003","unstructured":"Sebastiani, R., Tonetta, S.: more deterministic\u201d vs. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 126\u2013140. Springer, Heidelberg (2003)"},{"key":"10_CR68","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"R. Sebastiani","year":"2005","unstructured":"Sebastiani, R., Tonetta, S., Vardi, M.Y.: Symbolic systems, explicit properties: on hybrid approaches for LTL symbolic model checking. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, Springer, Heidelberg (2005)"},{"key":"10_CR69","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. Theoretical Computer Science\u00a049, 217\u2013237 (1987)","journal-title":"Theoretical Computer Science"},{"key":"10_CR70","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_21","volume-title":"Computer Aided Verification","author":"F. Somenzi","year":"2000","unstructured":"Somenzi, F., Bloem, R.: Efficient B\u00fcchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, Springer, Heidelberg (2000)"},{"key":"10_CR71","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Methods in Computer-Aided Design","author":"F. Somenzi","year":"2002","unstructured":"Somenzi, F., Ravi, K., Bloem, R.: Analysis of symbolic scc hull algorithms. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, Springer, Heidelberg (2002)"},{"issue":"1\u20132","key":"10_CR72","first-page":"127","volume":"70","author":"H. Tauriainen","year":"2006","unstructured":"Tauriainen, H.: Nested emptiness search for generalized B\u00fcchi automata. Fundamenta Informaticae\u00a070(1\u20132), 127\u2013154 (2006)","journal-title":"Fundamenta Informaticae"},{"doi-asserted-by":"crossref","unstructured":"Thirioux, X.: Simple and efficient translation from LTL formulas to B\u00fcchi automata. Electr. Notes Theor. Comput. Sci.\u00a066(2) (2002)","key":"10_CR73","DOI":"10.1016\/S1571-0661(04)80409-2"},{"key":"10_CR74","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"575","DOI":"10.1007\/3-540-57887-0_116","volume-title":"Theoretical Aspects of Computer Software","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y.: Nontraditional applications of automata theory. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol.\u00a0789, pp. 575\u2013597. Springer, Heidelberg (1994)"},{"key":"10_CR75","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency","author":"M.Y. Vardi","year":"1996","unstructured":"Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol.\u00a01043, pp. 238\u2013266. Springer, Heidelberg (1996)"},{"key":"10_CR76","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45319-9_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M.Y. Vardi","year":"2001","unstructured":"Vardi, M.Y.: Branching vs.\u00a0linear time: Final showdown. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031, pp. 1\u201322. Springer, Heidelberg (2001)"},{"unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. 1st Symp. on Logic in Computer Science, Cambridge, June 1986, pp. 332\u2013344 (1986)","key":"10_CR77"},{"issue":"1","key":"10_CR78","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. Information and Computation\u00a0115(1), 1\u201337 (1994)","journal-title":"Information and Computation"},{"issue":"1\u20132","key":"10_CR79","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"Wolper, P.: Temporal logic can be more expressive. Information and Control\u00a056(1\u20132), 72\u201399 (1983)","journal-title":"Information and Control"},{"key":"10_CR80","first-page":"110","volume":"136","author":"P. Wolper","year":"1985","unstructured":"Wolper, P.: The tableau method for temporal logic: An overview. Logique et Analyse\u00a0136, 110\u2013111 (1985)","journal-title":"Logique et Analyse"},{"doi-asserted-by":"crossref","unstructured":"Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths. In: Proc. 24th IEEE Symp. on Foundations of Computer Science, Tucson, pp. 185\u2013194 (1983)","key":"10_CR81","DOI":"10.1109\/SFCS.1983.51"},{"key":"10_CR82","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/11787006_50","volume-title":"Automata, Languages and Programming","author":"Q. Yan","year":"2006","unstructured":"Yan, Q.: Lower bounds for complementation of \u03c9-automata via the full automata technique. In: Bugliesi, M., et al. (eds.) ICALP 2006. LNCS, vol.\u00a04052, pp. 589\u2013600. Springer, Heidelberg (2006)"},{"key":"10_CR83","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1007\/3-540-45620-1_26","volume-title":"Automated Deduction - CADE-18","author":"L. Zhang","year":"2002","unstructured":"Zhang, L., Malik, S.: The quest for efficient Boolean satisfiability solvers. In: Voronkov, A. (ed.) Automated Deduction - CADE-18. LNCS (LNAI), vol.\u00a02392, pp. 295\u2013313. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69738-1_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:45:01Z","timestamp":1620017101000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69738-1_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540697350"],"references-count":83,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69738-1_10","relation":{},"subject":[]}}