ORBi: Boigelot Bernard - Counting the solutions of Presburger equations without enumerating them

Reference : Counting the solutions of Presburger equations without enumerating them


	Document type :	Scientific journals : Article
	Discipline(s) :	Engineering, computing & technology : Computer science
	To cite this reference:	http://hdl.handle.net/2268/74856

Title :	Counting the solutions of Presburger equations without enumerating them
Language :	English
Author, co-author :	Boigelot, Bernard [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique >]
	Latour, Louis [ > > ]
Publication date :	2004
Journal title :	Theoretical Computer Science
Publisher :	Elsevier Science
Volume :	313
Issue/season :	1
Pages :	17-29
Audience :	International
ISSN :	0304-3975
City :	Amsterdam
Country :	The Netherlands
Keywords :	[en] Presburger arithmetic ; automata ; counting ; symbolic representation systems
Abstract :	[en] The Number Decision Diagram (NDD) has recently been introduced as a powerful representation system for sets of integer vectors. NDDs can notably be used for handling sets defined by arbitrary Presburger formulas, which makes them well suited for representing the set of reachable states of finite-state systems extended with unbounded integer variables. In this paper, we address the problem of counting the number of distinct elements in a set of numbers or, more generally, of vectors, represented by an NDD. We give an algorithm that is able to produce an exact count without enumerating explicitly the vectors, which makes it capable of handling very large sets. As an auxiliary result, we also develop an efficient projection method that allows to construct efficiently NDDs from quantified formulas, and thus makes it possible to apply our counting technique to sets specified by formulas. Our algorithms have been implemented in the verification tool LASH, and applied successfully to various counting problems.
Funders :	This work was partially funded by a grant of the "Communauté française de Belgique - Direction de la recherche scientifique - Actions de recherche concertées", and by the European Commission (FET project ADVANCE, contract No IST-1999-29082)
Target :	Researchers
Permalink :	http://hdl.handle.net/2268/74856
DOI :	10.1016/j.tcs.2003.10.002
Mentions required by the publisher for OA :	This is the author's version of the work. The published version is available online at http://dx.doi.org/10.1016/j.tcs.2003.10.002

File(s) associated to this reference

Fulltext file(s):

	File	Commentary	Version	Size	Access
Open access	BL04-preprint.pdf		Author preprint	226.73 kB	View/Open

All documents in ORBi are protected by a user license.

Dspace v1.5