Reference : Counting the solutions of Presburger equations without enumerating them
Scientific journals : Article
Engineering, computing & technology : Computer science
http://hdl.handle.net/2268/74856
Counting the solutions of Presburger equations without enumerating them
English
Boigelot, Bernard mailto [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique >]
Latour, Louis [ > > ]
2004
Theoretical Computer Science
Elsevier Science
313
1
17-29
Yes (verified by ORBi)
International
0304-3975
Amsterdam
The Netherlands
[en] Presburger arithmetic ; automata ; counting ; symbolic representation systems
[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.
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)
Researchers
http://hdl.handle.net/2268/74856
10.1016/j.tcs.2003.10.002
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):

FileCommentaryVersionSizeAccess
Open access
BL04-preprint.pdfAuthor preprint226.73 kBView/Open

Bookmark and Share SFX Query

All documents in ORBi are protected by a user license.