[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
scite shows how a scientific paper has been cited by providing the context of the citation, a classification describing whether it supports, mentions, or contrasts the cited claim, and a label indicating in which section the citation was made.
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.
Similar publications
Sorry the service is unavailable at the moment. Please try again later.
This website uses cookies to improve user experience. Read more
Save & Close
Accept all
Decline all
Show detailsHide details
Cookie declaration
About cookies
Strictly necessary
Performance
Strictly necessary cookies allow core website functionality such as user login and account management. The website cannot be used properly without strictly necessary cookies.
This cookie is used by Cookie-Script.com service to remember visitor cookie consent preferences. It is necessary for Cookie-Script.com cookie banner to work properly.
Performance cookies are used to see how visitors use the website, eg. analytics cookies. Those cookies cannot be used to directly identify a certain visitor.
Used to store the attribution information, the referrer initially used to visit the website
Cookies are small text files that are placed on your computer by websites that you visit. Websites use cookies to help users navigate efficiently and perform certain functions. Cookies that are required for the website to operate properly are allowed to be set without your permission. All other cookies need to be approved before they can be set in the browser.
You can change your consent to cookie usage at any time on our Privacy Policy page.
