Marco Voigt

The Bernays-Schönfinkel-Ramsey Fragment with Bounded Difference Constraints over the Reals is Decidable

Keywords: Bernays-Schönfinkel-Ramsey fragment, linear arithmetic constraints, difference constraints, combination of theories

The Bernays-Schönfinkel-Ramsey Fragment with Bounded Difference Constraints over the Reals Is Decidable

Introduction

It has been discovered about half a century ago that linear arithmetic with additional uninterpreted predicate symbols has an undecidable satisfiability problem [START_REF] Putnam | Decidability and Essential Undecidability[END_REF]. Even enriching Presburger arithmetic with only a single uninterpreted predicate symbol of arity one suffices to facilitate encodings of the halting problem for two-counter machines [START_REF] Peter | Undecidability of Presburger Arithmetic with a Single Monadic Predicate Letter[END_REF][START_REF] Horbach | The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable[END_REF]. These results do not change substantially when we use the reals as underlying domain instead of the integers. This means, in order to obtain a decidable subfragment of the combination of linear arithmetic with uninterpreted predicate symbols, the arithmetic part has to be restricted considerably. In this paper, two subfragments with a decidable satisfiability problem are presented. Both are based on the Bernays-Schönfinkel-Ramsey fragment (BSR) of first-order logic, which is the ∃ * ∀ * prefix class. Uninterpreted constant symbols and the distinguished equality predicate are allowed, non-constant function symbols are not. The arity of uninterpreted predicate symbols is not restricted. We extend BSR in two ways and call the obtained clause fragments BSR modulo simple linear real constraints-BSR(SLR)-and BSR modulo bounded difference constraints-BSR(BD).

The first clause class-defined in Definition 1 and treated in detail in Section 4-adds constraints of the form s t, x t, and x y to BSR clauses, where x and y are real-valued variables that are implicitly universally quantified, s and t are linear arithmetic terms that are ground, and ranges over <, ≤, =, =, ≥, >. We allow Skolem constants in the ground terms s and t. Since their value is not predetermined, they can be conceived as being existentially quantified. The constraints used in this clause fragment are similar to the kind of constraints that appear in the context of the array property fragment [START_REF] Bradley | What's Decidable About Arrays? In Verification, Model Checking, and Abstract Interpretation[END_REF] and extensions thereof (see, e.g., [START_REF] Ge | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories[END_REF][START_REF] Horbach | On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic[END_REF]). The main differences are that we use the real domain in this paper instead of the integer domain, and that we allow strict inequalities and disequations between universally quantified variables. In the presence of uninterpreted function symbols, strict inequality or disequations can be used to assert that some uninterpreted function f is injective. This expressiveness prevents certain instantiation-based approaches to satisfiability checking from being applicable, e.g. the methods in [START_REF] Bradley | What's Decidable About Arrays? In Verification, Model Checking, and Abstract Interpretation[END_REF][START_REF] Horbach | On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic[END_REF]. In the context of the array property fragment, this expressiveness even leads to undecidability.

The BSR(BD) clause class-presented in Definition 2 and in Section 5-adds constraints of the form x c, x y and x -y c to BSR clauses, where x and y are real-valued variables, c could be any rational number, and ranges over <, ≤, =, =, ≥, > again. We refer to constraints of the form x -y c as difference constraints. Already in the seventies, Pratt identified difference constraints and boolean combinations thereof as an important tool for the formalization of verification conditions [START_REF] Vaughan | Two Easy Theories Whose Combination is Hard[END_REF]. Applications include the verification of timed systems and scheduling problems (see, e.g., [START_REF] Kroening | Decision Procedures[END_REF] for references). As unrestricted combinations of uninterpreted predicate symbols with difference constraints lead to an undecidable satisfiability problem (once more, two-counter machines can be encoded in a simple way [START_REF] Voigt | Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete[END_REF]), we have to further confine the language. Every difference constraint x -y c has to be conjoined with four additional constraints c x ≤ x, x ≤ d x , c y ≤ y, y ≤ d y , where c x , d x , c y , d y are rationals. This restriction seems to weaken expressiveness severely. Indeed, it has to, since we aim for a decidable satisfiability problem. Yet, we show in Section 6 that BSR(BD) clause sets are expressive enough to formulate the reachability problem for timed automata. In [START_REF] Niebert | Verification of Timed Automata via Satisfiability Checking[END_REF] an encoding of the reachability problem for timed automata in difference logic (boolean combinations of difference constraints without uninterpreted predicate symbols) is given, which facilitates deciding bounded reachability, i.e. the problem of reaching a given set of states within a bounded number of transition steps. When using BSR(BD) as a modeling language, we do not have to fix an upper bound on the number of steps a priori.

The main result of the present paper is that satisfiability of finite BSR(SLR) clause sets and finite BSR(BD) clause sets is decidable, respectively (Theorems 12 and 19). The proof technique is very similar for the two fragments. It is partially based on methods from Ramsey theory, which are briefly introduced in Section 3. The used approach may turn out to be applicable to other fragments of BSR modulo linear real arithmetic as well. Due to space limitations, most proofs are only sketched. Detailed proofs can be found in [START_REF] Voigt | The Bernays-Schönfinkel-Ramsey Fragment with Bounded Difference Constraints over the Reals is Decidable[END_REF].

Preliminaries and notation

Hierarchic combinations of first-order logic with background theories build upon sorted logic with equality [START_REF] Bachmair | Refutational Theorem Proving for Hierarchic First-Order Theories[END_REF][START_REF] Baumgartner | Hierarchic Superposition with Weak Abstraction[END_REF][START_REF] Kruglov | Superposition Decides the First-Order Logic Fragment Over Ground Theories[END_REF]. We instantiate this framework with the BSR fragment and linear arithmetic over the reals as the base theory. The base sort R shall always be interpreted by the reals R. For simplicity, we restrict our considerations to a single free sort S, which may be freely interpreted as some nonempty domain, as usual.

