Representing arithmetic constraints with finite automata: An overview

Boigelot, Bernard; Wolper, Pierre

doi:10.1007/3-540-45619-8_1

Request a copy

Paper published in a journal (Scientific congresses and symposiums)

Representing arithmetic constraints with finite automata: An overview

Boigelot, Bernard; Wolper, Pierre

2002 • In Lecture Notes in Computer Science, 2401

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

DOI
10.1007/3-540-45619-8_1

Files (2)Send to Details Statistics Bibliography Similar publications

Files

Full Text

BW03-iclp.pdf

Publisher postprint (319.3 kB)

Request a copy

Full Text Parts

BW02-iclp.pdf

Author postprint (273.57 kB)

Download

The original publication is available at www.springerlink.com

All documents in ORBi are protected by a user license.

Send to

RIS BibTex APA Chicago Permalink X Linkedin

Details

Keywords :

arithmetic; automata; Presburger

Abstract :

[en] Linear numerical constraints and their first-order theory, whether defined over the reals or the. integers, are basic tools that appear in many areas of Computer Science. This paper overviews a set of techniques based on finite automata that lead to decision procedures and other useful algorithms, as well as to a normal form, for the first-order linear theory of the integers, of the reals, and of the integers and reals combined. This approach has led to an implemented tool, which has the so far unique capability of handling the linear. first-order theory of the integers and reals combined.

Disciplines :

Computer science

Author, co-author :

Boigelot, Bernard ; 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 :

Representing arithmetic constraints with finite automata: An overview

Publication date :

July 2002

Event name :

18th International Conference on Logic Programming

Event organizer :

U Roskilde, Denmark

Event place :

Copenhagen, Denmark

Event date :

July 27th to August 1st 2002

By request :

Yes

Audience :

International

Journal title :

Lecture Notes in Computer Science

ISSN :

0302-9743

eISSN :

1611-3349

Publisher :

Springer-Verlag Berlin, Berlin, Germany

Special issue title :

Logics Programming, Proceedings

Volume :

2401

Funders :

Communauté française de Belgique - Direction de la recherche scientifique - Actions de recherche concertées
European IST-FET project ADVANCE (IST-1999-29082)

Available on ORBi :

since 14 August 2009

Statistics

Number of views

105 (11 by ULiège)

Number of downloads

310 (4 by ULiège)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenCitations

OpenAlex citations

Bibliography

[BBR97] 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-178, Haifa, June 1997. Springer-Verlag.
[BC96] A. Boudet and H. Comon. Diophantine equations, Presburger arithmetic and finite automata. In Proceedings of CAAP'96, number 1059 in Lecture Notes in Computer Science, pages 30-43. Springer-Verlag, 1996.
[BCM+90] J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the 5th Symposium on Logic in Computer Science, pages 428-439, Philadelphia, June 1990.
[BJW01] Bernard Boigelot, Sebastien Jodogne, and Pierre Wolper. On the use of weak automata for deciding linear arithmetic with integer and real variables. In Proc. International Joint Conference on Automated Reasoning (IJCAR), volume 2083 of Lecture Notes in Computer Science, pages 611- 625, Siena, June 2001. Springer-Verlag.
[BL01] B. Boigelot and L. Latour. Counting the solutions of Presburger equations without enumerating them. In Proc. International Conference on Implementations and Applications of Automata, Lecture Notes in Computer Science, Pretoria, South Africa, July 2001. Springer-Verlag. To appear.
[Boi98] B. Boigelot. Symbolic Methods for Exploring Infinite State Spaces. PhD thesis, Universite de Liege, 1998.
[BRW98] Bernard Boigelot, Stephane 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-163. Springer-Verlag, July 1998.
[Bry86] R. E. Bryant. Graph based algorithms for boolean function manipulation. IEEE Transactions on Computers, 35(8):677-691, 1986.
[Buc60] J. R. Buchi. Weak second-order arithmetic and finite automata. Zeitschrift Math. Logik und Grundlagen der Mathematik, 6:66-92, 1960.
[BW94] Bernard Boigelot and Pierre Wolper. Symbolic verification with periodic sets. In Computer Aided Verification, Proc. 6th Int. Conference, volume 818 of Lecture Notes in Computer Science, pages 55-67, Stanford, California, June 1994. Springer-Verlag.
[Hop71] J. E. Hopcroft. An n log n algorithm for minimizing states in a finite automaton. Theory of Machines and Computation, pages 189-196, 1971.
[KV97] 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-158. IEEE Computer Society Press, 1997.
[LAS] The Liege Automata-based Symbolic Handler (LASH). Available at http://www.montefiore.ulg.ac.be/~boigelot/research/lash/.
[Lod01] C. Loding. Efficient minimization of deterministic weak ω-automata, 2001. Submitted for publication.
[MH84] S. Miyano and T. Hayashi. Alternating finite automata on ω-words. Theoretical Computer Science, 32:321-330, 1984.
[MS97] O. Maler and L. Staiger. On syntactic congruences for ω-languages. Theoretical Computer Science, 183(1):93-112, 1997.
[MSS86] 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.
[Pug92] W. Pugh. A practical algorithm for exact array dependency analysis. Comm. of the ACM, 35(8):102, August 1992.
[Sta83] L. Staiger. Finite-state ω-languages. Journal of Computer and System Sciences, 27(3):434-448, 1983.
[Tho90] 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-191. Elsevier, Amsterdam, 1990.
[WB95] Pierre Wolper and Bernard Boigelot. An automata-theoretic approach to Presburger arithmetic constraints. In Proc. Static Analysis Symposium, volume 983 of Lecture Notes in Computer Science, pages 21-32, Glasgow, September 1995. Springer-Verlag.
[WB98] Pierre Wolper and Bernard Boigelot. Verifying systems with infinite but regular state spaces. In Proc. 10th Int. Conf. on Computer Aided Verification, volume 1427 of Lecture Notes in Computer Science, pages 88-97, Vancouver, July 1998. Springer-Verlag.
[WB00] 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-19, Berlin, March 2000. Springer-Verlag.