An effective decision procedure for linear arithmetic over the integers and reals

Boigelot, Bernard; Jodogne, Sébastien; Wolper, Pierre

doi:10.1145/1071596.1071601

Download

Article (Scientific journals)

An effective decision procedure for linear arithmetic over the integers and reals

Boigelot, Bernard; Jodogne, Sébastien; Wolper, Pierre

2005 • In ACM Transactions on Computational Logic, 6 (3), p. 614-633

Peer Reviewed verified by ORBi

Permalink
https://hdl.handle.net/2268/12428

DOI
10.1145/1071596.1071601

Files (1)Send to Details Statistics Bibliography Similar publications

Files

Full Text

BJW05.pdf

Author postprint (218.05 kB)

Download

All documents in ORBi are protected by a user license.

Send to

RIS BibTex APA Chicago Permalink X Linkedin

Details

Keywords :

Decision procedure; finite-state representations; integer and real arithmetic; weak ω-automata

Abstract :

[en] 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.

Disciplines :

Computer science

Author, co-author :

Boigelot, Bernard ; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique

Jodogne, Sébastien ; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique

Wolper, Pierre ; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique (parallélisme et banques de données)

Language :

English

Title :

An effective decision procedure for linear arithmetic over the integers and reals

Publication date :

2005

Journal title :

ACM Transactions on Computational Logic

ISSN :

1529-3785

Publisher :

ACM, New-York, United States

Volume :

Issue :

Pages :

614-633

Peer reviewed :

Peer Reviewed verified by ORBi

Commentary :

© ACM, 2005. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Transactions on Computional Logic {VOL 6, ISS 3, (July 2005} http://doi.acm.org/10.1145/1071596.1071601

Available on ORBi :

since 07 May 2009

Statistics

Number of views

155 (22 by ULiège)

Number of downloads

501 (12 by ULiège)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenCitations

OpenAlex citations

Bibliography

ALUR, R., COURCOUBETIS, C., HALBWACHS, N., HENZINGER, T. A., HO, P. H., NICOLLIN, X., OLIVERO, A., SIFAKIS, J., AND YOVINE, S. 1995. The algorithmic analysis of hybrid systems. Theoret. Comput. Sci. 138, 1 (Feb.), 3-34.
BOIGELOT, B. 1998. Symbolic methods for exploring infinite state spaces. Ph.D. dissertation. Université de Liège, Liège, Belgium.
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., 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. 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., 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.
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.
BRUYÈRE, 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.
BÜCHI, J. R. 1960. Weak second-order arithmetic and finite automata. Z. Math. Logik Grundl. Math. 6, 66-92.
BÜCHI, 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.
CHOMICKI, J. AND IMIELIŃSKI, 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.
COBHAM, A. 1969. On the base-dependence of sets of numbers recognizable by finite automata. Math. Syst. Theor. 3, 186-192.
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.
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.
HOLZMANN, G. J. 1997. The model checker SPIN. IEEE Trans. Softw. Eng. 23, 5 (May), 279-295. (Special issue on Formal Methods in Software Practice).
HOPCROFT, J. E. 1971. An n log n algorithm for minimizing states in a finite automaton. Theor. Mach. Computat. 189-196.
JÜRGENSEN, 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ürgensen, Eds. Lecture Notes in Computer Science, vol. 2214. Springer-Verlag, Potsdam, Germany, 101-108.
KABANZA, F., STÉVENNE, 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.
KLARLUND, N. 1991. Progress measures for complementation of ω-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.
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., VARDI, M. Y., AND WOLPER, P. 2000. An automata-theoretic approach to branching-time model checking. J. ACM 47, 2 (Mar.), 312-360.
LANDWEBER, L. H. 1969. Decision problems for ω-automata. Math. Syst. Theor. 3, 4, 376-384.
LöDING, C. 2001. Efficient minimization of deterministic weak ω-automata. Informat. Process. Lett. 79, 3, 105-109.
MALER, O. AND STAIGER, L. 1997. On syntactic congruences for ω-languages. Theoret. Comput. Sci. 183,1, 93-112.
MIYANO, S. AND HAYASHI, T. 1984. Alternating finite automata on ω-words. Theoret. Comput. Sci. 32, 321-330.
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.
RABIN, M. O. 1969. Decidability of second order theories and automata on infinite trees. Trans. AMS 141, 1-35.
SAFEA, 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.
SEMENOV, A. L. 1977. Presburgerness of predicates regular in two number systems. Siberian Math. J. 18, 289-299.
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-faded Verification. Lecture Notes in Computer Science, vol. 1427. Springer-Verlag, Berlin, Germany, 280-292.
SISTLA, A. P., VARDI, M. Y., AND WOLPER, P. 1987. The complementation problem for Büchi automata with applications to temporal logic. Theoret. Comput. Sci. 49, 217-237.
STAIGER, L. 1983. Finite-state ω-languages. J. Comput. Syst. Sci. 27, 3, 434-448.
STAIGER, L. AND WAGNER, K. 1974. Automaten theoretische und automatenfreie Charakterisierungen topologischer klassen regulärer folgenmengen. Elektron. Informationsverarbeitung und Kybernetik EIK 10, 379-392.
THOMAS, W. 1990. Automata on 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.
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. 1986b. Automata-theoretic techniques or modal logics of programs. J. Comput. Syst. Sci. 32, 2 (Apr.), 183-221.
VARDI, M. Y. AND WOLPER, P. 1994. Reasoning about infinite computations. Inform. Computat. 115, 1 (Nov.), 1-37.
WAGNER, K. 1979. On omega-regular sets. Inform. Contr. 43, 2 (Nov.), 123-177.
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.
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. 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.