{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:06:06Z","timestamp":1776305166589,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":41,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540305538","type":"print"},{"value":"9783540316503","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11591191_28","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T09:44:25Z","timestamp":1132652665000},"page":"396-411","source":"Crossref","is-referenced-by-count":57,"title":["Experimental Evaluation of Classical Automata Constructions"],"prefix":"10.1007","author":[{"given":"Deian","family":"Tabakov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"28_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"538","DOI":"10.1007\/10722167_40","volume-title":"Computer Aided Verification","author":"Y. Abarbanel","year":"2000","unstructured":"Abarbanel, Y., Beer, I., Gluhovsky, L., Keidar, S., Wolfstal, Y.: FoCs - automatic generation of simulation checkers from formal specifications. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 538\u2013542. Springer, Heidelberg (2000)"},{"key":"28_CR2","doi-asserted-by":"crossref","unstructured":"Achlioptas, D.: Setting two variables at a time yields a new lower bound for random 3-SAT. In: Proc. of 32nd Annual ACM Symposium on Theory of Computing (2000)","DOI":"10.1145\/335305.335309"},{"key":"28_CR3","doi-asserted-by":"crossref","unstructured":"Aguirre, A.S.M., Vardi, M.Y.: Random 3-SAT and BDDs: The plot thickens further. In: Principles and Practice of Constraint Programming, pp. 121\u2013136 (2001)","DOI":"10.1007\/3-540-45578-7_9"},{"key":"28_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","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., 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: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, p. 296. Springer, Heidelberg (2002)"},{"key":"28_CR5","doi-asserted-by":"crossref","first-page":"596","DOI":"10.1145\/196244.196575","volume-title":"Proc. 31st Design Automation Conference","author":"D. Beatty","year":"1994","unstructured":"Beatty, D., Bryant, R.: Formally verifying a microprocessor using a simulation methodology. In: Proc. 31st Design Automation Conference, pp. 596\u2013602. IEEE Computer Society Press, Los Alamitos (1994)"},{"key":"28_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-44585-4_33","volume-title":"Computer Aided Verification","author":"I. Beer","year":"2001","unstructured":"Beer, I., Ben-David, S., Eisner, C., Fisman, D., Gringauze, A., Rodeh, Y.: The temporal logic sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 363\u2013367. Springer, Heidelberg (2001)"},{"key":"28_CR7","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511814068","volume-title":"Random Graphs","author":"B. Bollobas","year":"2001","unstructured":"Bollobas, B.: Random Graphs. Cambridge University Press, Cambridge (January 2001)"},{"key":"28_CR8","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean-function manipulation. IEEE Trans. on Computers\u00a0C-35(8) (1986)","DOI":"10.1109\/TC.1986.1676819"},{"issue":"3","key":"28_CR9","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R.E. Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys\u00a024(3), 293\u2013318 (1992)","journal-title":"ACM Computing Surveys"},{"key":"28_CR10","unstructured":"Brzozowski, J.A.: Canonical regular expressions and minimal state graphs for definite events. In: Mathematical theory of Automata. MRI Symposia Series, vol.\u00a012, pp. 529\u2013561. Polytechnic Press. Polytechnic Institute of Brooklyn (1962)"},{"key":"28_CR11","unstructured":"Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic model checking with partitioned transition relations. In: Proc. IFIP TC10\/WG 10.5 International Conference on Very Large Scale Integration, pp. 49\u201358 (1991)"},{"issue":"2","key":"28_CR12","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., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Information and Computation\u00a098(2), 142\u2013170 (1992)","journal-title":"Information and Computation"},{"key":"28_CR13","unstructured":"Cadence. SMV, http:\/\/www.cadence.com\/company\/cadence_labs_research.html"},{"key":"28_CR14","unstructured":"Cheeseman, P., Kanefsky, B., Taylor, W.M.: Where the really hard problems are. In: IJCAI 1991, pp. 331\u2013337 (1991)"},{"key":"28_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 359. Springer, Heidelberg (2002)"},{"issue":"4","key":"28_CR16","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. International Journal on Software Tools for Technology Transfer\u00a02(4), 410\u2013425 (2000)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"28_CR17","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":"28_CR18","unstructured":"Dubois, O., Boufkhad, Y., Mandler, J.: Typical random 3-SAT formulae and the satisfiability threshold. In: SODA, pp. 126\u2013127 (2000)"},{"key":"28_CR19","first-page":"1017","volume":"12","author":"E. Friedgut","year":"1999","unstructured":"Friedgut, E.: Necessary and sufficient conditions for sharp thresholds of graph properties, and the k-SAT problem. Journal of the A.M.S.\u00a012, 1017\u20131054 (1999)","journal-title":"Journal of the A.M.S."},{"key":"28_CR20","doi-asserted-by":"crossref","unstructured":"Glenn, J., Gasarch, W.I.: Implementing WS1S via finite automata: Performance issues. In: Workshop on Implementing Automata, pp. 75\u201386 (1997)","DOI":"10.1007\/3-540-63174-7_5"},{"key":"28_CR21","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/BF00264025","volume":"2","author":"D. Gries","year":"1973","unstructured":"Gries, D.: Describing an algorithm by Hopcroft. Acta Informatica\u00a02, 97\u2013109 (1973)","journal-title":"Acta Informatica"},{"key":"28_CR22","volume-title":"Logic Synthesis and Verification Algorithms","author":"G.D. Hachtel","year":"1996","unstructured":"Hachtel, G.D., Somenzi, F.: Logic Synthesis and Verification Algorithms. Kluwer Academic Publishers, Norwell (1996)"},{"key":"28_CR23","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/B978-0-12-417750-5.50022-1","volume-title":"The Theory of Machines and Computations","author":"J.E. Hopcroft","year":"1971","unstructured":"Hopcroft, J.E.: An n log n algorithm for minimizing the states in a finite automaton. In: Kohavi, Z. (ed.) The Theory of Machines and Computations, pp. 189\u2013196. Academic Press, London (1971)"},{"key":"28_CR24","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"J.E. Hopcroft","year":"1979","unstructured":"Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading (1979)"},{"key":"28_CR25","volume-title":"Sequential Machines: Selected Papers","author":"D.A. Huffman","year":"1964","unstructured":"Huffman, D.A.: The synthesis of sequential switching circuits. In: Moore, E.F. (ed.) Sequential Machines: Selected Papers. Addison-Wesley, Reading (1964)"},{"issue":"1","key":"28_CR26","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1002\/rsa.3240010106","volume":"1","author":"R.M. Karp","year":"1990","unstructured":"Karp, R.M.: The transitive closure of a random digraph. Random Struct. Algorithms\u00a01(1), 73\u201394 (1990)","journal-title":"Random Struct. Algorithms"},{"key":"28_CR27","unstructured":"Koster, A.M.C.A., Bodlaender, H.L., van Hoesel, C.P.M.: Treewidth: Computational experiments. ZIB-Report 01\u201338, Konrad-Zuse-Zentrum f\u00fcr Informationstechnik Berlin, Berlin, Germany, 2001. Also available as technical report UU-CS-2001-49 (Utrecht University) and research memorandum 02\/001 (Universiteit Maastricht)."},{"issue":"3","key":"28_CR28","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":"28_CR29","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1145\/377978.377993","volume":"2001","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Trans. on Computational Logic\u00a02001(2), 408\u2013429 (2001)","journal-title":"ACM Trans. on Computational Logic"},{"key":"28_CR30","doi-asserted-by":"crossref","unstructured":"Lee, D., Yannakakis, M.: Online minimization of transition systems. In: Proc. 24th ACM Symp. on Theory of Computing, Victoria, May 1992, pp. 264\u2013274 (1992)","DOI":"10.1145\/129712.129738"},{"key":"28_CR31","volume-title":"An introduction to formal languages and automata","author":"P. Linz","year":"1990","unstructured":"Linz, P.: An introduction to formal languages and automata. D. C. Heath and Company, Lexington (1990)"},{"key":"28_CR32","unstructured":"M\u00f8ller, A.: dk.brics.automaton (2004), http:\/\/www.brics.dk\/automaton\/"},{"key":"28_CR33","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, Dordrecht (1993)"},{"key":"28_CR34","doi-asserted-by":"crossref","unstructured":"Meyer, A.R., Fischer, M.J.: Economy of description by automata, grammars, and formal systems. In: Proc. 12th IEEE Symp. on Switching and Automata Theory, pp. 188\u2013191 (1971)","DOI":"10.1109\/SWAT.1971.11"},{"key":"28_CR35","doi-asserted-by":"crossref","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. 125\u2013129 (1972)","DOI":"10.1109\/SWAT.1972.29"},{"key":"28_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/11527695_19","volume-title":"Theory and Applications of Satisfiability Testing","author":"G. Pan","year":"2005","unstructured":"Pan, G., Vardi, M.Y.: Search vs. symbolic techniques in satisfiability solving. In: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 235\u2013250. Springer, Heidelberg (2005)"},{"issue":"1-2","key":"28_CR37","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/0004-3702(95)00045-3","volume":"81","author":"B. Selman","year":"1996","unstructured":"Selman, B., Mitchell, D.G., Levesque, H.J.: Generating hard satisfiability problems. Artificial Intelligence\u00a081(1-2), 17\u201329 (1996)","journal-title":"Artificial Intelligence"},{"issue":"3","key":"28_CR38","doi-asserted-by":"publisher","first-page":"566","DOI":"10.1137\/0213035","volume":"13","author":"R.E. Tarjan","year":"1984","unstructured":"Tarjan, R.E., Yannakakis, M.: Simple linear-time algorithms to test chordality of graphs, test acyclicity of hypergraphs, and selectively reduce acyclic hypergraphs. SIAM J. Comput.\u00a013(3), 566\u2013579 (1984)","journal-title":"SIAM J. Comput."},{"key":"28_CR39","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":"28_CR40","series-title":"Computing Science Note 93\/44","volume-title":"A taxonomy of finite automata minimization algorithmes","author":"B.W. Watson","year":"1993","unstructured":"Watson, B.W.: A taxonomy of finite automata minimization algorithmes. Computing Science Note 93\/44. Eindhoven University of Technology, The Netherlands (1993)"},{"key":"28_CR41","unstructured":"Watson, B.W.: Taxonomies and Toolkits of Regular Language Algorithms. PhD thesis, Eindhoven University of Technology, the Netherlands (1995)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11591191_28.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:02:28Z","timestamp":1605643348000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11591191_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540305538","9783540316503"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/11591191_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}