Deciding Satisfiability for Fragments with Unary Predicates and Difference Arithmetic

We report our work in progress\footnote[2]{Our knowledge on this matter has significantly improved since this paper was written. An update on this work will be provided in a following article.} to build decision procedures for highly expressive languages mixing arithmetic and uninterpreted predicates. More precisely, we study a language combining difference-logic constraints and unary predicates. The decision
problem is impacted by the domain of interpretation $\mathbb{N}$, $\mathbb{Z}$, $\mathbb{Q}$ or $\mathbb{R}$. For the integer domains $\mathbb{N}$ and $\mathbb{Z}$, the problem reduces to deciding the monadic second-order theory of $\mathbb{N}$ with the successor relation (S1S), which is known to be feasible by translating formulas into automata, and then checking the emptiness of their accepted language. We also advocate the use of automata as an appropriate tool to represent the set of models for the real domain $\mathbb{R}$.