leroux05d

J. Leroux. A Polynomial Time Presburger Criterion and Synthesis for Number Decision Diagrams. In Proc. 20th IEEE Symp. Logic in Computer Science (LICS'2005), Pages 147-156, Chicago, USA, June 2005.

Download [help]

Download paper: Doi page

Download paper: Adobe portable document (pdf)

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic

Abstract

Number Decision Diagrams (NDD) are the automatabased symbolic representation for manipulating sets of integer vectors encoded as strings of digit vectors (least or most significant digit first). Since 1969 [8, 29], we know that any Presburger-definable set [26] (a set of integer vectors satisfying a formula in the first-order additive theory of the integers) can be represented by a NDD, and efficient algorithm for manipulating these sets have been recently developed [31, 4]. However, the problem of deciding if a NDD represents such a set, is a well-known hard problem first solved by Muchnik in 1991 [23, 24, 5] with a quadruplyexponential time algorithm. In this paper, we show how to determine in polynomial time whether a NDD represents a Presburger-definable set, and we provide in this positive case a polynomial time algorithm that constructs from the NDD a Presburger-formula that defines the same set

BibTex Reference

@InProceedings{leroux05d,
   Author = {Leroux, J.},
   Title = {A Polynomial Time Presburger Criterion and Synthesis for Number Decision Diagrams},
   BookTitle = {Proc. 20th IEEE Symp. Logic in Computer Science (LICS'2005)},
   Pages = {147--156},
   Address = {Chicago, USA},
   Month = {June},
   Year = {2005}
}

EndNote Reference [help]

Get EndNote Reference (.ref)