We denote by V R a countably infinite set of base-sort variables. Linear arithmetic (LA) terms are build from rational constants 0, 1, 1 2 , -2, -3 4 , etc., the operators +, -, and the variables from V R . We moreover allow base-sort constant symbols whose values have to be determined by an interpretation (Skolem constants). They can be conceived as existentially quantified. As predicates over the reals we allow the standard relations <, ≤, =, =, ≥, >.

In order to hierarchically extend the base theory by the BSR fragment, we introduce the free sort S, a countably infinite set V S of free-sort variables, a finite set Ω S of free (uninterpreted) constant symbols of sort S and a finite set Π of free predicate symbols equipped with sort information. Note that every predicate symbol in Π has a finite, nonnegative arity and can be of a mixed sort over the two sorts R and S, e.g. P : R × S × R. We use the symbol ≈ to denote the built-in equality predicate on S. To avoid confusion, we tacitly assume that no constant or predicate symbol is overloaded, i.e. they have a unique sort.

Definition 1 (BSR with simple linear real constraints-BSR(SLR)). A BSR(SLR) clause has the form Λ Γ → ∆, where Λ, Γ , ∆ are multisets of atoms satisfying the following conditions. (i) Every atom in Λ is an LA constraint of the form s t or x t or x y where s, t are ground (i.e. variable-free) LA terms, x, y ∈ V R , and ∈{<, ≤, =, =, ≥, >}. (ii) Every atom in Γ and ∆ is either an equation s ≈ s over free-sort variables and constant symbols, or a non-equational atom P (s 1 , . . . , s m ) that is well sorted and where the s i range over base-sort variables, free-sort variables, and free-sort constant symbols.

Definition 2 (BSR with bounded difference constraints-BSR(BD)).

A BSR(BD) clause has the form Λ Γ → ∆, where the multisets Γ , ∆ satisfy Condition (ii) of Definition 1, and every atom in Λ is an LA constraint of the form x c, x y, or x -y c where c may be any rational constant (not a Skolem constant), x, y ∈ V R , and ∈{<, ≤, =, =, ≥, >}. Moreover, we require that whenever Λ contains a constraint of the form x -y c, then Λ also contains constraints c x ≤ x, x ≤ d x , c y ≤ y, and y ≤ d y with c x , d x , c y , d y ∈ Q.

We omit the empty multiset left of "→" and denote it by right of "→" (where at the same time stands for falsity). The introduced clause notation separates arithmetic constraints from the free first-order part. We use the vertical double bar " " to indicate this syntactically. Intuitively, clauses Λ Γ → ∆ can be read as Λ ∧ Γ → ∆, i.e. the multisets Λ, Γ stand for conjunctions of atoms and ∆ stands for a disjunction of atoms. Requiring the free parts Γ and ∆ of clauses to not contain any base-sort terms apart from variables does not limit expressiveness. Every base-sort term t ∈ V R in the free part can safely be replaced by a fresh base-sort variable x t when an atomic constraint x t = t is added to the constraint part of the clause (a process known as purification or abstraction [START_REF] Bachmair | Refutational Theorem Proving for Hierarchic First-Order Theories[END_REF][START_REF] Kruglov | Superposition Decides the First-Order Logic Fragment Over Ground Theories[END_REF]).

A (hierarchic) interpretation is an algebra A which interprets the base sort R as R A = R, assigns real values to all occurring base-sort Skolem constants and interprets all LA terms and constraints in the standard way. Moreover, A comprises a nonempty domain S A , assigns to each free-sort constant symbol c in Ω S a domain element c A ∈ S A , and interprets every sorted predicate symbol

P : ξ 1 × . . . × ξ m in Π by some set P A ⊆ ξ A 1 × . . . × ξ A m .
Summing up, A extends the standard model of linear arithmetic and adopts the standard approach to semantics of (sorted) first-order logics when interpreting the free part of clauses.

Given an interpretation A and a sort-respecting variable assignment β : Given a BSR(SLR) or BSR(BD) clause C, we use the following notation: the set of all constant symbols occurring in C is denoted by consts(C). The set bconsts(C) (fconsts(C)) is the restriction of consts(C) to base-sort (free-sort) constant symbols. We denote the set of all variables occurring in a clause C by vars(C). The same notation is used for sets of clauses.

V R ∪ V S → R A ∪ S A ,
Definition 3 (Normal form of BSR(SLR) and BSR(BD) clauses). A BSR(SLR) or BSR(BD) clause Λ Γ → ∆ is in normal form if (1) all nonground atoms in Λ have the form x c, x y, or x -y c where c is a rational constant or a Skolem constant, and (2) every variable that occurs in Λ also occurs in Γ or in ∆. A BSR(SLR) or BSR(BD) clause set N is in normal form if all clauses in N are in normal form and pairwise variable disjoint. Moreover, we assume that N contains at least one free-sort constant symbol.

For BSR(SLR) clause sets, we pose the following additional requirement. N can be divided into two parts N def and N such that (a) every clause in N def has the form c = t → where c is a Skolem constant and t is some ground LA term, and (b) any ground atom s t in any constraint part Λ in any clause Λ Γ → ∆ in N is such that s and t are constants (Skolem or rational, respectively).

For every BSR(SLR) clause set N there is an equisatisfiable BSR(SLR) clause set N in normal form, such that N |= N . The same holds for BSR(BD) clause sets. Requirement (2) can be established by any procedure for eliminating existentially quantified variables in LA constraints (see, e.g., [START_REF] Fietzke | Superposition as a Decision Procedure for Timed Automata[END_REF]). Establishing the other requirements is straightforward.

For two sets R, Q ⊆ R we write R < Q if r < q holds for all r ∈ R and q ∈ Q. Given a real r, we denote the integral part of r by r , i.e. r is the largest integer for which r ≤ r. By fr(r) we denote the fractional part of r, i.e. fr(r) := r -r . Notice that fr(r) is always nonnegative, e.g. fr(3.71) = 0.71, whereas fr(-3.71) = 0.29. Given any tuple r of reals, we write fr(r) to mean the corresponding tuple of fractional parts, i.e. fr r 1 , . . . , r µ := fr(r 1 ), . . . , fr(r µ ) . We use the notation r in a component-wise fashion as well.

