Reference : On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables
Scientific congresses and symposiums : Paper published in a journal
Engineering, computing & technology : Computer science
http://hdl.handle.net/2268/21102
On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables
English
Boigelot, Bernard mailto [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique >]
Jodogne, Sébastien mailto [Université de Liège - ULG > > > Département d'Electricité, Electronique et Informatique > Informatique > >]
Wolper, Pierre mailto [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique (parallélisme et banques de données) >]
2001
Lecture Notes in Computer Science
Springer
2083
611--625
Yes
No
International
0302-9743
1611-3349
Berlin
Germany
First International Joint Conference on Automated Reasoning (IJCAR)
June 18–22 2001
Siana
Italy
[en] Presburger Arithmetic ; Automata ; reals ; integers
[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.
Communauté française de Belgique - Direction de la recherche scienti que - Actions de recherche concertées
Researchers
http://hdl.handle.net/2268/21102
10.1007/3-540-45744-5_50
The original publication is available at www.springerlink.com

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
BJW01-ijcar.pdfAuthor postprint177.14 kBView/Open

Bookmark and Share SFX Query

All documents in ORBi are protected by a user license.