Jump to : Download | Abstract | Contact | BibTex reference | EndNote reference |


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) 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


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

   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)

| VerTeCs | Team | Publications | New Results | Softwares |
Irisa - Inria - Copyright 2005 © Projet VerTeCs