{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T16:20:13Z","timestamp":1649175613146},"reference-count":18,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2005,6,1]],"date-time":"2005-06-01T00:00:00Z","timestamp":1117584000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Higher-Order Symb Comput"],"published-print":{"date-parts":[[2005,6]]},"DOI":"10.1007\/s10990-005-7007-4","type":"journal-article","created":{"date-parts":[[2005,7,12]],"date-time":"2005-07-12T17:54:33Z","timestamp":1121190873000},"page":"79-120","source":"Crossref","is-referenced-by-count":0,"title":["Relativizations for the Logic-Automata Connection"],"prefix":"10.1007","volume":"18","author":[{"given":"Nils","family":"Klarlund","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7007_CR1","doi-asserted-by":"crossref","unstructured":"Ayari, A. and Basin, D. Bounded model construction for monadic second-order logics. In Computer Aided Verification, 2000 pp. 99\u2013112.","DOI":"10.1007\/10722167_11"},{"key":"7007_CR2","unstructured":"Basin, D. and Klarlund, N. 1998, Automata based symbolic reasoning in hardware verification. Formal Methods in System Design, Extended version of \u201cHardware verification using monadic second-order logic,\u201d Computer aided verification: 7th International Conference, CAV \u201895, LNCS 939, 1995, pp. 255\u2013288."},{"key":"7007_CR3","unstructured":"Bell, J. and Machover, M. A Course in Mathematical Logic. North-Holland, 1977."},{"issue":"3","key":"7007_CR4","doi-asserted-by":"crossref","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, 24(3) (1992) 293\u2013318.","journal-title":"ACM Computing Surveys"},{"key":"7007_CR5","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1002\/malq.19600060105","volume":"6","author":"J. B\u00fcchi","year":"1960","unstructured":"B\u00fcchi, J. Weak second-order arithmetic and finite automata. Z. Math. Logik Grundl. Math., 6 (1960) 66\u201392.","journal-title":"Z. Math. Logik Grundl. Math."},{"key":"7007_CR6","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1090\/S0002-9947-1961-0139530-9","volume":"98","author":"C. Elgot","year":"1961","unstructured":"Elgot, C. Decision problems of finite automata design and related arithmetics. Trans. Amer. Math. Soc., 98 (1961) 21\u201352.","journal-title":"Trans. Amer. Math. Soc."},{"key":"7007_CR7","doi-asserted-by":"crossref","unstructured":"Henriksen, J., Jensen, J., J\u00f8rgensen, M., Klarlund, N., Paige, B., Rauhe, T., and Sandholm, A. Mona: Monadic Second-order logic in practice. In Tools and Algorithms for the Construction and Analysis of Systems, First International Workshop, TACAS \u201895, LNCS 1019, 1996.","DOI":"10.7146\/brics.v2i21.19923"},{"key":"7007_CR8","unstructured":"Elgaard, J., Klarlund, N., A.M. Mona 1.x: New techniques for WS1S and WS2S. In Computer Aided Verification, CAV \u201898, Proceedings, Vol. 1427 of LNCS. Springer Verlag, 1998."},{"key":"7007_CR9","doi-asserted-by":"crossref","unstructured":"Kelb, P., Margaria, T., Mendler, M., and Gsottberger, C. Mosel: A flexible toolset for Monadic Second-order Logic. In Computer Aided Verification, CAV \u201897, Proceedings, 1997,","DOI":"10.1007\/BFb0035388"},{"key":"7007_CR10","doi-asserted-by":"crossref","unstructured":"Klarlund, N. Mona & Fido: The logic-automaton connection in practice. In CSL \u201897 Proceedings. LNCS 1414, Springer-Verlag, 1998.","DOI":"10.1007\/BFb0028022"},{"key":"7007_CR11","unstructured":"Klarlund, N. and M\u00f8ller, A. MONA Version 1.3 User Manual, BRICS. URL: http:\/\/www.brics.dk\/mona, 1998,"},{"issue":"4","key":"7007_CR12","doi-asserted-by":"crossref","first-page":"571","DOI":"10.1142\/S012905410200128X","volume":"13","author":"N. Klarlund","year":"2002","unstructured":"Klarlund, N., M\u00f8ller, A., and Schwartzbach, M. MONA implementation Secrets. International Journal of Foundations of Computer Science, 13(4) (2002) 571\u2013586.","journal-title":"International Journal of Foundations of Computer Science"},{"key":"7007_CR13","doi-asserted-by":"crossref","unstructured":"M\u00f8ller, A. and Schwartzbach, M. The pointer assertion logic engine. In Proceedings of ACM SIGPLAN Conference of Programming Language Design and Implementation, 2001.","DOI":"10.1145\/378795.378851"},{"key":"7007_CR14","doi-asserted-by":"crossref","unstructured":"Smith, M. and Klarlund, N. Verification of a sliding window protocol using IOA and MONA. In FORTE\/PSTV 2000: IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XIII), and Protocol Specification, Testing, and Verification (PSTV XX). Kluwer Academic Publishers, 2000 pp. 19\u201334.","DOI":"10.1007\/978-0-387-35533-7_2"},{"key":"7007_CR15","doi-asserted-by":"crossref","unstructured":"Straubing, H. Finite Automata, Formal Logic, and Circuit Complexity. Birkh\u00e4user, 1994.","DOI":"10.1007\/978-1-4612-0289-9"},{"key":"7007_CR16","doi-asserted-by":"crossref","unstructured":"Thomas, W. Languages, automata, and logic. In Handbook of Formal Languages. G. Rozenberg and A. Salomaa (Eds.). Springer Verlag, Chapt. Languages, automata, and logic, 1997.","DOI":"10.1007\/978-3-642-59126-6_7"},{"key":"7007_CR17","unstructured":"Trakhtenbrot, B. Finite automata and the logic of one-place predicates. Sib. Math. J, 3 (1962) 103\u2013131. In Russian. English translation: AMS Transl., 59 (1966), 23\u201355."},{"key":"7007_CR18","doi-asserted-by":"crossref","unstructured":"Vaillette, N. Logical specification of finite-state transductions for NLP. Natural Language Engineering, 9(1) (2003).","DOI":"10.1017\/S1351324903003103"}],"container-title":["Higher-Order and Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-005-7007-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10990-005-7007-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-005-7007-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,8]],"date-time":"2020-04-08T06:26:50Z","timestamp":1586327210000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10990-005-7007-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,6]]},"references-count":18,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2005,6]]}},"alternative-id":["7007"],"URL":"https:\/\/doi.org\/10.1007\/s10990-005-7007-4","relation":{},"ISSN":["1388-3690","1573-0557"],"issn-type":[{"value":"1388-3690","type":"print"},{"value":"1573-0557","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,6]]}}}