{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T23:40:17Z","timestamp":1737502817399,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540422549"},{"type":"electronic","value":"9783540457442"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45744-5_50","type":"book-chapter","created":{"date-parts":[[2007,10,26]],"date-time":"2007-10-26T21:02:07Z","timestamp":1193432527000},"page":"611-625","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":20,"title":["On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables"],"prefix":"10.1007","author":[{"given":"Bernard","family":"Boigelot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S\u00e9bastien","family":"Jodogne","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre","family":"Wolper","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,6,8]]},"reference":[{"key":"50_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/3-540-63166-6_18","volume-title":"Proc. 9th Int. Conf.on Computer Aided Verification","author":"B. Boigelot","year":"1997","unstructured":"B. Boigelot, L. Bronne, and S. Rassart. An improved reachability analysis method for strongly linear hybrid systems. In Proc. 9th Int. Conf.on Computer Aided Verification, volume 1254 of Lecture Notes in Computer Science, pages 167\u2013178, Haifa, June 1997. Springer-Verlag."},{"key":"50_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1007\/3-540-61064-2_27","volume-title":"Proceedings of CAAP\u201996","author":"A. Boudet","year":"1996","unstructured":"A. Boudet and H. Comon. Diophantine equations, Presburger arithmetic and finite automata. In Proceedings of CAAP\u201996, number 1059 in Lecture Notes in Computer Science, pages 30\u201343. Springer-Verlag, 1996."},{"issue":"2","key":"50_CR3","doi-asserted-by":"crossref","first-page":"191","DOI":"10.36045\/bbms\/1103408547","volume":"1","author":"V. Bruy\u00e8re","year":"1994","unstructured":"V. Bruy\u00e8re, G. Hansel, C. Michaux, and R. Villemaire. Logic and p-recognizable sets of integers. Bulletin of the Belgian Mathematical Society, 1(2):191\u2013238, March 1994.","journal-title":"Bulletin of the Belgian Mathematical Society"},{"key":"50_CR4","unstructured":"B. Boigelot. Symbolic Methods for Exploring Infinite State Spaces. PhD thesis, Universit\u00e9e de Universit\u00e8e, 1998."},{"key":"50_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/BFb0055049","volume-title":"Proc. 25th Colloq. on Automata, Programming, and Languages (ICALP)","author":"B. Boigelot","year":"1998","unstructured":"Bernard Boigelot, St\u00e9ephane Rassart, and Pierre Wolper. On the expressiveness of real and integer arithmetic automata. In Proc. 25th Colloq. on Automata, Programming, and Languages (ICALP), volume 1443 of Lecture Notes in Computer Science, pages 152\u2013163. Springer-Verlag, July 1998."},{"key":"50_CR6","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1002\/malq.19600060105","volume":"6","author":"J. R. B\u00fcchi","year":"1960","unstructured":"J. R. B\u00fcchi. Weak second-order arithmetic and finite automata. Zeitschrift Math. Logik und Grundlagen der Mathematik, 6:66\u201392, 1960.","journal-title":"Zeitschrift Math. Logik und Grundlagen der Mathematik"},{"key":"50_CR7","unstructured":"J.R. B\u00fcchi. On a decision method in restricted second order arithmetic. In Proc. Internat. Congr. Logic, Method and Philos. Sci. 1960, pages 1\u201312, Stanford, 1962. Stanford University Press."},{"key":"50_CR8","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1007\/BF01746527","volume":"3","author":"A. Cobham","year":"1969","unstructured":"A. Cobham. On the base-dependence of sets of numbers recognizable by finite automata. Mathematical Systems Theory, 3:186\u2013192, 1969.","journal-title":"Mathematical Systems Theory"},{"key":"50_CR9","series-title":"Lect Notes Comput Sci","first-page":"233","volume-title":"Proc. 2nd Workshop on Computer Aided Verification","author":"C. Courcoubetis","year":"1990","unstructured":"Constantin Courcoubetis, Moshe Y. Vardi, Pierre Wolper, and Mihalis Yannakakis. Memory efficient algorithms for the verification of temporal properties. In Proc. 2nd Workshop on Computer Aided Verification, volume 531 of Lecture Notes in Computer Science, pages 233\u2013242, Rutgers, June 1990. Springer-Verlag."},{"key":"50_CR10","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0062837","volume-title":"The Computational Complexity of Logical Theories","author":"J. Ferrante","year":"1979","unstructured":"J. Ferrante and C. W. Rackoff. The Computational Complexity of Logical Theories, volume 718 of Lecture Notes in Mathematics. Springer-Verlag, Berlin-Heidelberg-New York, 1979."},{"issue":"5","key":"50_CR11","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. J. Holzmann","year":"1997","unstructured":"Gerard J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279\u2013295, May 1997. Special Issue: Formal Methods in Software Practice.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"50_CR12","unstructured":"N. Klarlund. Progress measures for complementation of \u03c9-automata with applications to temporal logic. In Proceedings of the 32nd IEEE Symposium on Foundations of Computer Science, San Juan, October 1991."},{"key":"50_CR13","doi-asserted-by":"crossref","unstructured":"O. Kupferman and M. Vardi. Weak alternating automata are not that weak. In Proc. 5th Israeli Symposium on Theory of Computing and Systems, pages 147\u2013158. IEEE Computer Society Press, 1997.","DOI":"10.1109\/ISTCS.1997.595167"},{"issue":"2","key":"50_CR14","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O. Kupferman","year":"2000","unstructured":"Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. An automata-theoretic approach to branching-time model checking. Journal of the ACM, 47(2):312\u2013360, March 2000.","journal-title":"Journal of the ACM"},{"key":"50_CR15","unstructured":"The Universit\u00e8e Automata-based Symbolic Handler (LASH). Available at http:\/\/www.montefiore.ulg.ac.be\/~boigelot\/research\/lash\/ ."},{"key":"50_CR16","doi-asserted-by":"crossref","unstructured":"C. L\u00f6ding. Efficient minimization of deterministic weak \u03c9-automata, 2001. Submitted for publication.","DOI":"10.1016\/S0020-0190(00)00183-6"},{"key":"50_CR17","first-page":"321","volume":"32","author":"S. Miyano","year":"1984","unstructured":"S. Miyano and T. Hayashi. Alternating finite automata on \u03c9-words. The-oretical Computer Science, 32:321\u2013330, 1984.","journal-title":"The-oretical Computer Science"},{"issue":"1","key":"50_CR18","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/S0304-3975(96)00312-X","volume":"183","author":"O. Maler","year":"1997","unstructured":"O. Maler and L. Staiger. On syntactic congruences for \u03c9-languages. The-oretical Computer Science, 183(1):93\u2013112, 1997.","journal-title":"The-oretical Computer Scienc"},{"key":"50_CR19","doi-asserted-by":"crossref","unstructured":"D.E. Muller, A. Saoudi, and P.E. Schupp. Alternating automata, the weak monadic theory of the tree and its complexity. In Proc. 13th Int. Colloquium on Automata, Languages and Programming. Springer-Verlag, 1986.","DOI":"10.1007\/3-540-16761-7_77"},{"key":"50_CR20","first-page":"1","volume":"141","author":"M.O. Rabin","year":"1969","unstructured":"M.O. Rabin. Decidability of second order theories and automata on infinite trees. Transaction of the AMS, 141:1\u201335, 1969.","journal-title":"Transaction of the AMS"},{"key":"50_CR21","doi-asserted-by":"crossref","unstructured":"S. Safra. On the complexity of omega-automata. In Proceedings of the 29th IEEE Symposium on Foundations of Computer Science, White Plains, October 1988.","DOI":"10.1109\/SFCS.1988.21948"},{"key":"50_CR22","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/BF00967164","volume":"18","author":"A. L. Semenov","year":"1977","unstructured":"A. L. Semenov. Presburgerness of predicates regular in two number systems. Siberian Mathematical Journal, 18:289\u2013299, 1977.","journal-title":"Siberian Mathematical Journal"},{"key":"50_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/BFb0028752","volume-title":"Proceedings of the 10th Intl. Conf. on Computer-Aided Verification","author":"T. R. Shiple","year":"1998","unstructured":"T. R. Shiple, J. H. Kukula, and R. K. Ranjan. A comparison of Presburger engines for EFSM reachability. In Proceedings of the 10th Intl. Conf. on Computer-Aided Verification, volume 1427 of Lecture Notes in Computer Science, pages 280\u2013292, Vancouver, June\/July 1998. Springer-Verlag."},{"issue":"3","key":"50_CR24","doi-asserted-by":"publisher","first-page":"434","DOI":"10.1016\/0022-0000(83)90051-X","volume":"27","author":"L. Staiger","year":"1983","unstructured":"L. Staiger. Finite-state \u03c9-languages. Journal of Computer and System Sciences, 27(3):434\u2013448, 1983.","journal-title":"Journal of Computer and System Sciences"},{"key":"50_CR25","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"A. P. Sistla","year":"1987","unstructured":"A. Prasad Sistla, Moshe Y. Vardi, and Pierre Wolper. The complementation problem for B\u00fcchi automata with applications to temporal logic. Theoretical Computer Science, 49:217\u2013237, 1987.","journal-title":"Theoretical Computer Science"},{"key":"50_CR26","first-page":"379","volume":"10","author":"L. Staiger","year":"1974","unstructured":"L. Staiger and K. Wagner. Automatentheoretische und automatenfreie Charakterisierungen topologischer Klassen regul\u00e4rer Folgenmengen. Elektron. Informationsverarbeitung und Kybernetik EIK, 10:379\u2013392, 1974.","journal-title":"Elektron. Informationsverarbeitung und Kybernetik EIK"},{"key":"50_CR27","doi-asserted-by":"crossref","unstructured":"Wolfgang Thomas. Automata on infinite objects. In J. Van Leeuwen, editor, Handbook of Theoretical Computer Science-Volume B: Formal Models and Semantics, chapter 4, pages 133\u2013191. Elsevier, Amsterdam, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"50_CR28","unstructured":"Moshe Y. Vardi and Pierre Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First Symposium on Logic in Computer Science, pages 322\u2013331, Cambridge, June 1986."},{"issue":"2","key":"50_CR29","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0022-0000(86)90026-7","volume":"32","author":"M. Y. Vardi","year":"1986","unstructured":"Moshe Y. Vardi and Pierre Wolper. Automata-theoretic techniques for modal logics of programs. Journal of Computer and System Science, 32(2):183\u2013221, April 1986.","journal-title":"Journal of Computer and System Science"},{"issue":"1","key":"50_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M. Y. Vardi","year":"1994","unstructured":"Moshe Y. Vardi and Pierre Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1\u201337, November 1994.","journal-title":"Information and Computation"},{"key":"50_CR31","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-46419-0_1","volume-title":"Proc. 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Wolper","year":"2000","unstructured":"Pierre Wolper and Bernard Boigelot. On the construction of automata from linear arithmetic constraints. In Proc. 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 1785 of Lecture Notes in Computer Science, pages 1\u201319, Berlin, March 2000. Springer-Verlag."}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45744-5_50","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T23:10:14Z","timestamp":1737501014000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45744-5_50"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540422549","9783540457442"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/3-540-45744-5_50","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2001]]},"assertion":[{"value":"8 June 2001","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}