Reference : An Automata-Theoretic Approach to Presburger Arithmetic Constraints
Scientific congresses and symposiums : Paper published in a journal
Engineering, computing & technology : Computer science
http://hdl.handle.net/2268/74877
An Automata-Theoretic Approach to Presburger Arithmetic Constraints
English
Wolper, Pierre mailto [Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique > >]
Boigelot, Bernard mailto [Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique >]
1995
Lecture Notes in Computer Science
Springer
983
21-32
No
Yes
International
0302-9743
1611-3349
Berlin
Germany
Static Analysis, Second International Symposium (SAS'95)
Glasgow
UK
[en] automata ; Presburger arithmetic
[en] This paper introduces a finite-automata based representation of
Presburger arithmetic definable sets of integer vectors. The
representation consists of concurrent automata operating on the
binary encodings of the elements of the represented sets. This
representation has several advantages. First, being
automata-based it is operational in nature and hence leads directly
to algorithms, for instance all usual operations on sets of integer
vectors translate naturally to operations on automata. Second, the
use of concurrent automata makes it compact. Third, it is insensitive
to the representation size of integers. Our representation can be
used whenever arithmetic constraints are needed. To illustrate its
possibilities we show that it can handle integer programming optimally,
and that it leads to a new original algorithm for the satisfiability
of arithmetic inequalities.
Fonds de la Recherche Scientifique (Communauté française de Belgique) - F.R.S.-FNRS
http://hdl.handle.net/2268/74877
The original publication is available at www.springerlink.com

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
WB95.pdfAuthor preprint155.51 kBView/Open

Bookmark and Share SFX Query

All documents in ORBi are protected by a user license.