Paper published in a journal (Scientific congresses and symposiums)
Counting the Solutions of Presburger Equations without Enumerating Them
Boigelot, Bernard; Latour, Louis
2001In Lecture Notes in Computer Science, 2494, p. 40-51
Peer reviewed
 

Files


Full Text
BL01.pdf
Author preprint (192.8 kB)
Download

The original publication is available at www.springerlink.com


All documents in ORBi are protected by a user license.

Send to



Details



Keywords :
automata; Presburger arithmetic; counting
Abstract :
[en] The Number Decision Diagram (NDD) has recently been proposed as a powerful representation system for sets of integer vectors. In particular, NDDs can be used for representing the sets of solutions of arbitrary Presburger formulas, or the set of reachable states of some systems using unbounded integer variables. In this paper, we address the problem of counting the number of distinct elements in a set of vectors represented as an NDD. We give an algorithm that is able to perform 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.
Disciplines :
Computer science
Author, co-author :
Boigelot, Bernard  ;  Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique
Latour, Louis
Language :
English
Title :
Counting the Solutions of Presburger Equations without Enumerating Them
Publication date :
2001
Event name :
Implementation and Application of Automata, 6th International Conference (CIAA 2001)
Event place :
Pretoria, South Africa
Event date :
2001
Audience :
International
Journal title :
Lecture Notes in Computer Science
ISSN :
0302-9743
eISSN :
1611-3349
Publisher :
Springer, Berlin, Germany
Volume :
2494
Pages :
40-51
Peer reviewed :
Peer reviewed
Name of the research project :
ARC - Actions de recherche concertées
Funders :
FWB - Fédération Wallonie-Bruxelles [BE]
Available on ORBi :
since 03 November 2010

Statistics


Number of views
28 (3 by ULiège)
Number of downloads
119 (1 by ULiège)

Scopus citations®
 
2
Scopus citations®
without self-citations
0

Bibliography


Similar publications



Contact ORBi