We report our work in progress2 to build decision procedures for highly expressive languages mixing arithmetic and uninterpreted predicates. More precisely, we study a language combining diference-logic constraints and unary predicates. The decision problem is impacted by the domain of interpretation N, Z, Q or R. For the integer domains N and Z, the problem reduces to deciding the monadic second-order theory of 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 R.
SMT (satisfiability modulo theories) solving has been very successfully used in various
applications, most notably in verification (see e.g., [
There is a simple explanation to this: mixing arithmetic and predicate symbols quickly leads to undecidability. For instance, Presburger arithmetic [5] is decidable, but adding a single ternary uninterpreted predicate symbol (or a binary function) to the language augments the expressive power to Peano arithmetic, since this uninterpreted symbol can be used to model multiplication. In fact, even adding a single unary uninterpreted predicate to Presburger arithmetic makes it undecidable [6]. It thus seems hopeless to find interesting decidable fragments with uninterpreted predicates for arbitrarily quantified formulas, on the basis of full linear arithmetic on integers.
However, if we weaken the expressiveness of arithmetic, there exist decidable quantified fragments with uninterpreted symbols, without restrictions on quantifiers. In Section 4 we recall that Büchi automata (a type of finite automata working on infinite words) provide a decision procedure for the monadic second-order theory of N with the successor relation (usually referred to as S1S), a language which is essentially equivalent to diference logic with uninterpreted predicates on the domain of the natural numbers N. In this extended abstract, we report on our work in progress to study the decidability of diference logic with uninterpreted predicates on various domains. For the domains of natural numbers N and integer numbers Z, this easily reduces to checking the emptiness of the language described by Büchi automata. For the real numbers however, the problem is significantly more complicated. We provide here some insights and directions to solve it. Our motivation is to precisely draw the frontier of decidability for satisfiability checking in presence of uninterpreted symbols and arithmetic.
After some prerequisites and notations in Section 2, we introduce in Section 3 the considered language and informally discuss its expressive power. Section 4 provides a decision procedure for this language when the domain is interpreted as the set of natural numbers N, restating a well established equivalence with checking the emptiness of the language accepted by Büchi automata. The following section adapts this result to the case of integers Z. We finally discuss in Section 6 our work in progress on this language interpreted over the real numbers R, before concluding.
We refer to e.g. [7] for a general introduction to first-order logic with equality, and assume that the reader is familiar with the notions of signature, term, variable, and formula. We use the usual logical connectives (∨, ∧, ¬, ⇒, ≡ ) and first-order quantification ( ∃. and ∀. ). Our signature essentially contains arithmetic symbols 0, 1, +, − , <, ≤ , ≥ , >, and uninterpreted symbols , ,. . . . A constant in N stands for a term 1 + 1 + . . . 1. In the following, we only consider unary predicate symbols. The set of all formulas built using variables and symbols from a signature is the language of formulas. An interpretation specifies a domain (i.e., a set of elements), assigns a value in the domain to each free variable, and assigns function and predicate relations of appropriate arity to the function and predicate symbols in the signature. We only consider interpretations whose domain is N, Z, Q or R. The arithmetic symbols are interpreted on the chosen domain, that is, an interpretation always assigns its usual meaning on the domain to each arithmetic symbol. The uninterpreted symbols are left free, that is, an interpretation can assign to a unary predicate an arbitrary subset of the domain on which the predicate is true, the predicate being false on the complement of this set in the domain.
By extension, an interpretation assigns a value in the domain to every term, and a truth value to every formula. A model is an interpretation that assigns true to the formula. A formula is satisfiable on a domain ( N, Z, Q or R) if it has a model on that domain.
A fragment is a first-order language of formulas, possibly with further syntactical restrictions, and a domain of interpretation. We say that a fragment is decidable if there is an efective procedure to check whether a given formula in the language is satisfiable on this domain.
We consider a first-order language of formulas, built using usual logical connectives ( ∨, ∧, ¬, ⇒, ≡ ) and first-order quantification ( ∃. and ∀. ). Atoms are either diference-logic constraints of the form − ◁▷ , where and are variables, is a constant in N, and ◁▷ ∈ {<, ≤ , =, ≥ , >}, or unary predicate formulas (), where is an uninterpreted predicate symbol and is a variable. The formulas are interpreted on a given domain, equal to either N, Z, Q or R. For the domains Z and R, our fragments are actually subsets of the SMT-LIB logics UFIDL and UFRDL [8], i.e., the logics that mix Uninterpreted Functions and Diference Logic over the Integers or the Reals. Since they only allow unary predicates, we call our fragments UF1NDL, UF1IDL, UF1QDL and UF1RDL when the domain of interpretation is N, Z, Q and R respectively.
These fragments are actually quite expressive, as we illustrate now: • (0) ∧ ¬ (1) ∧ ∀ ∀ . ( − = 2) ⇒ ( () ≡ ())
Over either N or Z, this formula states that the predicate is true for all even numbers. • ∀ ∀ ∃ . < ⇒ ( < ∧ < ∧ ())
This formula enforces the set of values that satisfy to be dense within the domain of interpretation. It is obviously unsatisfiable if the domain itself is not dense, e.g., for the domains N and Z. • ∀ ∀ ∃ . < ⇒ ( < ∧ < )
Since no predicate variable is used here, this sentence is valid if and only if the domain is dense, which holds for Q and R. • ∀ ∀ ∃ ∃ . < ⇒ ( < < ∧ < < ∧ () ∧ ¬ ())
This property (that we call chaoticity) states that both the predicate and its complement ¬ are dense within the domain. In other words, there does not exist a non-empty open interval of the domain in which is either uniformly true or uniformly false. • (∃ ∀. () ⇒ < ) ∧ (∀. (∀. () ⇒ ≤ ) ⇒ (∃. (∀. () ⇒ ≤ ) ∧ ( > ))) This states that the subset described by admits a lower bound, but no maximal lower bound; this partly expresses the negation of the Dedekind completeness property [9].
Notice that this logical formalism is suficiently expressive to discriminate between the various domains of interpretation. Namely, the sentence describing the density of the domain is false on N and Z, and true on Q and R. It is easy to imagine a formula discriminating N from Z by stating the existence of a smaller element. We are able to discriminate between Q and R thanks to the last property.
The satisfiability problem for UF1NDL, i.e., our fragment interpreted over the natural numbers, reduces to the satisfiability of S1S, that is, the monadic second-order theory of N with the successor relation [10]. Indeed, the order relation ≤ can be reconstructed as follows in S1S: ∀ . (() ∧ ∀ . () ⇒ ( + 1)) ⇒ ()
It is also known that the language of models of a given S1S formula is recognizable by an infinite-word automaton. Every formula of S1S can indeed be translated by structural induction into a Büchi automaton that represents the set of its models [11]. Checking the satisfiability of a given S1S formula therefore reduces to checking the emptiness of the language accepted by the corresponding Büchi automaton, which is decidable [11, 10]. This shows that satisfiability is decidable for UF1NDL.
A related but slightly diferent way of deciding the satisfiability of the fragment UF1NDL consists in translating directly UF1NDL formulas into infinite-word automata representing their models. We now provide some details on this translation procedure.
A predicate : N → {⊤, ⊥} can be encoded by an infinite word 012 . . . ∈ {0, 1}, where for all ∈ N, = 1 if () = ⊤. Similarly, the value of a variable ∈ N can be encoded by the word 010. For a formula (1, . . . , , 1, . . . , ) with predicates 1, . . . , and free variables 1, . . . , , an interpretation of these variables and predicates over N is encoded by an infinite word over the alphabet {0, 1}+, every symbol of which provides one digit of the encoding of each predicate and each variable value.
For a given UF1NDL formula , the set of encodings of the models of forms a language ( ). It is easily shown that this language is -regular, and that a Büchi automaton that accepts this language can efectively be built, by proceeding by induction on the structure of . The atoms − ◁▷ and ( ) directly translate into elementary automata. Then, similarly to the translation of S1S formulas into automata, one applies Boolean connectives and quantifiers by means of automata manipulations that essentially amount to performing the same operation on their accepted languages [11]. The problem of deciding whether is satisfiable then becomes equivalent to checking whether the resulting automaton accepts a non-empty language.
This decision procedure has the advantage of simplicity, but requires to be able to complement Büchi automata, which is a costly operation in practice [12, 13].
The translation procedure from UF1NDL to Büchi automata sketched in Section 4.2 sufices to establish that satisfiability is decidable for UF1NDL. It is however worth mentioning that the reverse translation is also possible, which shows that UF1NDL and Büchi automata share the same expressive power.
More precisely, given a Büchi automaton accepting a language , one can build a formula of UF1NDL that is satisfiable if is not empty. The main principle of this translation consists in employing the appropriate number of predicates for encoding the sequence of states visited by the automaton during a run. One then constructs a formula that checks that every step in this sequence satisfies the transition relation of the automaton, that its first element corresponds to the initial state of the automaton, and that it describes an accepting run [10].
The decision procedure for UF1NDL outlined in Section 4.2 straightforwardly generalizes to the integer domain. The only dificulty is to design a scheme for encoding values in Z and predicates over Z as infinite words.
A solution consists in encoding ∈ Z such that ≥ 0 as 0210, and < 0 as 0− 2− 110. The same idea can be adapted to represent predicates. With this encoding, the atoms − ◁▷ and ( ) translate into elementary automata that are identical or only slightly more complex than the ones obtained for UF1NDL. The same approach then reduces the decidability of UF1IDL to the problem of checking whether the automaton constructed from a given formula accepts a non-empty language.
We now address the problem of deciding satisfiability for UF1RDL formulas, i.e., our fragment interpreted over the domain R. As a first step, we only consider a restricted fragment that we call Weak UF1RDL (WUF1RDL), in which • each formula involves at most one unary uninterpreted predicate , • diference-logic atoms are of the form − ◁▷ 0, i.e., the only constant allowed is 0. Notice that even with such restrictions, all the properties illustrated in Section 3 but the first one remain expressible.
Our goal is to follow the same approach as in Sections 4 and 5 for the domains N and Z, which consists in designing an encoding scheme for the predicate and variable values, building a symbolic representation of the set of models of a given formula, and checking whether this set is empty or not.
Unlike the case of the integer domains N and Z, a predicate : R → {⊤, ⊥} cannot be unambiguously encoded as an infinite word 012 . . . over some finite alphabet. Such a precise representation of is however not needed. Indeed, the fragment WUF1RDL does not make it possible to express constraints about the absolute diference between real values, but only about their relative order. This means that if two predicates and ′ admit characteristic sets { ∈ R | ()} and { ∈ R | ′()} whose elements are ordered in the same way over R, then for every formula of WUF1RDL involving one predicate and free variables, (, 1, . . . , ) is satisfiable if ( ′, 1, . . . , ) is satisfiable as well.
Instead of designing an encoding scheme that precisely describes a given predicate, we thus opt for an abstract encoding relation that maps multiple predicate interpretations onto the same representation. Our goal is to design this relation in such a way that if two predicates and ′ share the same representation, then for every formula of WUF1RDL involving one predicate and free variables, (, 1, . . . , ) will be satisfiable if ( ′, 1, . . . , ) is satisfiable as well.
Consider an arbitrary predicate : R → {⊤, ⊥}. We define the set ⊆ R as the set of all real values that belong to an open interval in which is uniformly true. Similarly, we define ⊆ R as the set of all real values that belong to an open interval in which is uniformly false. Finally, we define ⊆ R as the set of all real values that belong to an open interval that has an empty intersection with ∪ . In such an interval, the behavior of is necessarily chaotic (cf. Section 3), since this interval cannot contain a sub-interval of non-zero length in which has a constant value.
Each of the sets , and is thus equal to a union of non-empty open intervals in R, with the additional property that those intervals do not overlap. This union is therefore necessarily countable [14], since each of them contains a rational value that does not belong to the others. Let denote the set of those intervals. The set ∪ ∪ entirely covers R except for a (possibly uncountable) number of discrete points, that we gather in a set . The elements of correspond to the endpoints of the intervals in , together with the limits of all convergent sequences of such endpoints.
The set ∪ thus forms a totally ordered partition of R. The following picture depicts such a partition, in which the elements of are shown as rectangles and those of as black dots. It is possible that an infinite number of intervals of appear within a bounded interval of the real line; the smaller dots appearing between two black dots in the right part of the picture illustrate such a behavior.
In order to obtain an abstract representation for the predicate , we use the notion of word over linear orderings introduced in [15], that generalizes the concept of infinite word. Given a totally ordered set and a finite alphabet Σ , a word over is a mapping from the ordering of to Σ , i.e., a function that associates each element of the ordering with an element of the alphabet.
For a predicate : R → {⊤, ⊥}, we define the abstract encoding of as the word over the totally ordered set ∪ that maps every element of onto the alphabet {, , }, and every element of onto {⊤, ⊥}. For every ∈ , one has () = if ⊆ , () = if ⊆ , and () = if ⊆ . For every ∈ , one has () = ⊤ if () = ⊤ and () = ⊥ if () = ⊥.
The abstract encoding of variable values must contain enough information to represent their relative order, as well as their relation with the predicate . We encode each variable value as a word over the same totally ordered set ∪ as for the predicate , or over an arbitrarily chosen ordering in the case of a formula with no predicate. For a variable, every element of is mapped onto a single symbol , and every element of onto the alphabet {⊤, ⊥}, such that () = ⊤ if the value of the variable is equal to .
With this encoding scheme, one cannot encode a variable value that does not belong to . This is not problematic, since intervals can easily be split. If one needs to express that a variable has a value that belongs to an interval (, ) ∈ , this interval can be replaced in by both (, ) and (, ), where is any value such that < < , and is then added to . Since the number of variables is finite, this operation has only to be carried out finitely many times.
Finally, just like in the case of the integer domains N and Z, the abstract encodings of the predicates and all variables can be combined into a single word over the totally ordered set ∪ . Each element of is mapped onto the alphabet {, , } × { }, where is the number of variables, and each element of is mapped onto {⊤, ⊥}1+.
A notion of automaton operating on words over any total ordering (hence possibly uncountable ones) has been introduced in [15]. We conjecture that this formalism makes it possible to represent symbolically the set of models of any WUF1RDL formula. More precisely, we aim at establishing that for every formula with one predicate and free variables: • for every predicates and ′ that share the same abstract encoding (cf. Section 6.1), (, 1, . . . , ) is satisfiable if ( ′, 1, . . . , ) is satisfiable as well, • the set of encodings of the models of can be recognized by an automaton over total orderings, and such an automaton can efectively be built by structural induction on , • the formula is satisfiable if its corresponding automaton accepts a non-empty language.
Those properties hold for the atomic formulas of WUF1RDL. In order to be able to apply Boolean connectives and to perform quantification, one needs to provide corresponding operations on the automata representing the set of models of the formula being handled, and show that these operations preserve the properties of interest. The main dificulty revolves around the complementation operation, which is needed in particular for handling universal quantification.
The problem of complementing automata over total orderings has been investigated in [16] and [17]. A solution has been obtained for automata operating over a restricted class of total orderings called finite-rank orderings. Whether this class is suited for representing models of WUF1RDL formulas remains an open problem, the question being to establish that for every formula , the set of finite-rank models of is non-empty if is satisfiable. Our preliminary results about this problem are promising. Finally, the problem of checking the emptiness of the language accepted by an automaton over a total ordering is solved in [18].
In this work, we have investigated highly expressive first-order languages that stand close to the frontier of decidability. These fragments mix diference-logic constraints and uninterpreted unary predicates, and their expressive power varies with their domain of interpretation.
For the domains of natural and integer numbers, there exists a natural translation of formulas expressed in the corresponding fragments into finite automata. Such automata can efectively be built by structural induction over the formulas, and provide a symbolic representation of their set of models. Checking whether a given formula is satisfiable amounts to checking whether the language accepted by the corresponding automaton is empty or not.
The case of the rational and real domains is more involved, since the expressive power of even a single unary predicate over a dense domain makes it possible to describe structures that are more complex than for the natural and integer domains. One could be startled by this, since arithmetic theories over the reals are very often simpler to handle than those over the integers, and usually admit decision procedures of lower complexity [19]. This is not the case for the fragments studied here, for which it actually turns out that the problem of deciding their satisfiability over N or Z reduces to the same problem over R, and not the other way around. Indeed, one can easily define a predicate over R that is only true for isolated values, and express the property that each of those values admit exactly one successor, which essentially allows to simulate natural or integer numbers with real variables.
We have presented our work in progress aimed at developing a decision procedure for the logic UF1RDL. Our approach relies on the automata over total orderings introduced in [15]. Our ifrst-priority goal is to establish that these automata provide suitable symbolic representations for the sets of models of formulas that involve a single unary predicate and diference-logic constraints of the form − ◁▷ 0.
The generalization of this result to formulas with multiple predicates seems to be straightforward; it essentially amounts to synchronizing the abstract encodings of all predicates with respect to the same total order, and adding equality and disequality constraints over them in each elementary interval of the representation. Allowing constraints of the form − ◁▷ for arbitrary values of seems to be more dificult, and would require to adapt the encoding of predicate and variable values so as to be able to reason about the absolute diference between values.
Our motivation is here to precisely draw the frontier of decidability for satisfiability checking of formulas containing uninterpreted symbols and arithmetic. This could also give us insights for quantifier elimination, or rather more generally for handling quantifiers for fragments mixing uninterpreted symbols and arithmetic.
Finally, another perspective would be to investigate the possibility of lifting our results to the domain of rational numbers. [4] E. Ábrahám, J. H. Davenport, M. England, G. Kremer, Deciding the consistency of nonlinear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings, Journal of Logical and Algebraic Methods in Programming 119 (2021) 100633. [5] M. Presburger, On the completeness of a certain system of arithmetic of whole numbers in which addition occurs as the only operation, History and Philosophy of Logic 12 (1991) 225–233. English translation of the original paper from 1929. [6] J. Y. Halpern, Presburger arithmetic with unary predicates is Π 11 complete, The Journal of
Symbolic Logic 56 (1991) 637–642. [7] H. B. Enderton, A mathematical introduction to logic, Elsevier, 2001. [8] C. Barrett, P. Fontaine, C. Tinelli, The Satisfiability Modulo Theories Library (SMT-LIB), www.SMT-LIB.org, 2016. [9] E. J. McShane, Partial orderings and Moore-Smith limits, The American Mathematical
Monthly 59 (1952) 1–11. [10] W. Thomas, Languages, automata, and logic, in: Handbook of formal languages, Springer, 1997, pp. 389–455. [11] J. R. Büchi, On a decision method in restricted second order arithmetic, Logic, Methodology and Philosophy of Science, 1962. [12] S. Safra, Complexity of automata on infinite objects, Ph.D. thesis, Weizmann Institute of
Science, 1989. [13] A. P. Sistla, M. Y. Vardi, P. Wolper, The complementation problem for Büchi automata with applications to temporal logic, Theoretical Computer Science 49 (1987) 217–237. [14] W. Sierpiński, Cardinal and ordinal numbers (2nd edition), PWN, Warszawa, 1965. [15] V. Bruyère, O. Carton, Automata on linear orderings, Journal of Computer and System
Sciences 73 (2007) 1–24. [16] C. Rispal, O. Carton, Complementation of rational sets on countable scattered linear orderings, International Journal of Foundations of Computer Science 16 (2005) 767–786. [17] C. Rispal, Automates sur les ordres linéaires: Complémentation, Ph.D. thesis, Université de Marne la Vallée, 2004. [18] O. Carton, Accessibility in automata on scattered linear orderings, in: International Symposium on Mathematical Foundations of Computer Science, Springer, 2002, pp. 155– 164. [19] J. Ferrante, C. W. Rackof, The computational complexity of logical theories, volume 718, Springer, 2006.