Reference : An effective decision procedure for linear arithmetic over the integers and reals
Scientific journals : Article
Engineering, computing & technology : Computer science
http://hdl.handle.net/2268/12428
An effective decision procedure for linear arithmetic over the integers and reals
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ép. d'électric., électron. et informat. (Inst.Montefiore) > 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) >]
2005
ACM transactions on Computational Logic
ACM
6
3
614--633
Yes (verified by ORBi)
International
1529-3785
New-York
USA
[en] Decision procedure ; finite-state representations ; integer and real arithmetic ; weak ω-automata
[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.
Researchers
http://hdl.handle.net/2268/12428
© 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

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
BJW05.pdfAuthor postprint212.94 kBView/Open

Bookmark and Share SFX Query

All documents in ORBi are protected by a user license.