ORBi: Wolper Pierre - An Automata-Theoretic Approach to Presburger Arithmetic Constraints

Reference : An Automata-Theoretic Approach to Presburger Arithmetic Constraints


	Document type :	Scientific congresses and symposiums : Paper published in a journal
	Discipline(s) :	Engineering, computing & technology : Computer science
	To cite this reference:	http://hdl.handle.net/2268/74877

Title :	An Automata-Theoretic Approach to Presburger Arithmetic Constraints
Language :	English
Author, co-author :	Wolper, Pierre [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique > >]
	Boigelot, Bernard [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique >]
Publication date :	1995
Journal title :	Lecture Notes in Computer Science
Publisher :	Springer
Volume :	983
Pages :	21-32
On invitation :	Yes
Audience :	International
ISSN :	0302-9743
e-ISSN :	1611-3349
City :	Berlin
Country :	Germany
Event name :	Static Analysis, Second International Symposium (SAS'95)
Event place (city) :	Glasgow
Event country :	UK
Keywords :	[en] automata ; Presburger arithmetic
Abstract :	[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.
Funders :	Fonds de la Recherche Scientifique (Communauté française de Belgique) - F.R.S.-FNRS
Permalink :	http://hdl.handle.net/2268/74877
Mentions required by the publisher for OA :	The original publication is available at www.springerlink.com

File(s) associated to this reference

Fulltext file(s):

	File	Commentary	Version	Size	Access
Open access	WB95.pdf		Author preprint	155.51 kB	View/Open

All documents in ORBi are protected by a user license.

Dspace v1.5