We write [k] to address the set {1, . . . , k} for any positive integer k > 0. Finally, P denotes the power set operator, i.e. for any set S, P(S) denotes the set of all subsets of S.

Basic tools from Ramsey theory

In this section we establish two technical results based on methods usually applied in Ramsey theory. We shall use these results later on to prove the existence of models of a particular kind for finite and satisfiable BSR(SLR) or BSR(BD) clause sets. These models meet certain uniformity conditions. In order to construct them, we rely on the existence of certain finite subsets of R that are used to construct prototypical tuples of reals. These finite subsets, in turn, have to behave nicely as well, since tuples that are not distinguishable by BSR(SLR) or BSR(BD) constraints are required to have certain uniformity properties.

A tuple r 1 , . . . , r m ∈ R m is called ascending if r 1 < . . . < r m . A coloring is a mapping χ : S → C for some arbitrary set S and some finite set C. For the most basic result of this section (Lemma 4), we consider an arbitrary coloring χ of m-tuples of real numbers and stipulate the existence of a finite subset Q ⊆ R of a given cardinality n such that all ascending m-tuples of elements from Q are assigned the same color by χ. Lemma 4. Let n, m > 0 be positive integers. Let χ : R m → C be some coloring. There is some positive integer n such that for every set R ⊆ R with |R| ≥ n-i.e. R needs to be sufficiently large-there exists a subset Q ⊆ R of cardinality n such that all ascending tuples r 1 , . . . , r m ∈ Q m are assigned the same color by χ.

