Article (Scientific journals)
An effective decision procedure for linear arithmetic over the integers and reals
Boigelot, Bernard; Jodogne, Sébastien; Wolper, Pierre
2005In ACM Transactions on Computational Logic, 6 (3), p. 614-633
Peer Reviewed verified by ORBi
 

Files


Full Text
BJW05.pdf
Author postprint (218.05 kB)
Download

All documents in ORBi are protected by a user license.

Send to



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 :
6
Issue :
3
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
138 (22 by ULiège)
Number of downloads
454 (11 by ULiège)

Scopus citations®
 
57
Scopus citations®
without self-citations
40
OpenCitations
 
45

Bibliography


Similar publications



Contact ORBi