{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T05:00:25Z","timestamp":1777870825315,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540404934","type":"print"},{"value":"9783540450610","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-45061-0_54","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T15:54:04Z","timestamp":1184601244000},"page":"681-696","source":"Crossref","is-referenced-by-count":46,"title":["Monadic Second-Order Logics with Cardinalities"],"prefix":"10.1007","author":[{"given":"Felix","family":"Klaedtke","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Harald","family":"Rue\u00df","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,6,18]]},"reference":[{"key":"54_CR1","unstructured":"D. Basin and S. Friedrich, Combining WS1S and HOL, in FroCos\u201998, Applied Logic Series, 2000, pp. 39\u201356."},{"key":"54_CR2","series-title":"Lect Notes Comput Sci","first-page":"91","volume-title":"FMCAD\u201900","author":"D. Basin","year":"2000","unstructured":"D. Basin, S. Friedrich, and S. M\u00f6dersheim, B2M: A semantic based tool for BLIF hardware descriptions, in FMCAD\u201900, vol. 1954 of LNCS, 2000, pp. 91\u2013107."},{"key":"54_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, FMSD, 13 (1998), pp. 255\u2013288.","journal-title":"FMSD"},{"key":"54_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1007\/BFb0028751","volume-title":"CAV\u201998","author":"H. Comon","year":"1998","unstructured":"H. Comon and Y. Jurski, Multiple counters automata, safety analysis and Pres-burger arithmetic, in CAV\u201998, vol. 1427 of LNCS, 1998, pp. 268\u2013279."},{"key":"54_CR5","doi-asserted-by":"crossref","unstructured":"S. Dal Zilio and D. Lugiez, XML schema, tree logic and sheaves automata, Research Report 4631, INRIA, 2002.","DOI":"10.1007\/3-540-44881-0_18"},{"key":"54_CR6","doi-asserted-by":"crossref","first-page":"725","DOI":"10.1142\/S0218196700000315","volume":"10","author":"J. Dassow","year":"2000","unstructured":"J. Dassow and V. Mitrana, Finite automata over free groups, International Journal of Algebra and Computation, 10 (2000), pp. 725\u2013737.","journal-title":"International Journal of Algebra and Computation"},{"key":"54_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1007\/3-540-46541-3_29","volume-title":"STACS\u201900","author":"A. Finkel","year":"2000","unstructured":"A. Finkel and G. Sutre, Decidability of rechability problems for classes of two counter automata, in STACS\u201900, vol. 1770 of LNCS, 2000, pp. 346\u2013357."},{"key":"54_CR8","unstructured":"M. Gordon, Why higher-order logics is a good formalism for specifying and verifying hardware, in Formal Aspects of VLSI Design, North-Holland, 1986, pp. 153\u2013177."},{"key":"54_CR9","doi-asserted-by":"crossref","unstructured":"G. Gottlob and C. Koch, Monadic Datalog and the expressive power of languages for web information extraction, in PODS\u201902, 2002, pp. 17\u201328.","DOI":"10.1145\/543613.543617"},{"key":"54_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/3-540-60630-0_5","volume-title":"TACAS\u201995","author":"J. Henriksen","year":"1995","unstructured":"J. Henriksen, J. Jensen, M. Jorgensen, N. Klarlund, B. Paige, T. Rauhe, and A. Sandholm, Mona: Monadic second-order logic in practice, in TACAS\u201995, vol. 1019 of LNCS, 1995, pp. 89\u2013110."},{"key":"54_CR11","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1145\/322047.322058","volume":"25","author":"O. Ibarra","year":"1978","unstructured":"O. Ibarra, Reversal-bounded multicounter machines and their decision problems, JACM, 25 (1978), pp. 116\u2013133.","journal-title":"JACM"},{"key":"54_CR12","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0304-3975(01)00268-7","volume":"289","author":"O. Ibarra","year":"2002","unstructured":"O. Ibarra, J. Su, Z. Dang, T. Bultan, and R. Kemmerer, Counter machines and verification problems, TCS, 289 (2002), pp. 165\u2013189.","journal-title":"TCS"},{"key":"54_CR13","doi-asserted-by":"crossref","unstructured":"F. Klaedtke, CMona: Monadic second-order logics with linear cardinality constraints in practice. in preparation, 2003.","DOI":"10.1007\/3-540-45061-0_54"},{"key":"54_CR14","unstructured":"F. Klaedtke and H. Rue\u00df, WS1S with cardinality constraints, Technical Report SRI-CSL-05-01, SRI International, 2001."},{"key":"54_CR15","unstructured":"\u2014, Parikh automata and monadic second-order logics with linear cardinality constraints, Technical Report 177, Albert-Ludwigs-Universit\u00e4t Freiburg, 2002. (revised version)."},{"key":"54_CR16","series-title":"Lect Notes Comput Sci","first-page":"182","volume-title":"CIAA\u201900","author":"N. Klarlund","year":"2000","unstructured":"N. Klarlund, A. M\u00f8ller, and M. Schwartzbach, MONA implementation secrets, in CIAA\u201900, vol. 2088 of LNCS, 2000, pp. 182\u2013194."},{"key":"54_CR17","doi-asserted-by":"crossref","unstructured":"N. Klarlund, M. Nielsen, and K. Sunesen, Automated logical verification based on trace abstraction, in PODC\u201996, 1996, pp. 101\u2013110.","DOI":"10.1145\/248052.248069"},{"key":"54_CR18","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1145\/357172.357176","volume":"4","author":"L. Lamport","year":"1982","unstructured":"L. Lamport, R. Shostak, and M. Pease, The Byzantine Generals problem, TOPLAS, 4 (1982), pp. 382\u2013401.","journal-title":"TOPLAS"},{"key":"54_CR19","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/BFb0064872","volume":"453","author":"A. Meyer","year":"1975","unstructured":"A. Meyer, Weak monadic second-order theory of successor is not elementary-recursive, in Logic Colloquium, vol. 453 of LNM, 1975, pp. 132\u2013154.","journal-title":"Logic Colloquium"},{"key":"54_CR20","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/S0166-218X(00)00200-6","volume":"108","author":"V. Mitrana","year":"2001","unstructured":"V. Mitrana and R. Stiebe, Extended finite automata over groups, Discrete Applied Mathematics, 108 (2001), pp. 287\u2013300.","journal-title":"Discrete Applied Mathematics"},{"key":"54_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"548","DOI":"10.1007\/10722167_42","volume-title":"CAV\u201900","author":"S. Owre","year":"2000","unstructured":"S. Owre and H. Ruess, Integrating WS1S with PVS, in CAV\u201900, vol. 1855 of LNCS, 2000, pp. 548\u2013551."},{"key":"54_CR22","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/0304-3975(85)90136-7","volume":"39","author":"M. Parigot","year":"1985","unstructured":"M. Parigot and E. Pelz, A logical approach of Petri net languages, TCS, 39 (1985), pp. 155\u2013169.","journal-title":"TCS"},{"key":"54_CR23","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1145\/321356.321364","volume":"13","author":"R. Parikh","year":"1966","unstructured":"R. Parikh, On context-free languages, JACM, 13 (1966), pp. 570\u2013581.","journal-title":"JACM"},{"key":"54_CR24","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1109\/32.815324","volume":"2","author":"J. Rushby","year":"1999","unstructured":"J. Rushby, Systematic formal verification for fault-tolerant time-triggered algorithms, IEEE Trans. on Software Engineering, 2 (1999), pp. 651\u2013660.","journal-title":"IEEE Trans. on Software Engineering"},{"key":"54_CR25","first-page":"19","volume":"183","author":"M. Smith","year":"2000","unstructured":"M. Smith and N. Klarlund, Verification of a sliding window protocol using IOA and MONA, in FORTE\/PSTV\u201900, vol. 183 of IFIP Conf. Proc., 2000, pp. 19\u201334.","journal-title":"FORTE\/PSTV\u201900"},{"key":"54_CR26","volume-title":"The Complexity of Decision Problems in Automata Theory and Logic","author":"L. Stockmeyer","year":"1974","unstructured":"L. Stockmeyer, The Complexity of Decision Problems in Automata Theory and Logic, PhD thesis, Dept. of Electrical Engineering, MIT, Boston, Mass., 1974."},{"key":"54_CR27","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/978-3-642-59126-6_7","volume":"3","author":"W. Thomas","year":"1997","unstructured":"W. Thomas, Languages, automata, and logic, in Handbook of Formal Languages, vol. 3, Springer-Verlag, 1997, pp. 389\u2013455.","journal-title":"Handbook of Formal Languages"},{"key":"54_CR28","doi-asserted-by":"crossref","unstructured":"A. Wilk and A. Pnueli, Specification and verification of VLSI systems, in IC-CAD\u201989, 1989, pp. 460\u2013463.","DOI":"10.1109\/ICCAD.1989.76991"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45061-0_54","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,19]],"date-time":"2025-01-19T11:43:40Z","timestamp":1737287020000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45061-0_54"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540404934","9783540450610"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-45061-0_54","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2003]]}}}