{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:17:28Z","timestamp":1725484648148},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540425540"},{"type":"electronic","value":"9783540448020"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44802-0_27","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T04:15:38Z","timestamp":1180671338000},"page":"384-398","source":"Crossref","is-referenced-by-count":0,"title":["Decision Procedure for an Extension of WS1S"],"prefix":"10.1007","author":[{"given":"Felix","family":"Klaedtke","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,8,30]]},"reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"A. Ayari, D. Basin, and S. Friedrich. Structural and behavioral modeling with monadic logics. In 29th IEEE International Symposium on Multiple-Valued Logic, pages 142\u2013151, 1999.","DOI":"10.1109\/ISMVL.1999.779709"},{"key":"27_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/10722167_16","volume-title":"12th International Conference on Computer-Aided Verification, CAV\u2019\u201900","author":"A. Ayari","year":"2000","unstructured":"A. Ayari, D. Basin, and F. Klaedtke. Decision procedures for inductive boolean functions based on alternating automata. In 12th International Conference on Computer-Aided Verification, CAV\u2019\u201900, volume 1855 of LNCS, pages 170\u2013186, 2000."},{"issue":"3","key":"27_CR3","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1023\/A:1008644009416","volume":"13","author":"D. Basin","year":"1998","unstructured":"D. Basin and N. Klarlund. Automata based symbolic reasoning in hardware verification. The Journal of Formal Methods in Systems Design, 13(3):255\u2013288, 1998.","journal-title":"The Journal of Formal Methods in Systems Design"},{"key":"27_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"6","DOI":"10.1007\/3-540-63174-7_2","volume-title":"1st International Workshop on Implementing Automata, WIA\u2019 96","author":"M. Biehl","year":"1997","unstructured":"M. Biehl, N. Klarlund, and T. Rauhe. Algorithms for guided tree automata. In 1st International Workshop on Implementing Automata, WIA\u2019 96, volume 1260 of LNCS, pages 6\u201325, 1997."},{"key":"27_CR5","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1002\/malq.19600060105","volume":"6","author":"J. B\u00fcchi","year":"1960","unstructured":"J. B\u00fcchi. Weak second-order arithmetic and finite automata. Zeitschrift der mathematischen Logik und Grundlagen der Mathematik, 6:66\u201392, 1960.","journal-title":"Zeitschrift der mathematischen Logik und Grundlagen der Mathematik"},{"key":"27_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/3-540-44612-5_23","volume-title":"25th International Symposium on Mathematical Foundations of Computer Science, MFCS 2000","author":"O. Carton","year":"2000","unstructured":"O. Carton and W. Thomas. The monadic theory of morphic infinite words and generalizations. In 25th International Symposium on Mathematical Foundations of Computer Science, MFCS 2000, volume 1893 of LNCS, pages 275\u2013284, 2000."},{"key":"27_CR7","unstructured":"H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree automata techniques and applications. Available on \n                    http:\/\/www.grappa.univ-lille3.fr\/tata\n                    \n                  , 1997."},{"key":"27_CR8","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1016\/S0022-0000(70)80041-1","volume":"4","author":"J. Doner","year":"1970","unstructured":"J. Doner. Tree acceptors and some of their applications. Journal of Computer and System Sciences, 4:406\u2013451, 1970.","journal-title":"Journal of Computer and System Sciences"},{"key":"27_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"516","DOI":"10.1007\/BFb0028773","volume-title":"10th International Conference on Computer Aided Verification, CAV\u201998","author":"J. Elgaard","year":"1998","unstructured":"J. Elgaard, N. Klarlund, and A. M\u00f8ller. Mona 1.x: New techniques for WS1S and WS2S. In 10th International Conference on Computer Aided Verification, CAV\u201998, volume 1427 of LNCS, pages 516\u2013520, 1998."},{"key":"27_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1007\/3-540-46425-5_8","volume-title":"9th European Symposium on Programming, ESOP\u201900","author":"J. Elgaard","year":"2000","unstructured":"J. Elgaard, A. M\u00f8ller, and M. Schwartzbach. Compile-time debugging of C programs working on trees. In 9th European Symposium on Programming, ESOP\u201900, volume 1782 of LNCS, pages 119\u2013134, 2000."},{"key":"27_CR11","doi-asserted-by":"publisher","first-page":"21","DOI":"10.2307\/1993511","volume":"98","author":"C. Elgot","year":"1961","unstructured":"C. Elgot. Decision problems of finite automata design and related arithmetics. Transactions of the AMS, 98:21\u201351, 1961.","journal-title":"Transactions of the AMS"},{"issue":"2","key":"27_CR12","doi-asserted-by":"publisher","first-page":"169","DOI":"10.2307\/2269808","volume":"31","author":"C. Elgot","year":"1966","unstructured":"C. Elgot and M. Rabin. Decidability and undecidability of extensions of second (first) order theory of (generalized) successor. Journal of Symbolic Logic, 31(2): 169\u2013181, 1966.","journal-title":"Journal of Symbolic Logic"},{"key":"27_CR13","volume-title":"Tree Automata","author":"F. G\u00e9cseg","year":"1984","unstructured":"F. G\u00e9cseg and M. Steinby. Tree Automata. Akad\u00e9miai Kiad\u00f3, Budapest, 1984."},{"key":"27_CR14","series-title":"PhD thesis","volume-title":"Inductive Boolean Function Manipulation: A Hardware Verification Methodology for Automatic Induction","author":"A. Gupta","year":"1994","unstructured":"A. Gupta. Inductive Boolean Function Manipulation: A Hardware Verification Methodology for Automatic Induction. PhD thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, USA, 1994."},{"key":"27_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/3-540-56922-7_3","volume-title":"5th International Conference on Computer-Aided Verification, CAV\u201993","author":"A. Gupta","year":"1993","unstructured":"A. Gupta and A. Fisher. Parametric circuit representation using inductive boolean functions. In 5th International Conference on Computer-Aided Verification, CAV\u201993, volume 697 of LNCS, pages 15\u201328, 1993."},{"key":"27_CR16","series-title":"Lect Notes Comput Sci","first-page":"89","volume-title":"1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS\u201995","author":"J. Henriksen","year":"1996","unstructured":"J. Henriksen, J. Jensen, M. J\u00f8rgensen, N. Klarlund, B. Paige, T. Rauhe, and A. Sandholm. Mona: Monadic second-order logic in practice. In 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS\u201995, volume 1019 of LNCS, pages 89\u2013110, 1996."},{"key":"27_CR17","unstructured":"J. Hopcroft and J. Ullman. Formal Languages and their Relation to Automata. Addison-Wesley, 1969."},{"key":"27_CR18","volume-title":"Diplomarbeit","author":"F. Klaedtke","year":"2000","unstructured":"F. Klaedtke. Induktive boolesche Funktionen, endliche Automaten und monadische Logik zweiter Stufe. Diplomarbeit, Institut f\u00fcr Informatik, Albert-Ludwigs-Universit\u00e4t, Freiburg i. Br., 2000. In German."},{"key":"27_CR19","unstructured":"N. Klarlund and A. M\u00f8ller. MONA Version 1.3 User Manual. BRICS Notes Series NS-98-3 (2.revision), Department of Computer Science, University of Aarhus, 1998."},{"key":"27_CR20","doi-asserted-by":"crossref","unstructured":"A. Meyer. Weak monadic second-order theory of successor is not elementary-recursive. In Logic Colloquium, volume 453 of Lecture Notes in Mathematics, pages 132\u2013154, 1975.","DOI":"10.1007\/BFb0064872"},{"key":"27_CR21","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1016\/0020-0190(94)00170-4","volume":"53","author":"A. Monti","year":"1995","unstructured":"A. Monti and A. Roncato. Completeness results concerning systolic tree automata and E0L languages. Information Processing Letters, 53:11\u201316, 1995.","journal-title":"Information Processing Letters"},{"key":"27_CR22","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/BF01691346","volume":"2","author":"J. Thatcher","year":"1968","unstructured":"J. Thatcher and J. Wright. Generalized finite automata theory with an application to a decision problem in second-order logic. Mathematical Systems Theory, 2:57\u201381, 1968.","journal-title":"Mathematical Systems Theory"},{"key":"27_CR23","doi-asserted-by":"crossref","unstructured":"W. Thomas. Languages, automata, and logic. In A. Salomaa and G. Rozenberg, editors, Handbook of Formal Languages, volume 3, chapter 7, pages 389\u2013455. Springer-Verlag, 1997.","DOI":"10.1007\/978-3-642-59126-6_7"},{"key":"27_CR24","first-page":"23","volume":"59","author":"B. Trakhtenbrot","year":"1966","unstructured":"B. Trakhtenbrot. Finite automata and the logic of one-place predicates. AMS, Transl., II. Ser., 59:23\u201355, 1966.","journal-title":"AMS, Transl., II. Ser."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44802-0_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,17]],"date-time":"2019-02-17T02:37:01Z","timestamp":1550371021000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44802-0_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425540","9783540448020"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-44802-0_27","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}