Least Significant Digit First Presburger Automata
<|reference_start|>Least Significant Digit First Presburger Automata: Since 1969 \cite{C-MST69,S-SMJ77}, we know that any Presburger-definable set \cite{P-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.<|reference_end|>
@article{leroux2006least,
    title={Least Significant Digit First Presburger Automata},
    author={J'er^ome Leroux (LaBRI)},
    journal={arXiv preprint arXiv:cs/0612037},
    year={2006},
    archivePrefix={arXiv},
    eprint={cs/0612037},
    primaryClass={cs.DS}
}