{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T23:10:24Z","timestamp":1771024224977,"version":"3.50.1"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"3","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2005,7]]},"abstract":"<jats:p>This article considers finite-automata-based algorithms for handling linear arithmetic with both real and integer variables. Previous work has shown that this theory can be dealt with by using finite automata on infinite words, but this involves some difficult and delicate to implement algorithms. The contribution of this article is to show, using topological arguments, that only a restricted class of automata on infinite words are necessary for handling real and integer linear arithmetic. This allows the use of substantially simpler algorithms, which have been successfully implemented.<\/jats:p>","DOI":"10.1145\/1071596.1071601","type":"journal-article","created":{"date-parts":[[2005,8,3]],"date-time":"2005-08-03T08:30:55Z","timestamp":1123057855000},"page":"614-633","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":51,"title":["An effective decision procedure for linear arithmetic over the integers and reals"],"prefix":"10.1145","volume":"6","author":[{"given":"Bernard","family":"Boigelot","sequence":"first","affiliation":[{"name":"Universit\u00e9 de Li\u00e8ge, Li\u00e8ge, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S\u00e9bastien","family":"Jodogne","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Li\u00e8ge, Li\u00e8ge, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre","family":"Wolper","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Li\u00e8ge, Li\u00e8ge, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2005,7]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the 9th International Conference on Computer-Aided Verification. Lecture Notes in Computer Science","volume":"1254","author":"Boigelot B.","unstructured":"Boigelot , B. , Bronne , L. , and Rassart , S . 1997. An improved reachability analysis method for strongly linear hybrid systems . In Proceedings of the 9th International Conference on Computer-Aided Verification. Lecture Notes in Computer Science , vol. 1254 . Springer-Verlag, Berlin, Germany, 167--177.]] Boigelot, B., Bronne, L., and Rassart, S. 1997. An improved reachability analysis method for strongly linear hybrid systems. In Proceedings of the 9th International Conference on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 1254. Springer-Verlag, Berlin, Germany, 167--177.]]"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the International Joint Conference on Automated Reasoning (IJCAR). Lecture Notes in Computer Science","volume":"2083","author":"Boigelot B.","unstructured":"Boigelot , B. , Jodogne , S. , and Wolper , P . 2001. On the use of weak automata for deciding linear arithmetic with integer and real variables . In Proceedings of the International Joint Conference on Automated Reasoning (IJCAR). Lecture Notes in Computer Science , vol. 2083 . Springer-Verlag, Berlin, Germany, 611--625.]] Boigelot, B., Jodogne, S., and Wolper, P. 2001. On the use of weak automata for deciding linear arithmetic with integer and real variables. In Proceedings of the International Joint Conference on Automated Reasoning (IJCAR). Lecture Notes in Computer Science, vol. 2083. Springer-Verlag, Berlin, Germany, 611--625.]]"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the International Conference on Implementations and Applications of Automata. Lecture Notes in Computer Science","volume":"2494","author":"Boigelot B.","unstructured":"Boigelot , B. and Latour , L . 2001. Counting the solutions of Presburger equations without enumerating them . In Proceedings of the International Conference on Implementations and Applications of Automata. Lecture Notes in Computer Science , vol. 2494 . Springer-Verlag, Berlin, Germany, 40--51.]] Boigelot, B. and Latour, L. 2001. Counting the solutions of Presburger equations without enumerating them. In Proceedings of the International Conference on Implementations and Applications of Automata. Lecture Notes in Computer Science, vol. 2494. Springer-Verlag, Berlin, Germany, 40--51.]]"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the 25th Colloquium on Automata, Programming, and Languages (ICALP). Lecture Notes in Computer Science","volume":"1443","author":"Boigelot B.","unstructured":"Boigelot , B. , Rassart , S. , and Wolper , P . 1998. On the expressiveness of real and integer arithmetic automata . In Proceedings of the 25th Colloquium on Automata, Programming, and Languages (ICALP). Lecture Notes in Computer Science , vol. 1443 . Springer-Verlag, Berlin, Germany, 152--163.]] Boigelot, B., Rassart, S., and Wolper, P. 1998. On the expressiveness of real and integer arithmetic automata. In Proceedings of the 25th Colloquium on Automata, Programming, and Languages (ICALP). Lecture Notes in Computer Science, vol. 1443. Springer-Verlag, Berlin, Germany, 152--163.]]"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of CAAP'96","volume":"1059","author":"Boudet A.","unstructured":"Boudet , A. and Comon , H . 1996. Diophantine equations, Presburger arithmetic and finite automata . In Proceedings of CAAP'96 . Lecture Notes in Computer Science , vol. 1059 . Springer-Verlag, Berlin, Germany, 30--43.]] Boudet, A. and Comon, H. 1996. Diophantine equations, Presburger arithmetic and finite automata. In Proceedings of CAAP'96. Lecture Notes in Computer Science, vol. 1059. Springer-Verlag, Berlin, Germany, 30--43.]]"},{"key":"e_1_2_1_8_1","first-page":"2","article-title":"Logic and p-recognizable sets of integers","volume":"1","author":"Bruy\u00e8re V.","year":"1994","unstructured":"Bruy\u00e8re , V. , Hansel , G. , Michaux , C. , and Villemaire , R. 1994 . Logic and p-recognizable sets of integers . Bull. Belgian Math. Soc. 1 , 2 (Mar.), 191--238.]] Bruy\u00e8re, V., Hansel, G., Michaux, C., and Villemaire, R. 1994. Logic and p-recognizable sets of integers. Bull. Belgian Math. Soc. 1, 2 (Mar.), 191--238.]]","journal-title":"Bull. Belgian Math. Soc."},{"key":"e_1_2_1_9_1","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1002\/malq.19600060105","article-title":"Weak second-order arithmetic and finite automata","volume":"6","author":"B\u00fcchi J. R.","year":"1960","unstructured":"B\u00fcchi , J. R. 1960 . Weak second-order arithmetic and finite automata . Z. Math. Logik Grundl. Math. 6 , 66 -- 92 .]] B\u00fcchi, J. R. 1960. Weak second-order arithmetic and finite automata. Z. Math. Logik Grundl. Math. 6, 66--92.]]","journal-title":"Z. Math. Logik Grundl. Math."},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the International Congress on Logic, Method, and Philosophy of Science","author":"B\u00fcchi J. R.","year":"1962","unstructured":"B\u00fcchi , J. R. 1962 . On a decision method in restricted second order arithmetic . In Proceedings of the International Congress on Logic, Method, and Philosophy of Science . Stanford University Press, Stanford, CA, 1--12.]] B\u00fcchi, J. R. 1962. On a decision method in restricted second order arithmetic. In Proceedings of the International Congress on Logic, Method, and Philosophy of Science. Stanford University Press, Stanford, CA, 1--12.]]"},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the Seventh ACM Symposium on Principles of Database Systems. ACM Press","author":"Chomicki J.","unstructured":"Chomicki , J. and Imieli\u0144ski , T . 1988. Temporal deductive databases and infinite objects . In Proceedings of the Seventh ACM Symposium on Principles of Database Systems. ACM Press , New York, NY, 61--73.]] 10.1145\/308386.308416 Chomicki, J. and Imieli\u0144ski, T. 1988. Temporal deductive databases and infinite objects. In Proceedings of the Seventh ACM Symposium on Principles of Database Systems. ACM Press, New York, NY, 61--73.]] 10.1145\/308386.308416"},{"key":"e_1_2_1_12_1","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1007\/BF01746527","article-title":"On the base-dependence of sets of numbers recognizable by finite automata","volume":"3","author":"Cobham A.","year":"1969","unstructured":"Cobham , A. 1969 . On the base-dependence of sets of numbers recognizable by finite automata . Math. Syst. Theor. 3 , 186 -- 192 .]] Cobham, A. 1969. On the base-dependence of sets of numbers recognizable by finite automata. Math. Syst. Theor. 3, 186--192.]]","journal-title":"Math. Syst. Theor."},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the 2nd Workshop on Computer Aided Verification. Lecture Notes in Computer Science","volume":"531","author":"Courcoubetis C.","unstructured":"Courcoubetis , C. , Vardi , M. Y. , Wolper , P. , and Yannakakis , M . 1990. Memory efficient algorithms for the verification of temporal properties . In Proceedings of the 2nd Workshop on Computer Aided Verification. Lecture Notes in Computer Science , vol. 531 . Springer-Verlag, Berlin, Germany, 233--242.]] Courcoubetis, C., Vardi, M. Y., Wolper, P., and Yannakakis, M. 1990. Memory efficient algorithms for the verification of temporal properties. In Proceedings of the 2nd Workshop on Computer Aided Verification. Lecture Notes in Computer Science, vol. 531. Springer-Verlag, Berlin, Germany, 233--242.]]"},{"key":"e_1_2_1_14_1","volume-title":"The Computational Complexity of Logical Theories. Lecture Notes in Mathematics","volume":"718","author":"Ferrante J.","unstructured":"Ferrante , J. and Rackoff , C. W . 1979 . The Computational Complexity of Logical Theories. Lecture Notes in Mathematics , vol. 718 . Springer-Verlag, Berlin and Heidelberg, Germany\/New York, NY.]] Ferrante, J. and Rackoff, C. W. 1979. The Computational Complexity of Logical Theories. Lecture Notes in Mathematics, vol. 718. Springer-Verlag, Berlin and Heidelberg, Germany\/New York, NY.]]"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Hopcroft J. E. 1971. An n log n algorithm for minimizing states in a finite automaton. Theor. Mach. Computat. 189--196.]]  Hopcroft J. E. 1971. An n log n algorithm for minimizing states in a finite automaton. Theor. Mach. Computat. 189--196.]]","DOI":"10.1016\/B978-0-12-417750-5.50022-1"},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the 4th International Workshop on Implementing Automata (WIA'99)","volume":"2214","author":"J\u00fcrgensen H.","unstructured":"J\u00fcrgensen , H. and Staiger , L . 2001. Finite automata encoding geometric figures . In Proceedings of the 4th International Workshop on Implementing Automata (WIA'99) , Revised Papers, O. Boldt and H. J\u00fcrgensen, Eds. Lecture Notes in Computer Science , vol. 2214 . Springer-Verlag, Potsdam, Germany, 101--108.]] J\u00fcrgensen, H. and Staiger, L. 2001. Finite automata encoding geometric figures. In Proceedings of the 4th International Workshop on Implementing Automata (WIA'99), Revised Papers, O. Boldt and H. J\u00fcrgensen, Eds. Lecture Notes in Computer Science, vol. 2214. Springer-Verlag, Potsdam, Germany, 101--108.]]"},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the 9th ACM Symposium on Principles of Database Systems. ACM Press","author":"Kabanza F.","unstructured":"Kabanza , F. , St\u00e9venne , J.-M. , and Wolper , P . 1990. Handling infinite temporal data . In Proceedings of the 9th ACM Symposium on Principles of Database Systems. ACM Press , New York, NY, 392--403.]] 10.1145\/298514.298590 Kabanza, F., St\u00e9venne, J.-M., and Wolper, P. 1990. Handling infinite temporal data. In Proceedings of the 9th ACM Symposium on Principles of Database Systems. ACM Press, New York, NY, 392--403.]] 10.1145\/298514.298590"},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the 32nd IEEE Symposium on Foundations of Computer Science. IEEE Computer Society Press","author":"Klarlund N.","year":"1991","unstructured":"Klarlund , N. 1991 . Progress measures for complementation of \u03c9-automata with applications to temporal logic . In Proceedings of the 32nd IEEE Symposium on Foundations of Computer Science. IEEE Computer Society Press , Los Alamitos, CA, 358--367.]] 10.1109\/SFCS. 1991.185391 Klarlund, N. 1991. Progress measures for complementation of \u03c9-automata with applications to temporal logic. In Proceedings of the 32nd IEEE Symposium on Foundations of Computer Science. IEEE Computer Society Press, Los Alamitos, CA, 358--367.]] 10.1109\/SFCS.1991.185391"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the 5th Israeli Symposium on Theory of Computing and Systems. IEEE Computer Society Press","author":"Kupferman O.","unstructured":"Kupferman , O. and Vardi , M . 1997. Weak alternating automata are not that weak . In Proceedings of the 5th Israeli Symposium on Theory of Computing and Systems. IEEE Computer Society Press , Los Alamitos, CA, 147--158.]] Kupferman, O. and Vardi, M. 1997. Weak alternating automata are not that weak. In Proceedings of the 5th Israeli Symposium on Theory of Computing and Systems. IEEE Computer Society Press, Los Alamitos, CA, 147--158.]]"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333987"},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","first-page":"376","DOI":"10.1007\/BF01691063","article-title":"Decision problems for \u03c9-automata","volume":"3","author":"Landweber L. H.","year":"1969","unstructured":"Landweber , L. H. 1969 . Decision problems for \u03c9-automata . Math. Syst. Theor. 3 , 4, 376 -- 384 .]] Landweber, L. H. 1969. Decision problems for \u03c9-automata. Math. Syst. Theor. 3, 4, 376--384.]]","journal-title":"Math. Syst. Theor."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(00)00183-6"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00312-X"},{"key":"e_1_2_1_25_1","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1016\/0304-3975(84)90049-5","article-title":"Alternating finite automata on \u03c9-words","volume":"32","author":"Miyano S.","year":"1984","unstructured":"Miyano , S. and Hayashi , T. 1984 . Alternating finite automata on \u03c9-words . Theoret. Comput. Sci. 32 , 321 -- 330 .]] Miyano, S. and Hayashi, T. 1984. Alternating finite automata on \u03c9-words. Theoret. Comput. Sci. 32, 321--330.]]","journal-title":"Theoret. Comput. Sci."},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of the 13th International Colloquium on Automata, Languages and Programming. Springer-Verlag","author":"Muller D. E.","unstructured":"Muller , D. E. , Saoudi , A. , and Schupp , P. E . 1986. Alternating automata, the weak monadic theory of the tree and its complexity . In Proceedings of the 13th International Colloquium on Automata, Languages and Programming. Springer-Verlag , Berlin, Germany, 275--283.]] Muller, D. E., Saoudi, A., and Schupp, P. E. 1986. Alternating automata, the weak monadic theory of the tree and its complexity. In Proceedings of the 13th International Colloquium on Automata, Languages and Programming. Springer-Verlag, Berlin, Germany, 275--283.]]"},{"key":"e_1_2_1_27_1","first-page":"1","article-title":"Decidability of second order theories and automata on infinite trees","volume":"141","author":"Rabin M. O.","year":"1969","unstructured":"Rabin , M. O. 1969 . Decidability of second order theories and automata on infinite trees . Trans. AMS 141 , 1 -- 35 .]] Rabin, M. O. 1969. Decidability of second order theories and automata on infinite trees. Trans. AMS 141, 1--35.]]","journal-title":"Trans. AMS"},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the 29th IEEE Symposium on Foundations of Computer Science. IEEE Computer Society Press","author":"Safra S.","year":"1988","unstructured":"Safra , S. 1988 . On the complexity of omega-automata . In Proceedings of the 29th IEEE Symposium on Foundations of Computer Science. IEEE Computer Society Press , Los Alamitos, CA, 319--327.]] Safra, S. 1988. On the complexity of omega-automata. In Proceedings of the 29th IEEE Symposium on Foundations of Computer Science. IEEE Computer Society Press, Los Alamitos, CA, 319--327.]]"},{"key":"e_1_2_1_29_1","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1007\/BF00967164","article-title":"Presburgerness of predicates regular in two number systems","volume":"18","author":"Semenov A. L.","year":"1977","unstructured":"Semenov , A. L. 1977 . Presburgerness of predicates regular in two number systems . Siberian Math. J. 18 , 289 -- 299 .]] Semenov, A. L. 1977. Presburgerness of predicates regular in two number systems. Siberian Math. J. 18, 289--299.]]","journal-title":"Siberian Math. J."},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the 10th International Conference on Computer-Aided Verification. Lecture Notes in Computer Science","volume":"1427","author":"Shiple T. R.","unstructured":"Shiple , T. R. , Kukula , J. H. , and Ranjan , R. K . 1998. A comparison of Presburger engines for EFSM reachability . In Proceedings of the 10th International Conference on Computer-Aided Verification. Lecture Notes in Computer Science , vol. 1427 . Springer-Verlag, Berlin, Germany, 280--292.]] Shiple, T. R., Kukula, J. H., and Ranjan, R. K. 1998. A comparison of Presburger engines for EFSM reachability. In Proceedings of the 10th International Conference on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 1427. Springer-Verlag, Berlin, Germany, 280--292.]]"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90008-9"},{"key":"e_1_2_1_32_1","doi-asserted-by":"crossref","first-page":"434","DOI":"10.1016\/0022-0000(83)90051-X","article-title":"Finite-state \u03c9-languages","volume":"27","author":"Staiger L.","year":"1983","unstructured":"Staiger , L. 1983 . Finite-state \u03c9-languages . J. Comput. Syst. Sci. 27 , 3, 434 -- 448 .]] Staiger, L. 1983. Finite-state \u03c9-languages. J. Comput. Syst. Sci. 27, 3, 434--448.]]","journal-title":"J. Comput. Syst. Sci."},{"key":"e_1_2_1_33_1","first-page":"379","article-title":"Automaten theoretische und automatenfreie charakterisierungen topologischer klassen regul\u00e4rer folgenmengen","volume":"10","author":"Staiger L.","year":"1974","unstructured":"Staiger , L. and Wagner , K. 1974 . Automaten theoretische und automatenfreie charakterisierungen topologischer klassen regul\u00e4rer folgenmengen . Elektron. Informationsverarbeitung und Kybernetik EIK 10 , 379 -- 392 .]] Staiger, L. and Wagner, K. 1974. Automaten theoretische und automatenfreie charakterisierungen topologischer klassen regul\u00e4rer folgenmengen. Elektron. Informationsverarbeitung und Kybernetik EIK 10, 379--392.]]","journal-title":"Elektron. Informationsverarbeitung und Kybernetik EIK"},{"key":"e_1_2_1_34_1","first-page":"133","article-title":"Automata on infinite objects. In Handbook of Theoretical Computer Science---Volume B: Formal Models and Semantics, J. Van Leeuwen, Ed. Elsevier, Amsterdam, The Netherlands","volume":"4","author":"Thomas W.","year":"1990","unstructured":"Thomas , W. 1990 . Automata on infinite objects. In Handbook of Theoretical Computer Science---Volume B: Formal Models and Semantics, J. Van Leeuwen, Ed. Elsevier, Amsterdam, The Netherlands , Chapter 4 , 133 -- 191 .]] Thomas, W. 1990. Automata on infinite objects. In Handbook of Theoretical Computer Science---Volume B: Formal Models and Semantics, J. Van Leeuwen, Ed. Elsevier, Amsterdam, The Netherlands, Chapter 4, 133--191.]]","journal-title":"Chapter"},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of the First Symposium on Logic in Computer Science. IEEE Computer Society Press","author":"Vardi M. Y.","unstructured":"Vardi , M. Y. and Wolper , P . 1986a. An automata-theoretic approach to automatic program verification . In Proceedings of the First Symposium on Logic in Computer Science. IEEE Computer Society Press , Los Alamitos, CA, 322--331.]] Vardi, M. Y. and Wolper, P. 1986a. An automata-theoretic approach to automatic program verification. In Proceedings of the First Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, CA, 322--331.]]"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(86)90026-7"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1092"},{"key":"e_1_2_1_38_1","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1016\/S0019-9958(79)90653-3","article-title":"On \u03c9-regular sets","volume":"43","author":"Wagner K.","year":"1979","unstructured":"Wagner , K. 1979 . On \u03c9-regular sets . Inform. Contr. 43 , 2 (Nov.), 123--177.]] Wagner, K. 1979. On \u03c9-regular sets. Inform. Contr. 43, 2 (Nov.), 123--177.]]","journal-title":"Inform. Contr."},{"key":"e_1_2_1_39_1","volume-title":"ISSAC: Proceedings of the ACM SIGSAM International Symposium on Symbolic and Algebraic Computation. ACM Press","author":"Weispfenning V.","year":"1999","unstructured":"Weispfenning , V. 1999 . Mixed real-integer linear quantifier elimination . In ISSAC: Proceedings of the ACM SIGSAM International Symposium on Symbolic and Algebraic Computation. ACM Press , New York, NY, 129--136.]] 10.1145\/309831.309888 Weispfenning, V. 1999. Mixed real-integer linear quantifier elimination. In ISSAC: Proceedings of the ACM SIGSAM International Symposium on Symbolic and Algebraic Computation. ACM Press, New York, NY, 129--136.]] 10.1145\/309831.309888"},{"key":"e_1_2_1_40_1","volume-title":"Proceedings of the Static Analysis Symposium. Lecture Notes in Computer Science","volume":"983","author":"Wolper P.","unstructured":"Wolper , P. and Boigelot , B . 1995. An automata-theoretic approach to Presburger arithmetic constraints . In Proceedings of the Static Analysis Symposium. Lecture Notes in Computer Science , vol. 983 . Springer-Verlag, Berlin, Germany, 21--32.]] Wolper, P. and Boigelot, B. 1995. An automata-theoretic approach to Presburger arithmetic constraints. In Proceedings of the Static Analysis Symposium. Lecture Notes in Computer Science, vol. 983. Springer-Verlag, Berlin, Germany, 21--32.]]"},{"key":"e_1_2_1_41_1","volume-title":"Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science","volume":"1785","author":"Wolper P.","unstructured":"Wolper , P. and Boigelot , B . 2000. On the construction of automata from linear arithmetic constraints . In Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science , vol. 1785 . Springer-Verlag, Berlin, Germany, 1--19.]] Wolper, P. and Boigelot, B. 2000. On the construction of automata from linear arithmetic constraints. In Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 1785. Springer-Verlag, Berlin, Germany, 1--19.]]"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1071596.1071601","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T13:59:58Z","timestamp":1672235998000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1071596.1071601"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,7]]},"references-count":40,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2005,7]]}},"alternative-id":["10.1145\/1071596.1071601"],"URL":"https:\/\/doi.org\/10.1145\/1071596.1071601","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,7]]},"assertion":[{"value":"2005-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}