2006/12/06 by Jérôme Leroux, Leroux, Jérôme · 1 citation
Computer Science · #Algorithms and Data Compression #Data Structures and Algorithms (cs.DS) #FOS: Computer and information sciences #Formal Methods in Verification #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.cs/0612037
openalex publication_date 2006/12/06 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Since 1969 \citeC-MST69,S-SMJ77, we know that any Presburger-definable set \citeP-PCM29 (a set of integer vectors satisfying a formula in the first-order additive theory of the integers) can be represented by a state-based symmbolic representation, called in this paper Finite Digit Vector Automata (FDVA). Efficient algorithms for manipulating these sets have been recently developed. However, the problem of deciding if a FDVA represents such a set, is a well-known hard problem first solved by Muchnik in 1991 with a quadruply-exponential time algorithm. In this paper, we show how to determine in polynomial time whether a FDVA represents a Presburger-definable set, and we provide in this positive case a polynomial time algorithm that constructs a Presburger-formula that defines the same set.