On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables

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

doi:10.1007/3-540-45744-5_50

Download

Paper published in a journal (Scientific congresses and symposiums)

On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables

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

2001 • In Lecture Notes in Computer Science, 2083, p. 611-625

Peer reviewed

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

DOI
10.1007/3-540-45744-5_50

Files (1)Send to Details Statistics Bibliography Similar publications

Files

Full Text

BJW01-ijcar.pdf

Author postprint (181.4 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 :

Presburger Arithmetic; Automata; reals; integers

Abstract :

[en] This paper 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 in finite words, but this involves some difficult and delicate to implement algorithms. The contribution of this paper is to show, using topological arguments, that only a restricted class of automata on in finite words are necessary for handling real and integer linear arithmetic. This allows the use of substantially simpler algorithms and opens the path to the implementation of a usable system for handling this combined theory.

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épartement d'Electricité, Electronique et Informatique > 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 :

On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables

Publication date :

2001

Event name :

First International Joint Conference on Automated Reasoning (IJCAR)

Event place :

Siana, Italy

Event date :

June 18–22 2001

Audience :

International

Journal title :

Lecture Notes in Computer Science

ISSN :

0302-9743

eISSN :

1611-3349

Publisher :

Springer, Berlin, Germany

Volume :

2083

Pages :

611-625

Peer reviewed :

Peer reviewed

Funders :

Communauté française de Belgique - Direction de la recherche scienti que - Actions de recherche concertées

Available on ORBi :

since 04 September 2009

Statistics

Number of views

90 (11 by ULiège)

Number of downloads

236 (4 by ULiège)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenCitations

Bibliography

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.
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.
V. Bruyère, G. Hansel, C. Michaux, and R. Villemaire. Logic and p-recognizable sets of integers. Bulletin of the Belgian Mathematical Society, 1(2):191-238, March 1994.
B. Boigelot. Symbolic Methods for Exploring Infinite State Spaces. PhD thesis, Université de Liège, 1998.
Bernard Boigelot, Stéphane 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.
J. R. Büchi. Weak second-order arithmetic and finite automata. Zeitschrift Math. Logik und Grundlagen der Mathematik, 6:66-92, 1960.
J.R. Büchi. On a decision method in restricted second order arithmetic. In Proc. Internat. Congr. Logic, Method and Philos. Sci. 1960, pages 1-12, Stanford, 1962. Stanford University Press.
A. Cobham. On the base-dependence of sets of numbers recognizable by finite automata. Mathematical Systems Theory, 3:186-192, 1969.
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-242, Rutgers, June 1990. Springer-Verlag.
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.
Gerard J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279-295, May 1997. Special Issue: Formal Methods in Software Practice.
N. Klarlund. Progress measures for complementation of ω-automata with applications to temporal logic. In Proceedings of the 32nd IEEE Symposium on Foundations of Computer Science, San Juan, October 1991.
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.
Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. An automatatheoretic approach to branching-time model checking. Journal of the ACM, 47(2):312-360, March 2000.
The Liège Automata-based Symbolic Handler (LASH). Available at http://www.montefiore.ulg.ac.be/~boigelot/research/lash/.
C. Löding. Efficient minimization of deterministic weak ω-automata, 2001. Submitted for publication.
S. Miyano and T. Hayashi. Alternating finite automata on ω-words. Theoretical Computer Science, 32:321-330, 1984.
O. Maler and L. Staiger. On syntactic congruences for ω-languages. Theoretical Computer Science, 183(1):93-112, 1997.
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.
M.O. Rabin. Decidability of second order theories and automata on infinite trees. Transaction of the AMS, 141:1-35, 1969.
S. Safra. On the complexity of omega-automata. In Proceedings of the 29th IEEE Symposium on Foundations of Computer Science, White Plains, October 1988.
A. L. Semenov. Presburgerness of predicates regular in two number systems. Siberian Mathematical Journal, 18:289-299, 1977.
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-292, Vancouver, June/July 1998. Springer-Verlag.
L. Staiger. Finite-state ω-languages. Journal of Computer and System Sciences, 27(3):434-448, 1983.
A. Prasad Sistla, Moshe Y. Vardi, and Pierre Wolper. The complementation problem for Büchi automata with applications to temporal logic. Theoretical Computer Science, 49:217-237, 1987.
L. Staiger and K. Wagner. Automatentheoretische und automatenfreie Charakterisierungen topologischer Klassen regulärer Folgenmengen. Elektron. Informationsverarbeitung und Kybernetik EIK, 10:379-392, 1974.
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.
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-331, Cambridge, June 1986.
Moshe Y. Vardi and Pierre Wolper. Automata-theoretic techniques for modal logics of programs. Journal of Computer and System Science, 32(2):183-221, April 1986.
Moshe Y. Vardi and Pierre Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1-37, November 1994.
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.