Proof (adaptation of the proof of Ramsey's Theorem on page 7 in [START_REF] Graham | A Wiley-Interscience publication[END_REF]). For n < m the lemma is trivially satisfied, since in this case Q m cannot contain ascending tuples. Hence, we assume n ≥ m. In order to avoid technical difficulties when defining the sequence of elements s m-1 , s m , s m+1 , . . . below, we assume for the rest of the proof that R is finite but sufficiently large. This assumption does not pose a restriction, as we can always consider a sufficiently large finite subset of R, if R were to be infinite.

We proceed by induction on m ≥ 1. The base case m = 1 is easy, since χ can assign only finitely many colors to elements in R and thus some color must be assigned at least |R| |C| times. Hence, if R contains at least n|C| elements, we find a uniformly colored subset Q of size n. Suppose m > 1. At first, we pick the m-2 smallest reals s 1 < . . . < s m-2 from R and set S m-2 := R\{s 1 , . . . , s m-2 }. Thereafter, we simultaneously construct two sufficiently long but finite sequences s m-1 , s m , s m+1 , . . . and S m-1 , S m , S m+1 , . . . as follows: Given S i , we define s i+1 to be the smallest real in S i . Given S i and the element s i+1 , we define an equivalence relation ∼ i on the set S i := S i \ {s i+1 } so that s ∼ i s holds if and only if for every sequence of indices j 1 , . . . , j m-1 with 1 ≤ j 1 < . . . < j m-1 ≤ i + 1, we have χ(s j1 , . . . , s jm-1 , s) = χ(s j1 , . . . , s jm-1 , s ). This equivalence relation partitions S i into at most |C| ( i+1 m-1 ) equivalence classes. We choose one such class with largest cardinality to be S i+1 .

By construction of the sequence s 1 , s 2 , s 3 , . . ., we must have χ(s j1 , . . . , s jm-1 , s k ) = χ(s j1 , . . . , s jm-1 , s k ) for every sequence of indices j 1 < . . . < j m-1 and all indices k, k ≥ j m-1 + 1. Please note that this covers all ascending mtuples in {s 1 , s 2 , s 3 , . . .} m starting with s j1 , . . . , s jm-1 , i.e. they all share the same color. We now define a new coloring χ : {s 1 , s 2 , s 3 , . . .} m-1 → C so that χ (s j1 , . . . , s jm-1 ) := χ(s j1 , . . . , s jm-1 , s jm-1+1 ) for every sequence of indices j 1 < . . . < j m-1 (in case of j m-1 being the index of the last element in the sequence s 1 , s 2 , s 3 , . . ., χ (s j1 , . . . , s jm-1 ) shall be an arbitrary color from C). By induction, there exists a subset Q ⊆ {s 1 , s 2 , s 3 , . . .} of cardinality n, such that every ascending (m-1)-tuple r ∈ Q m-1 is colored the same by χ . The definition of χ entails that now all ascending m-tuples r ∈ Q m are colored the same by χ. Hence, Q is the sought set.

Based on Lemma 4, one can derive similar results for more structured ways of coloring tuples of reals. We shall employ such a structured coloring when proving that the satisfiability problem for finite BSR(SLR) clause sets is decidable. More precisely, the proof of Lemma 10 will rely on such a result. The technical details are elaborated in [START_REF] Voigt | The Bernays-Schönfinkel-Ramsey Fragment with Bounded Difference Constraints over the Reals is Decidable[END_REF].

Decidability of satisfiability for BSR(SLR) clause sets

For the rest of this section we fix two positive integers m, m > 0 and some finite BSR(SLR) clause set N in normal form. For the sake of simplicity, we assume that all uninterpreted predicate symbols P occurring in N have the sort P : S m × R m . This assumption does not limit expressiveness, as the arity of a predicate symbol P can easily be increased in an (un)satisfiability-preserving way by padding the occurring atoms with additional arguments. For instance, every occurrence of atoms P (t 1 , . . . , t m ) can be replaced with P (t 1 , . . . , t m , v, . . . , v) for some fresh variable v that is added sufficiently often as argument.

Given the BSR(SLR) clause set N , every interpretation A induces a partition of R into finitely many intervals: the interpretations of all the rational and Skolem constants c occurring in N yield point intervals that are interspersed with and enclosed by open intervals.

Definition 5 (A-induced partition of R).

Let A be an interpretation and let r 1 , . . . , r k be all the values in the set {c A | c ∈ bconsts(N )} in ascending order. By J A we denote the following partition of R:

J A := (-∞, r 1 ), [r 1 , r 1 ], (r 1 , r 2 ), [r 2 , r 2 ], . . . , (r k-1 , r k ), [r k , r k ], (r k , +∞) .
The idea of the following equivalence is that equivalent tuples are indistinguishable by the constraints that we allow in the BSR(SLR) clause set N . Definition 6 (J A -equivalence, ∼ J A ). Let A be an interpretation and let k be a positive integer. We call two k-tuples r, q ∈ R k J A -equivalent if (i) for every J ∈ J A and every i, 1 ≤ i ≤ k, we have r i ∈ J if and only if q i ∈ J and (ii) for all i, j, 1 ≤ i, j ≤ k we have r i < r j if and only if q i < q j . The induced equivalence relation on tuples of positive length is denoted by ∼ J A .

For every positive k the relation ∼ J A induces only finitely many equivalence classes on the set of all k-tuples over the reals. We intend to show that, if N is satisfiable, then there is some model A for N which does not distinguish between different J A -equivalent tuples. First, we need some notion that reflects how the interpretation A treats a given tuple r ∈ R m . This role will be taken by the coloring χ A , which maps r to a set of expressions of the form P ā, where P is some predicate symbol occurring in N and ā is an m -tuple of domain elements from S A . The presence of P ā in the set χ A (r) indicates that A interprets P in such a way that P A contains the pair ā, r . In this sense, χ A (r) comprises all the relevant information that A contains regarding the tuple r.

Definition 7 (A-coloring χ A ). Given an interpretation A, let S := {a ∈ S A | a = c A for some c ∈ fconsts(N )} be the set of all domain elements assigned to free-sort constant symbols by A. The A-coloring of R m is the mapping χ A : R m → P{P ā | ā ∈ S m and P is an uninterpreted predicate symbol in N } defined such that for every r ∈ R m we have P ā ∈ χ A (r) if and only if ā, r ∈ P A .

Having the coloring χ A at hand, it is easy to formulate a uniformity property for a given interpretation A. Two tuples r, r ∈ R m are treated uniformly by A, if the colors χ A (r) and χ A (r ) agree. Put differently, A does not distinguish r from r .

Definition 8 (J A -uniform interpretation). An interpretation A is J A -uniform if χ A colors each and every ∼ J A -equivalence class uniformly, i.e. for all ∼ J A -equivalent tuples r, r we have χ A (r) = χ A (r ).

We next show that there exists a J B -uniform model B of N , if N is satisfiable. Since such a model does not distinguish between J B -equivalent m-tuples, and as there are only finitely many equivalence classes induced by ∼ J B , only a finite amount of information is required to describe B. This insight will give rise to a decision procedure that nondeterministically guesses how each and every equivalence class shall be treated by the uniform model.

Given some model A of N , the following lemma assumes the existence of certain finite sets Q i with a fixed cardinality which are subsets of the open intervals in J A . All J A -equivalent m-tuples that can be constructed from the reals belonging to the Q i are required to be colored identically by χ A . The existence of the Q i is the subject of Lemma 10. Lemma 9. Let λ be the maximal number of distinct base-sort variables in any single clause in N . In case of λ < m, we set λ := m. Let A be a model of N . Let J 0 , . . . , J κ be an enumeration of all open intervals in J A sorted in ascending order. Moreover, let r 1 , . . . , r κ be all reals in ascending order that define point intervals in J A , i.e. J 0 < [r 1 , r 1 ] < J 1 < . . . < [r κ , r κ ] < J κ . Suppose we are given a collection of finite sets Q 0 , . . . , Q κ possessing the following properties:

(i) Q i ⊆ J i and |Q i | = λ for every i. (ii) Let Q := i Q i ∪ {r 1 , . . . , r κ }. For all J A -equivalent m-tuples q, q ∈ Q m we have χ A (q) = χ A (q ).
Then we can construct a model B of N that is J B -uniform and that interprets the free sort S as a finite set.

Proof sketch. Claim I: Let µ be a positive integer with µ ≤ λ. Every ∼ J A -equivalence class over R µ contains some representative lying in Q µ . ♦ Let S denote the set {a ∈ S A | a = c A for some c ∈ fconsts(N )}. We construct the interpretation B as follows: S B := S; c B := c A for every constant symbol c; for every uninterpreted predicate symbol P and for all tuples ā ∈ S m and s ∈ R m we pick some tuple q ∈ Q m with q ∼ J A s, and we define P B so that ā, s ∈ P B if and only if ā, q ∈ P A . By construction, B is J B -uniform. It remains to show B |= N . Consider any clause C = Λ Γ → ∆ in N and let β be any variable assignment ranging over S B ∪ R. Starting from β, we derive a special variable assignment β C as follows. Let x 1 , . . . , x be all basesort variables in C. By Claim I, there is some tuple q 1 , . . . , q ∈ Q such that q 1 , . . . , q ∼ J A β(x 1 ), . . . , β(x ) . We set β C (x i ) := q i for every x i . For all other base-sort variables, β C can be defined arbitrarily. For every free-sort variable u we set β C (u) := β(u).

As In order to show that uniform models always exist for satisfiable clause sets N , we still need to prove the existence of the sets Q i mentioned in Lemma 9.

Lemma 10. Let A be an interpretation. Let r 1 , . . . , r κ be all the reals defining point intervals in J A and let J 0 , . . . , J κ be all open intervals in J A such that

J 0 < [r 1 , r 1 ] < J 1 < [r 2 , r 2 ] < . . . < J κ-1 < [r κ , r κ ] < J κ .
Let λ be a positive integer. There is a collection of finite sets Q 0 , . . . , Q κ such that Requirements (i) and (ii) of Lemma 9 are met.

Proof sketch. We employ a more sophisticated variant of the Ramsey result stated in Lemma 4. Claim I: There are sets Q 0 , . . . , Q κ satisfying Requirement (i) of Lemma 9 and the following conditions. For every Q i , 0 ≤ i ≤ κ, let s i,1 , . . . , s i,λ be all the values in Q i in ascending order. Moreover, we set s κ+i,1 := r i for every i with 1 ≤ i ≤ κ. Then, for every mapping : [m] → {0, . . . , 2κ} × [m] we have χ A (s (1) , . . . , s (m) ) = χ A (s (1) , . . . , s (m) ). ♦

One can show that for every ∼ J A -equivalence class S over R m there is some mapping : [m] → {0, . . . , 2κ} × [m] such that (1) whenever (i) = k, with k > κ + 1 then = 1, and (2) for all ascending tuples s0 = s 0,1 , . . . , s 0,m ∈ J m 0 ; . . . ; sκ = s κ,1 , . . . , s κ,m ∈ J m κ ; sκ+1 = r κ+1,1 = r 1 ; . . . ; s2κ = s 2κ,1 = r κ we have s (1) , . . . , s (m) ∈ S, and (3) for every tuple q 1 , . . . , q m ∈ S there exist ascending tuples s1 , . . . , s2κ defined as in ( 2) such that q 1 , . . . , q m = s (1) , . . . , s (m) .

Consider any q, q ∈ S. By (2), q can be written into s (1) , . . . , s (m) for appropriate values s k, and q can be represented by s (1) , . . . , s (m) for appropriate

s k, . Claim I entails χ A (q) = χ A ( s (1) , . . . , s (m) ) = χ A ( s (1) , . . . , s (m) ) = χ A (q ).
Lemmas 9 and 10 together entail the existence of some J A -uniform model A |= N with a finite free-sort domain S A , if N is satisfiable.

Corollary 11.

If N has a model, then it has a model A that is J A -uniform and that interprets the sort S as some finite set.

Given any interpretation A, the partition J A of the reals is determined by the rational constants in N and by the values that A assigns to the base-sort Skolem constants in N . Let d 1 , . . . , d λ be all the base-sort Skolem constants in N . If we are given some mapping γ : {d 1 , . . . , d λ } → R, then γ induces a partition J γ , just as A induces J A . We can easily verify whether N has a model B that is compatible with γ (i.e. B assigns the same values to d 1 , . . . , d λ ) and that is J B -uniform. Due to the uniformity requirement, there is only a finite number of candidate interpretations that have to be checked.

Consequently, in order to show decidability of the satisfiability problem for finite BSR(SLR) clause sets in normal form, the only question that remains to be answered is whether it is sufficient to consider a finite number of assignments γ of real values to the Skolem constants in N . Recall that since N is in normal form, we can divide N into two disjoint parts N def and N such that all ground LA terms occurring in N are either (Skolem) constants or rationals. Moreover, every clause in N def constitutes a definition c = t of some Skolem constant c. As far as the LA constraints occurring in N are concerned, the most relevant information regarding the interpretation of Skolem constants is their ordering relative to one another and relative to the occurring rationals. This means, the clauses in N cannot distinguish two assignments γ, γ if (a) for every Skolem constant d i and every rational r occurring in N we have (a.1) γ(d i ) ≤ r if and only if γ (d i ) ≤ r, and (a.2) γ(d i ) ≥ r if and only if γ (d i ) ≥ r, and (b) for all d i , d j we have that γ(d i ) ≤ γ(d j ) if and only if γ

(d i ) ≤ γ (d j ).
This observation leads to the following nondeterministic decision procedure for finite BSR(SLR) clause sets in normal form:

Decidability of satisfiability for BSR(BD) clause sets

Similarly to the previous section, we fix some finite BSR(BD) clause set N in normal form for the rest of this section, and we assume that all uninterpreted predicate symbols P occurring in N have the sort P : S m × R m . Moreover, we assume that all base-sort constants in N are integers. This does not lead to a loss of generality, as we could multiply all rational constants with the least common multiple of their denominators to obtain an equisatisfiable clause set in which all base-sort constants are integers. We could even allow Skolem constants, if we added clauses stipulating that every such constant is assigned a value that is (a) an integer and (b) is bounded from above and below by some integer bounds. Dropping any of these two restrictions leads to an undecidable satisfiability problem. For the sake of simplicity, we do not consider Skolem constants in this section.

Our general approach to decidability of the satisfiability problem for finite BSR(BD) clause sets is very similar to the path taken in the previous section. Due to the nature of the LA constraints in BSR(BD) clause sets, the employed equivalence relation characterizing indistinguishable tuples has to be a different one. In fact, we use one equivalence relation κ on the unbounded space R m and another equivalence relation κ on the subspace (-κ -1, κ + 1) m for some positive integer κ. Our definition of the relations κ and κ is inspired by the notion of clock equivalence used in the context of timed automata (see, e.g., [START_REF] Alur | A Theory of Timed Automata[END_REF]).

Definition 13 (bounded region equivalence κ ). Let κ be a positive integer. We define the equivalence relation κ on (-κ -1, κ + 1) m such that we get r 1 , . . . , r m κ s 1 , . . . , s m if and only if the following conditions are met: (i) For every i we have r i = s i , and fr(r i ) = 0 if and only if fr(s i ) = 0. (ii) For all i, j we have fr(r i ) ≤ fr(r j ) if and only if fr(s i ) ≤ fr(s j ).

The relation κ induces only a finite number of equivalence classes over (-κ -1, κ + 1) m . Over R m , on the other hand, an analogous equivalence relation ∞ would lead to infinitely many equivalence classes. In order to overcome this problem and obtain an equivalence relation over R m that induces only a finite number of equivalence classes, we use the following compromise. Definition 14 (unbounded region equivalence κ ). Let κ be a positive integer. We define the equivalence relation κ on R m in such a way that r 1 , . . . , r m κ s 1 , . . . , s m holds if and only if (i) for every i either r i > κ and s i > κ, or r i < -κ and s i < -κ, or the following conditions are met: (i.i) r i = s i and (i.ii) fr(r i ) = 0 if and only if fr(s i ) = 0, and (ii) for all i, j (ii.i) if r i , r j > κ or r i , r j < -κ, then r i ≤ r j if and only if s i ≤ s j , (ii.ii) if -κ ≤ r i , r j ≤ κ, then fr(r i ) ≤ fr(r j ) if and only if fr(s i ) ≤ fr(s j ).

Obviously, the equivalence relations κ and κ coincide on the subspace (-κ, κ) m . Over (-κ -1, κ + 1) m the relation κ constitutes a proper refinement of κ . Figure 1 depicts the equivalence classes induced by κ and κ in a twodimensional setting for κ = 1. We need both relations in our approach. Definition 15 ( κ -uniform and κ -uniform interpretations). Let κ be a positive integer. Consider a interpretation A. We call A κ -uniform if its corresponding coloring χ A (cf. Definition 7) colors each κ -equivalence class over (-κ -1, κ + 1) m uniformly, i.e. for all tuples q, q ∈ (-κ -1, κ + 1) m with q κ q we have χ A (q) = χ A (q ). We call A κ -uniform if χ A colors each κ -equivalence class over R m uniformly.

The parameter κ will be determined by the base-sort constant in N with the largest absolute value. If κ is defined in this way, one can show that the LA constraints occurring in N cannot distinguish between two κ -equivalent m-tuples of reals. This observation is crucial for the proof of Lemma 16.

In order to prove the existence of κ -uniform models for satisfiable N , we start from some model A of N and rely on the existence of a certain finite set Q ⊆ [0, 1) of fractional parts. This set Q can be extended to a set Q ⊆ (-κ -1, κ + 1) by addition of the fractional parts in Q with integral parts k from the range -κ -1 ≤ k ≤ κ. Hence, Q contains 2(κ + 1) • |Q| reals. We assume that all κequivalent tuples s, s from Q m are treated uniformly by A. Put differently, we require χ A (s) = χ A (s ). We choose to formulate this requirement with respect to κ because of the more regular structure of its equivalence classes, which facilitates a more convenient way of invoking Lemma 4. Due to the fact that κ constitutes a refinement of κ on the subspace (-κ -1, κ + 1) m , and since for every κ -equivalence class S over R m there is some κ -equivalence class S ⊆ (-κ-1, κ+1) m such that S ⊆ S, we can use the color χ A (r) of representative m-tuples r constructed from Q to serve as a blueprint when constructing a κuniform model B.

Lemma 16. Let λ be the maximal number of distinct base-sort variables in any single clause in N ; in case of λ < m, we set λ := m. Let A be a model of N . Let κ be the maximal absolute value of any rational occurring in N ; in case this value is zero, we set κ := 1. Suppose we are given a finite set Q ⊆ [0, 1) of cardinality λ + 1 such that 0 ∈ Q and for all tuples r, s ∈ Q m , r κ s entails χ A (r) = χ A (s), where Q := q + k q ∈ Q and k ∈ {-κ -1, . . . , 0, . . . , κ} . Then we can construct a model B of N that is κ -uniform and that interprets the free sort S as a finite set.

Proof sketch. The construction of B from A is similar to the construction of uniform models outlined in the proof of Lemma 9.

Claim I: Let µ be a positive integer with µ ≤ λ. For every κ -equivalence class S over R µ and every r ∈ S there is some q ∈ S ∩ Q µ such that r κ q and for all i 1 , i 2 , i 3 with r i1 < -κ and r i2 > κ and -κ ≤ r i3 ≤ κ we have fr(q i1 ) < fr(q i2 ) < fr(q i3 ). ♦ Let S denote the set {a ∈ S A | a = c A for some c ∈ fconsts(N )}. We construct the interpretation B as follows: S B := S; c B := c A for every constant symbol c; for every uninterpreted predicate symbol P occurring in N and for all tuples ā ∈ S m and r ∈ R m we pick some tuple q ∈ Q m in accordance with Claim I-i.e. q satisfies r κ q-and define P B in such a way that ā, r ∈ P B if and only if ā, q ∈ P A .

Claim II: The interpretation B is κ -uniform. ♦ It remains to show B |= N . We use the same approach as in the proof for Lemma 9, this time based on the equivalence relation κ instead of ∼ J A .

We employ Lemma 4 to prove the existence of the set Q used in Lemma 16.

Lemma 17. Let A be an interpretation and let κ, λ be positive integers with λ ≥ m. There exists a finite set Q ⊆ [0, 1) of cardinality λ + 1 such that 0 ∈ Q and for all tuples s, s ∈ Q m , s κ s entails χ A (s) = χ A (s ), where Q := q + k q ∈ Q and k ∈ {-κ -1, . . . , 0, . . . , κ} .

Proof sketch. One can show that every κ -equivalence class S over (-κ -1, κ + 1) m can be represented by a pair of mappings : [m] → {0, 1, . . . , m} and σ : [m] → {-κ -1, . . . , 0, . . . , κ} such that (i) for any ascending tuple r 0 , r 1 , . . . , r m ∈ [0, 1) m+1 with r 0 = 0 we have r (1) + σ(1), . . . , r (m) + σ(m) ∈ S, and (ii) for every tuple s 1 , . . . , s m ∈ S there is an ascending tuple r 0 , r 1 , . . . , r m ∈ [0, 1) m+1 with r 0 = 0 such that s 1 , . . . , s m = r (1) + σ(1), . . . , r (m) + σ(m) .

Having an enumeration 1 , σ 1 , . . . , k , σ k of pairs of such mappings in which every κ -equivalence class over (-κ -1, κ + 1) m is represented, we construct a coloring χ : R m → P{P i ā | ā ∈ S m and P i occurs in N } k by setting

χ(r) := χ A r 1 (1) + σ 1 (1), . . . , r 1(m) + σ 1 (m) , . . . , χ A r k (1) + σ k (1), . . . , r k (m) + σ k (m)
for every tuple r = r 1 , . . . , r m ∈ (0, 1) m , where we define r 0 to be 0. By virtue of Lemma 4, there is a set Q ⊆ (0, 1) of cardinality λ such that all ascending tuples r 1 , . . . , r m ∈ Q m are assigned the same color by χ. Then Q := Q ∪ {0} is the sought set.

Lemmas 16 and 17 together entail the existence of κ -uniform models for finite satisfiable BSR(BD) clause sets, where κ is defined as in Lemma 16.

Corollary 18. Let κ be defined as in Lemma 16. If N is satisfiable, then it has a model A that is κ -uniform and that interprets the sort S as some finite set.

By virtue of Corollary 18, we can devise a nondeterministic decision procedure for finite BSR(BD) clause sets N . We adapt the decision procedure for BSR(SLR) as follows. Since base-sort Skolem constants do not occur in N , Steps (1), [START_REF] Bachmair | Refutational Theorem Proving for Hierarchic First-Order Theories[END_REF], and (3.3) are skipped. Moreover, Step (3.4) has to be modified slightly. The interpretations of uninterpreted predicate symbols need to be constructed in such a way that the candidate interpretation B is κ -uniform for κ := max {1} ∪ {|c| c ∈ bconsts(N )} .

Theorem 19. Satisfiability of finite BSR(BD) clause sets is decidable.

Formalizing reachability for timed automata

In this section we show that reachability for timed automata (cf. [START_REF] Alur | A Theory of Timed Automata[END_REF]) can be formalized using finite BSR(BD) clause sets. In what follows, we fix a finite sequence x of pairwise distinct clock variables that range over the reals. For convenience, we occasionally treat x as a set and use set notation such at x ∈ x, |x|, and P(x). A clock constraint over x is a finite conjunction of LA constraints of the form true, x c, or x -y c, where x, y ∈ x, c is an integer and ∈{<, ≤, =, =, ≥, >}. We denote the set of all clock constraints over x by cc(x). A timed automaton is a tuple Loc, 0 , x, inv ∈Loc , T , where Loc is a finite set of locations; 0 ∈ Loc is the initial location; inv ∈Loc is a family of clock constraints from cc(x) where each inv describes the invariant at location ; T ⊆ Loc × cc(x) × P(x) × Loc is the location transition relation within the automaton, including guards with respect to clocks and the set of clocks that are being reset when the transition is taken.

Although the control flow of a timed automaton is described by finite means, the fact that clocks can assume uncountably many values yields an infinite state space, namely, Loc×[0, ∞) |x| . Transitions between states fall into two categories: delay transitions , r → , r with r = r + t for some t ≥ 0 and . The operation r := r + t is defined by setting r i := r i + t for every i, and r := r[Z → 0] means that r i = 0 for every x i ∈ Z and r i = r i for every x i ∈ Z.

In [START_REF] Fietzke | Superposition as a Decision Procedure for Timed Automata[END_REF] Fietzke and Weidenbach present an encoding of reachability for a given timed automaton A in terms of first-order logic modulo linear arithmetic.

Definition 20 (FOL(LA) encoding of a timed automaton, [START_REF] Fietzke | Superposition as a Decision Procedure for Timed Automata[END_REF]). Given a timed automaton A := Loc, 0 , x, inv ∈Loc , T , the FOL(LA) encoding of A is the following clause set N A , where Reach is a (1 + |x|)-ary predicate symbol: the initial clause

x∈x x = 0 ∧ inv 0 [x] → Reach( 0 , x); delay clauses z ≥ 0 ∧ x∈x x = x + z ∧ inv [x ] Reach( , x) → Reach( , x ) for every location ∈ Loc; transition clauses g[x] ∧ x∈Z x = 0 ∧ x∈x\Z x = x ∧ inv [x ]
Reach( , x) → Reach( , x ) for every location transition , g, Z, ∈ T .

Corollary 4.3 in [START_REF] Fietzke | Superposition as a Decision Procedure for Timed Automata[END_REF] states that for any model of N A , every location ∈ Loc, and every tuple r ∈ R |x| we have A, [x →r] |= Reach( , x) if and only if A can reach the state , r from its initial configuration. Given any clock constraint ψ ∈ cc(x) and some location , the timed automaton A can reach at least one of the states , r with [x →r] |= ψ[x] from its initial configuration if and only if the clause set N A ∪ ψ[x] Reach( , x) → is unsatisfiable (cf. Proposition 4.4 in [START_REF] Fietzke | Superposition as a Decision Procedure for Timed Automata[END_REF]).

Next, we argue that the passage of time does not have to be formalized as a synchronous progression of all clocks. Instead, it is sufficient to require that clocks progress in such a way that their valuations do not drift apart excessively. Although this weakens the semantics slightly, reachability remains unaffected.

Lemma 21. Consider any delay clause

C := z ≥ 0 ∧ x∈x x = x + z ∧ inv [x ]
Reach( , x) → Reach( , x ) that belongs to the FOL(LA) encoding of some timed automaton A := Loc, 0 , x, inv ∈Loc , T . Let λ be some positive integer. Let M be a finite clause set corresponding to the following formula

ϕ := x1,x2∈x -λ≤k≤λ x 1 -x 2 ≤ k ↔ x 1 -x 2 ≤ k ∧ x 1 -x 2 ≥ k ↔ x 1 -x 2 ≥ k ∧ x∈x x ≥ x ∧ inv [x ]
Reach( , x) → Reach( , x ) .

For every λ -uniform interpretation A we have A, [x →r, x →r ] |= C for all tuples r, r ∈ [0, λ + 1) |x| if and only if A, [x →q, x →q ] |= M holds for all tuples q, q ∈ [0, λ + 1) |x| .

Our approach to decidability of BSR(BD)-satisfiability exploits the observation that the allowed constraints cannot distinguish between tuples from one and the same equivalence class with respect to λ , which induces only a finite number of such classes. Decidability of the reachability problem for timed automata can be argued in a similar fashion, using a suitable equivalence relation on clock valuations [START_REF] Alur | A Theory of Timed Automata[END_REF]. We refer to the induced classes of indistinguishable clock valuations over R |x| , which are induced by a given timed automaton A = Loc, 0 , x, inv ∈Loc , T , as TA regions of A. Figure 2 illustrates the TA regions for some timed automaton with two clocks and in which all integer constants have an absolute value of at most 2. For every TA region R ⊆ R 2 of such an automaton, there is at least one representative r ∈ R which lies in [0, 5) 2 . Let k be the maximal absolute value of any integer constant occurring in the invariants and the transition guards of A. Moreover, let x 1 , . . . , x be the clock variables in x. Consider a constraint of the form

ψ := x 1 -x 2 = k ∧ x 2 -x 3 = k ∧ . . . ∧ x -1 -x = k. We observe that ψ entails x 1 -x = ( -1) • k.
Of course, ψ can also be conjoined with the constraint x 1 < -k, say, which entails x < -k -( -1) • k. This example illustrates that one can combine several difference constraints x -y c over different clock variables in such a way that bounds are entailed which cannot be formulated with a single constraint u -v d with |d| ≤ k. However, all of these combined constraints can be equivalently represented with atomic constraints x -y c or x c, where |c| ≤ |x| • k.

In order to decide reachability for A, it is sufficient to consider a bounded subspace of R |x| . More precisely, there exists a computable integer λ, namely |x| • k, such that any valuation r of A's clocks can be projected to some valuation r ∈ [0, λ + 1) |x| that A cannot distinguish from r. In the subspace [0, λ + 1) |x| , A's TA regions coincide with (finite unions of) equivalence classes with respect to λ . In fact, the quotient [0, λ+1) |x| / λ constitutes a refinement of the division of [0, λ + 1) |x| into TA regions. Since any pair , r with r ∈ R for some TA region R is reachable if and only if all pairs , r with r ∈ R are reachable, any minimal model A of the encoding N A is λ -uniform (where minimality of A refers to the minimality of the set Reach A with respect to set inclusion). This is why Lemma 21 may focus on λ -uniform models.

This means, given the FOL(LA) encoding N A of A, we obtain a BSR(BD) encoding N A of reachability with respect to A in the following two steps: (1) Replace every delay clause in N A with a corresponding finite set of clauses M in accordance with Lemma 21, where we set λ := |x| • k.

(2) Conjoin the constraints 0 ≤ x ∧ x < κ for κ := λ + 1 = |x| • k + 1 to every constraint in which a base-sort variable x occurs. Since any λ+1 -uniform model of N A is λ -uniform over the subspace (-λ -1, λ + 1) |x| , Lemma 21 entails that N A faithfully encodes reachability for A.

Theorem 22. The reachability problem for a given timed automaton can be expressed in terms of satisfiability of a finite BSR(BD) clause set.

Discussion

We have shown that satisfiability for the clause fragments BSR(SLR) and BSR(BD) is decidable. Both fragments hierarchically combine the Bernays-Schönfinkel-Ramsey fragment over uninterpreted predicate symbols with restricted forms of linear arithmetic over the reals.

Since the syntax of BSR(SLR) allows only a very restricted form of arithmetic on universally quantified variables, this part of the fragment seems to reduce to the theory of (dense) orderings. Except for density, all characteristic properties of orderings (e.g. transitivity) are already definable in the non-extended BSR fragment. On the other hand, regarding existentially quantified variables-which appear in the form of Skolem constants-, BSR(SLR) allows linear arithmetic expressions without notable restrictions, as long as no universally quantified variables are involved in the arithmetic expressions, and as long as no existential quantifier lies within the scope of a universal quantifier. Unfortunately, a more liberal syntax quickly leads to undecidability, as already pointed out in Section 1.

With BSR(BD) we have investigated another decidable fragment that is a hierarchic combination of the Bernays-Schönfinkel-Ramsey fragment with restricted arithmetic over the reals. Since difference constraints have been of use in the analysis and verification of timed systems, the idea suggested itself that BSR(BD) may find applications in this area. Indeed, we have seen that reachability for timed automata can be expressed with BSR(BD), although not entirely in a straightforward fashion. To this end, we have slightly weakened the usual notion of synchronous progression of all clocks. Our modifications do not affect the reachability relation. It is to be expected that BSR(BD) lends itself to more sophisticated applications in the area of timed systems or other fields.

  A is a model of N , we get A, β C |= C. By case distinction on why A, β C |= C holds, one can infer B, β |= C. Consequently, B |= N .

( 1 )

 1 Nondeterministically fix a total preorder (reflexive and transitive) on the set of all base-sort Skolem constants and rational constants occurring in N . Define a clause set N that enforces for base-sort Skolem constants, i.e. N := c > c → c c , either c or c or both are Skolem constants . (2) Check whether there is some mapping γ : {d 1 , . . . , d λ } → R such that γ is a solution for the clauses in N def ∪ N . (This step relies on the fact that linear arithmetic over existentially quantified variables is decidable.) (3) If such an assignment γ exists, define an interpretation B as follows. (3.1) Nondeterministically define S B to be some subset of fconsts(N ), i.e. use a subset of the Herbrand domain with respect to the free sort S. (3.2) For every e ∈ fconsts(N ) nondeterministically pick some a ∈ S B and set e B := a. (3.3) Set d B i := γ(d i ) for every d i . (3.4) For every uninterpreted predicate symbol P occurring in N nondeterministically define the set P B in such a way that B is J B -uniform. (4) Check whether B is a model of N . Theorem 12. Satisfiability of finite BSR(SLR) clause sets is decidable.

Fig. 1 .

 1 Fig. 1. Left: partition of the set (-2, 2) 2 induced by 1. Right: partition of R 2 induced by 1. Every dot, line segment, and white area represents an equivalence class.

  [x →r ] |= inv [x ]; and location transitions , r → , r for some , g, Z, ∈ T with [x →r] |= g[x], r = r[Z → 0], and [x →r ] |= inv [x ]

Fig. 2 .

 2 Fig. 2. Partition of the set [0, ∞) 2 into classes of clock valuations that cannot be distinguished by a timed automaton with two clocks in which the absolute value of integer constants occurring in location invariants and transition guards does not exceed 2. Every dot, line segment, and white area represents an equivalence class.

  we write A(β)(s) to mean the value of the term s under A with respect to the variable assignment β. The variables occurring in clauses are implicitly universally quantified. Therefore, given a clause C, we call A a (hierarchic) model of C, denoted A |= C, if and only if A, β |= C holds for every variable assignment β. For clause sets N , we write A |= N if and only if A |= C holds for every clause C ∈ N . We call a clause C (a clause set N ) satisfiable if and only if there exists a model A of C (of N ). Two clauses C, D (clause sets N, M ) are equisatisfiable if and only if C (N ) is satisfiable whenever D (M ) is satisfiable and vice versa.

Acknowledgement The present author is indebted to the anonymous reviewers for their constructive criticism and valuable suggestions.