Éphane St

Demri

Concrete Domains in Logics: A Survey

In this short survey, we present logical formalisms in which reasoning about concrete domains is embedded in formulae at the atomic level. These include temporal logics with concrete domains, description logics with concrete domains as well as variant formalisms. We discuss several proof techniques to solve logical decision problems for such formalisms, including those based on constrained automata or on translation into decidable second-order logics. We also present recent results mainly related to decidability and complexity as well as a selection of open problems.

INTRODUCTION

Reasoning about concrete domains. A concrete domain is a relational structure with a fixed non-empty domain and a family of relations. Typical examples of concrete domains are (N; <), (P(N); ⊆), and the set of finite words over the alphabet {0, 1} * with the prefix relation. Multiple logical formalisms have been developed to express properties on concrete domains, ranging from quantifier-free languages to first-order languages. A prominent example is Presburger arithmetic [Pre29;Gr ä88;Haa18] understood as the first-order theory on the natural numbers with addition and the standard ordering relation. Other concrete domains are relevant in computer science, in particular those related to the verification of programs with typed variables (real numbers, finite binary trees, lists, etc.).

Reasoning about concrete domains embedded in logical formalisms can be materialised in at least two ways; combinations are also possible. One option is to keep the semantical structures of the plain logic but to enrich the logical language so that values in the concrete domains can be inferred from the models. This is what is done in [BEH95] in which a version of constrained LTL is introduced that is interpreted over standard LTL models but the logical language is enriched with Presburger constraints to reason about the number of occurrences of events in the models. Graded modal logics are of the same nature, see e.g. [Tob01], as the models are standard Kripke-style structures but the modal language can state constraints about the number of successor worlds satisfying a specific formula.

Another option is to enrich the semantical structures of the plain logic L with values from a concrete domain D (see e.g. [BH91]). The logic L(D) -L with the concrete domain D -can express constraints between these values thanks to atomic formulae that can compare these values. For instance, every position of an LTL-model can be associated with two natural numbers. In LTL(N; <), the atomic formula x < Xy expresses that the value of the variable x at the current position is strictly less than the value of y at the next position.

This paper is mainly dedicated to logical formalisms with concrete domains of the second kind, i.e., extensions of L in which the semantical structures of the plain logic are augmented with concrete values.

From ontologies to database-driven systems. Logical formalisms in which reasoning about concrete domains is embedded in formulae at the atomic level and the models are Kripke-style structures (transition systems, interpretations for description logics [BHLS17]) are quite ubiquitous in theoretical computer science. Usually, every world (state, domain element) is associated with a collection of values from concrete domains. For example, in timed logics [AH93; AH94; AFH96], states have a timestamp in R whereas in logics for the verification of counter automata, see e.g. [CC00; BQS19], every state comes with a tuple of counter values in N. This can be gener-alised to other specification languages for the behaviour of non-terminating programs by understanding valuation sequences as snapshots of program's variables at specific points of time during its execution. Similarly, in description logics with concrete domains handling ontologies with values from concrete domains, domain elements are enriched with tuples of values, see e.g. [BH91; Lut02b; Lut03; Lut04b; LM07]. Dealing with concrete domains in logics happens to be natural and further examples can be found in spatial-temporal logics [WZ00; BC02], in first-order temporal logics for modelling dynamical biological behaviours [FR09; Fag20], in synthesis problems [EFR21; CDOT21], for the verification of hierarchical systems [FK18] and for reasoning about sequences of memory states [BDL09]. Such logical formalisms have been also shown relevant for analysing database-driven systems [DHV14]. For instance, a variant of first-order LTL has been introduced in [DHV14] to verify data-driven web applications.

The expressive power of the plain logics augmented with constraints about concrete domains often allows us to encode counting mechanisms, leading to undecidability of the main reasoning tasks (satisfiability, model-checking), see e.g. [CC00; Lut02b]. However, properties of the concrete domains have been identified to get decidable logical problems, see e.g. [BC02; LM07; CKL16; BR20], and syntactic restrictions have been also elaborated to reduce the expressive power at the gain of having better computational properties, see e.g. [Laz11; BQS19].

Motivations. In view of the plethora of recent works dealing with logics with concrete domains and the diversity of proof methods and decision problems, we would like to provide a short survey about recent advances, in a uniform framework that allows us to compare the different techniques and contributions. Pinpointing the most promising research directions is an important motivation, too.

Content. In this paper, we present results about the decidability/complexity status of reasoning tasks for logics with concrete domains focusing on recent works as well as on the relationships between seemingly distinct formalisms. In Section 2.1, we introduce the notion of concrete domains, we provide examples and we state a few standard results in particular related to numerical domains and to string domains. The remaining part of Section 2 deals with the introduction of temporal and description logics equipped with concrete domains. The automata-based approach is described in Section 3, extending the approach for modal and temporal logics, see e.g. [VW86; VW94]. Decidability results obtained by translation into second-order theories are sketched in Section 4, following recent developments in [Car15; CKL16; CT16]. Comparisons with other proof techniques are also provided there. Whereas the previous sections mainly contain formalisms in which contraints between values from the concrete domains have a local scope, Section 5 presents richer logical formalisms with global constraints (including the use of the freeze operator, and its restriction to express value repetitions) and a selection of decidability/complexity results. Finally, Section 6 concludes the paper with a selection of open questions. Let us consider some examples of concrete domains. A generic concrete domain is (D; ≡), where D is an arbitrary set of data values and ≡ is an equivalence relation over D. We may extend this to (D; ≡, (= d ) d∈D ), where = d is a unary predicate stating the equality with the constant d (the singleton = d is also simply written d in concrete domains). Numerical concrete domains belong to the concrete domains probably studied the most in computer science. We mention here the integers (Z; +, <, =, 0, 1) that are used for analysing and reasoning about systems with integer variables [CC00; BQS19] and for representing infinite-state systems [Haa18]. Another example is the real numbers (R; <, =), used in the verification of real-timed systems [AH93; AH94; AFH96]. Concrete domains that can be used to reason about strings play a key role in the analysis of programs [HW12; AAC + 14; KS15; HSZ17]. Let A be a finite or infinite set of letters, in the following called the alphabet, and let A * denote the set of all finite strings over A. Given two finite strings u, v ∈ A * , we use u • v (often abbreviated by uv) to denote the concatenation of u and v. The pair (A * ; •), where • is a ternary relation interpreted as concatenation, is an example of a concrete domain with domain A * . There are many interesting partial orders that can be used to form concrete domains with domain A * ; we mention here the following ones. A subsequence of a string v ∈ A * is a string u that is obtained from v by removing any letters from v; in that case we write u< seq v. If u is contiguous, we call u a subword of v, and write u < sbwd v. The prefix < pre and suffix < suf relations are special cases of the subword order, with the obvious respective meanings.

LOGICAL FORMALISMS WITH CONCRETE DOMAINS

Concrete domains and constraints

Concrete

Constraints. Let VAR = {x, y, . . .} be a countable set of variables. A term over VAR is an expression of the form X i x, where x ∈ VAR and X i is a (possible empty) sequence of i symbols X. A term X i x should be understood as a variable (that needs to be interpreted) but, later on, we will see that the prefix X i will have a temporal interpretation. We write T VAR to denote the set of all terms over VAR. For all i ∈ N, we write T ≤i VAR to denote the subset of terms of the form X j x, where j ≤ i. For instance, T ≤0 VAR = VAR. Constraints are defined over a concrete domain and a set T ⊆ T VAR of terms. Let D be a concrete domain over a relational signature σ. An atomic constraint c over D and T is an expression of the form R(t 1 , . . . , t d ), where R ∈ σ of arity d and t i ∈ T , for all 1 ≤ i ≤ d. A constraint C is defined as a (finite) Boolean combination of atomic constraints; we use ∧, ∨ and ¬ for the standard Boolean connectives. Constraints are interpreted on valuations v : T → D that assign elements from D to the terms in T , so that v satisfies R(t 1 , . . . , t d ), written v |= R(t 1 , . . . , t d ), if and only if, (v(t 1 ), . . . , v(t d )) ∈ R D . The Boolean connectives are interpreted in the usual way. A constraint C over D and T is satisfiable

def ⇔ there is a valuation v : T → D such that v |= C. Similarly, a constraint C 1 entails a constraint C 2 (written C 1 |= C 2 ) def ⇔ for all valuations v, we have v |= C 1 implies v |= C 2 .
In this document, most of the logics are based on concrete domains whose satisfiability problem restricted to finite conjunctions of atomic constraints can be solved in NP, if not in PTIME.

Models with concrete domains

In order to define logics with concrete domain D, the semantical structures of such logics (typically, Kripke-style structures) are enriched with valuations that interpret the variables of the logic by elements of the concrete domain.

Kripke structures. Let PROP = {p, q, . . .} be a countably infinite set of propositional variables. A Kripke structure K is a triple (W, R, l), where W is a set of worlds, R ⊆ W× W is the accessibility relation and l : W → P(PROP) is a labelling function. A Kripke structure K is total whenever for all w ∈ W, there is w ∈ W such that (w, w ) ∈ R. Totality is a standard property for defining classes of models for temporal logics such as CTL * . For instance, an LTL model K = (W, R, l) is a Kripke structure where (W, R) is isomorphic to (N; succ), where succ is the successor relation on N. Given a Kripke structure K = (W, R, l) and a world w ∈ W, an infinite path π from w is an ω-sequence w 0 , . . . , w n , . . . such that w 0 = w and for all i ∈ N, we have (w i , w i+1 ) ∈ R. Finite paths are defined accordingly. Decorated Kripke structures. A D-decorated Kripke structure K is a structure of the form (D, W, R, l, v) such that D = (D; σ) is a concrete domain, (W, R, l) is a Kripke structure and v : W × VAR → D is a valuation function. A D-decorated Kripke structure can be understood as a plain Kripke structure in which to each world is associated a valuation interpreting the variables from VAR by elements in D. We may omit the labelling function l from K if there is no need for propositional labelling (as in Section 2.3). Similarly, D might be omitted if it is clear from the context. Note also that numerous variants exist for the above definition, for instance one may admit a family of accessibility relations (instead of a single one) or consider disjoint sets of variables interpreted in distinct concrete domains (instead of a single concrete domain).

Temporal logics with concrete domains

We introduce temporal logics with concrete domains of the form LTL(D) and CTL * (D), naturally extending what is known for the temporal logics LTL and CTL * . Other options are possible and some are evoked in the document, but these two cases allow us to illustrate the main features.

Linear case. We write LTL(D) to denote the variant of LTL for which models are D-decorated Kripke structures with underlying LTL models. LTL(D) formulae are defined below; in short, propositional variables from LTL are replaced by atomic constraints over D and T VAR . The set of LTL(D)-formulae is defined as follows.

φ ::= R(t 1 , . . . , t d ) | φ ∧ φ | ¬φ | Xφ | φUφ,
where t i is a term in T VAR , and R ∈ σ is of arity d. The temporal operators X and U are interpreted as in LTL. Note that the symbol 'X' is overloaded here (temporal operator and operator in the terms to access future variable values) but this should not cause any confusion in the sequel. Other standard operators like →, or the temporal operators sometimes F and always G can be defined in the usual way.

An LTL(D) model is a map of the form v : N × VAR → D. Given an LTL(D) model v, we write v(i, X j x) to denote the value v(i + j, x) ∈ D. The satisfaction relation |= for LTL(D) is defined as follows (i ∈ N).

-v, i |= R(t 1 , . . . , t d ) def ⇔ (v(i, t 1 ), . . . , v(i, t d )) ∈ R D , -v, i |= φ ∧ ψ def ⇔ v, i |= φ and v, i |= ψ; v, i |= ¬φ def ⇔ not v, i |= φ, -v, i |= Xφ def ⇔ v, i + 1 |= φ, -v, i |= φUψ def ⇔ there is j ≥ i s.t. v, j |= ψ and for all j ∈ [i, j -1], we have v, j |= φ.
As usual, φ is satisfiable iff there is a model v such that v, 0 |= φ. Note that given an atomic constraint R(t 1 , . . . , t d ) such that t j = X mj x j for all j and M = max{m 1 , . . . , m d }, the satisfaction of v, i |= R(t 1 , . . . , t d ) only depends on the values of the variables x 1 , . . . , x d at the positions i, . . . , i + M (understood as a finite path).

Recall that satisfiability for LTL is . A natural question is whether solving the satisfiability problem for LTL(D), denoted by SAT(LTL(D)), is computationally more complex than for plain LTL; obviously, this depends on D. In comparison with plain LTL, new constraints between variable values need to be satisfied due to the interpretation to the specific concrete domain D. Moreover, as terms can refer to the values of variables at the next position, the propagation of constraints may lead to a possibly infinite "network" of constraints (known as constraint graphs, see e.g. [Lut04a; DD07; LOS20]). For instance, in LTL(N; <), no infinite sequence of variables with strictly decreasing values is admitted; so G(x > Xx) is not satisfiable. Considering another concrete domain, the formula 0

• x = Xx → X(1 • x = Xx) in LTL({0, 1} * ; 0•, 1•)
where 0• is a binary relation concatenating the letter 0 (similarly for 1•). is interpreted by "If 0 is popped from the 'stack' x, then at the next step 1 is pushed onto it."

One of the first results established for LTL(D) can be found in [BC02], where SAT(LTL(R; <, =)) and SAT(LTL(Q; <, =)) are shown in PSPACE by adapting the proof method from [SC85] to decide LTL satisfiability in PSPACE. In [DD07; ST11], conditions generalising the above result are identified that guarantee a PSPACE upper bound. Besides, SAT(LTL({0, 1} * ; < pre , =)) is in PSPACE, too (see e.g. [KW15; DD16]) although ({0, 1} * ; < pre , =) and (Q; <, =) are quite different structures. When a concrete domain D is able to encode a counting mechanism, LTL(D) becomes quite expressive, for instance SAT(LTL(N; succ, =)) is undecidable [CC00]. A natural question is which properties of D make SAT(LTL(D)) decidable, or even better in PSPACE. We shall see that several answers have been proposed in the literature.

Branching case. Next, we introduce the temporal logic CTL * (D) understood as the branching-time extension of LTL(D). State formulae φ and path formulae Φ of CTL * (D) are defined below

φ := ¬φ | φ ∧ φ | EΦ Φ := φ | R(t 1 , . . . , t d ) | ¬Φ | Φ ∧ Φ | XΦ | ΦUΦ,
where t i is a term in T VAR , and R ∈ σ is of arity d. State formulae are interpreted on worlds from a D-decorated Kripke structure, whereas path formulae are interpreted on LTL(D) models (or, equivalently, on infinite paths from D-decorated Kripke structures). The two satisfaction relations are defined as follows (we omit the standard clauses for Boolean connectives), where K = (D, W, R, v) is a total D-decorated Kripke structure, w ∈ W, and π is an infinite path of K.

-K, w |= EΦ def ⇔ there is an infinite path π starting from w such that K,

π |= Φ, -K, π |= R(t 1 , . . . , t d ) def ⇔ (v(π(0), t 1 ), . . . , v(π(0), t d )) ∈ R D , where v(π(0), X j x) def = v(w j , x) with w j the jth world of π, -K, π |= XΦ def ⇔ K, π[1, +∞[|= Φ, where for any n, π[n, +∞[ is the suffix of π truncated by the n first worlds, -K, π |= ΦUΨ def ⇔ there is j ≥ 0 such that K, π[j, +∞[|= Ψ and for all j ∈ [i, j -1], we have K, π[j , +∞[|= Φ.
Several results from [BC02] can can be adapted to the branching case for a quite large family of concrete domains, see e.g. [Gas09]. For instance, SAT(CTL * (R; <, =)) and SAT(CTL * (Q; <, =)) are in 2EXPTIME (see also Section 3.3). Decidability of strict fragments of CTL * (Z; <, =, (= n ) n∈Z ) is shown in [BG06; Gas07]. It is only recently in [Car15; CKL16] that decidability has been established for the full logic using a translation into a decidable second-order logic (details are provided in Section 4).

THEOREM 2.1 ([CKL16]). SAT(CTL * (Z; <, =, (= n ) n∈Z )) is decidable.
The proof of Theorem 2.1 does not provide a sharp complexity upper bound and actually apart from determining the decidability status of logics of the form CTL * (D), characterising the computational complexity is a general issue too. By contrast, SAT(LTL(Z; <, =, (= n ) n∈Z )) is known to be in PSPACE [DG08; ST11] (with integers encoded in binary). In order to conclude this section, we would like to note that it is also possible to define logics of the form LTL(∆) or CTL * (∆) where ∆ is a class of concrete domains instead of a fixed concrete domain D as in CTL * (D). For instance, in [Car15; CKL16], the class of semi-orders is taken for ∆.

DL notation TL notation concept name

A; concept ∃r.C prop. variable p; formula EXr φ path constraint ∃P. R(S i 1 x1, . . . , S i d x d ) [CT16] atomic constraint EP. R(X i 1 x1, . . . , X i d x d ) concept ∃p1, . . . , p d . R(x1, . . . , x d ) [BR20] atomic constraint R(EP1 x1, . . . , EP d x d )

Description logics with concrete domains

Concrete domains are also handled in description logics by adding concrete values in ontologies, following the seminal work [BH91]. Since [Sch91], correspondences between modal logics and description logics are well identified and this applies also to relationships with temporal logics. Below, we present several ways to consider concrete domains in description logics. To avoid the introduction of too lengthy definitions, we present the new logics following the way the logics LTL(D) and CTL * (D) have been already defined (we limit ourselves to a selection of typical features). Figure 2.4 contains a table with the appropriate syntactic correspondences dedicated to the readers that are fluent in description logics lingua. Apart from the gain of space, this should facilitate any comparison with temporal logics with concrete domains.

We adapt and extend several definitions introduced so far. Given a set N R = {r, s, . . .} of role names, the notion of D-decorated Kripke structure is generalised to structures of the form (D, W, (R r ) r∈N R , l, v). Instead of having a single accessibility relation, the D-decorated Kripke structures now admit a family of accessibility relations indexed by role names r ∈ N R . A role path P = r 1 • • • r n is a (possibly empty) word in N * R . Sometimes, role paths admit abstract features that are role names interpreted by deterministic relations, see e.g. [Lut01]. Herein, we do not consider such role names (except in Section 3.3).

Let us recall how concrete values and constraints between them are considered in LTL(D) and CTL * (D). An atomic constraint R(X i1 x j1 , . . . , X i d x j d ) holds at a position i ∈ N along the path π understood as an ω-sequence of valuations, whenever R D (π(i + i 1 )(x j1 ), . . . , π(i + i d )(x j d )) holds. Hence, only the values for the variables x j1 , . . . , x j d at the positions i, i + 1, . . . , i + max(i 1 , . . . , i d ) determine whether R(X i1 x j1 , . . . , X i d x j d ) holds true. Moreover, R(X i1 x j1 , . . . , X i d x j d ) is always evaluated along a path: in LTL(D) because the models are linear structures, and in CTL * (D) because R(X i1 x j1 , . . . , X i d x j d ) always occurs in the scope of a path quantifier E. In description logics with concrete domains, at least two generalisations are performed. Firstly, there are multiple accessibility relations (interpretations of role names) and it is possible to specify that a finite path is defined by taking steps from distinct relations using role paths. Secondly, values picked to satisfy an atomic constraint may be taken from a finite rooted subtree instead of a (linear) path. Both extensions are substantial and require to extend the way constraints are defined.

The set of ALC (D)-formulae (' ' for 'linear') is defined as follows.

φ ::= p | EP R(t 1 , . . . , t d ) | φ ∧ φ | ¬φ | EX r φ,
where p ∈ PROP, t i is a term, P is a role path, R ∈ σ is of arity d and r is a role name.

We have the additional proviso that in EP R(t 1 , . . . , t d ), if t i = X α x, then α ≤ |P | with |P | the length of P (possibly zero), otherwise we would not know how to interpret t i . The satisfaction relation is defined as follows (obvious clauses are omitted).

-

K, w |= p def ⇔ p ∈ l(w); -K, w |= EX r φ def ⇔ there is w ∈ R r (w) such that K, w |= φ, -K, w |= Er 1 • • • r n R(t 1 , . . . , t d ) def ⇔ there is a finite path w = w 0 R r1 w 1 R r2 • • • R rn w n such that R(d 1 , . . . , d d ) holds with d i def = v(w j , x) assuming that t i = X j x for all i.
Logics of the form ALC (D) can be found in [CT16; LOS20], and these are probably the closest variants to LTL(D)/CTL * (D). An axiom is an expression of the form φ ψ where φ, ψ are ALC (D) formulae. A terminological box (TBox, for short) is a set of axioms. We say that K satisfies φ ψ (written K |= φ ψ) iff for every w ∈ W, K, w |= φ implies K, w |= ψ; this generalises to TBoxes in the expected way. The satisfiability problem w.r.t. a TBox, written TSAT(ALC (D)) takes as input an ALC (D)-formula φ and a finite TBox T , and asks whether there exist a D-decorated Kripke structure K and w ∈ W such that K, w |= φ and K |= T . It is well known that decision problems for description logics are quite diverse, herein we have picked one that is a good representative.

THEOREM 2.2 ([CT16; LOS20]). TSAT(ALC (Z; <, =, (= n ) n∈Z )) is in EXPTIME (with integers encoded in unary).
Now, let us define the description logics ALC t (D), variants of ALC (D) in which the values in constraints are extracted from tree-like structures. The set of ALC t (D)formulae is defined from

φ ::= p | R(EP 1 x 1 , . . . , EP d x d ) | φ ∧ φ | ¬φ | EX r φ,
where the P j 's are role paths, R ∈ σ is of arity d and r is a role name. Unlike in ALC (D), each variable within an atomic constraint comes with a (possibly distinct) role path. The satisfaction relation |= is updated as follows.

-

K, w |= R(EP 1 x 1 , . . . , EP d x d ) def ⇔ for all j ∈ [1, d], assuming P j = r 1 • • • r n , there is a finite path π = w j 0 R r1 w j 1 R r2 • • • R rn w j n with d j = v(w j n , x j ), and R D (d 1 , . . . , d d ) holds.
Logics of the form ALC t (D) can be found in [Lut01; LM07; BR20] and this is probably the variant that is the most common for description logics, see also [Lut02a; Lut04a] and the original proposal for description logics with concrete domains in [BH91]. Atomic constraints of the form R(AP 1 x 1 , . . . , AP d x d ) with universal quantifications over values instead can be found in [LM07] but are not developed herein. Similarly, the language can be extended to admit Boolean combinations in the scope of quantification over role paths as in [LOS20; BR20].

In [LM07], ω-admissible concrete domains D are introduced for which a very general decidability result is proved. ω-admissibility implies that the signature σ contains a finite set of binary relations with additional properties, namely:

(1) Satisfiability problem for D-constraints is decidable.

(2) D satisfies the patchwork property, meaning roughly that two satisfiable finite sets of constraints agreeing on common variables admit a satisfiable union. A similar property can be found in [BC02], see condition ( † †) in Section 3.2.2. (3) D satisfies a compactness property, meaning roughly that an infinite set of constraints is satisfiable iff any finite subset is satisfiable.

THEOREM 2.3 ([LM07]

). For any ω-admissible concrete domain D, TSAT(ALC t (D)) is decidable.

By way of example, (R; <, =) and (Q; <, =) are ω-admissible (see an early work on (Q; <, =) in [Lut01]), whereas (N; <, =) is not. Besides, [BR20] provides a new definition for ω-admissibility, with conditions using model-theoretical characterisations.

A selection of other formalisms

In this section we shortly present some related formalisms. We start by giving a quick summary about classical first-order (FO) logics. One of the most widely used results is the decidability of the FO theory over (N; +, <, =, 0, 1), nowadays commonly known as Logics of the form LTL(D) have been extended or adapted in order to design logical formalisms for the verification of database-driven systems, see e.g. [DHPV09; DHV14]. For instance, LTL-FO is an extension of LTL obtained by replacing propositional variables by quantifier-free FO formulae about tuples in the underyling database (an overview can be found in [DHV14]). Moreover, universal quantification for variables is also considered, providing similarities with the freeze operator, see e.g. [DHV14, Section 3] and Section 5. As for LTL(D), the difficulty for reasoning with LTL-FO rests on the infinite domain from which the data values are taken. Decidability results with a linearly ordered dense data domain can be found in [DHPV09]. Besides, separation logics with data, see e.g. [BBL09; KJW18] are logical formalisms involving concrete domains, but this cannot be developed further here.

Constraints also appear in constraint satisfaction problems (CSPs) [Bod20]. A CSP is a computational problem parameterized by a concrete domain, similarly to the logics defined above. Formally, a CSP over a concrete domain D = (D; σ) is the problem of deciding, given a relational structure A over the same signature σ, whether there exists a homomorphism from A to D. In terms of logic, a CSP can be seen as finite conjunction of constraints R(x 1 , . . . , x d ), where x i is a variable. The main focus of research in the area of CSP is the study of the computational complexity of CSPs. For finite-domain CSPs there has recently been a major breakthrough achieved by the confirmation [Bul17; Zhu17] of the twenty-year-old dichotomy conjecture by Feder and Vardi [Bul18], stating that every CSP over a finite domain can be solved efficiently or is NP-hard. Ongoing research attempts to generalize methods (based on universal algebra, model theory, and graph homomorphisms) from finite-domain CSP to infinite domains [Bod20].

AUTOMATA-BASED APPROACH

In this section, we present the automata-based approach for solving decision problems for logics with concrete domains L(D) by extending the approach followed in seminal works, for instance for MSO logic [B üc62] and for temporal logics, see e.g. [VW94; KVW00]. In short, this approach consists of reducing logical problems (satisfiability, model-checking) to automata-based decision problems while taking advantage of existing results and decision procedures from automata theory, see e.g. [VW07]. Below, we present the main steps for solving satisfiability and model-checking problems for L(D) thanks to so-called D-automata (see Section 3.1). Actually, the mate-rial presented below is quite orthodox in view of the automata-based approach for temporal/description/modal logics. However, solving the nonemptiness problem for Dautomata can be trickier than for automata defined on finite alphabets. Indeed, the elements of the concrete domain D can be much more constrained than letters from a finite alphabet. For many concrete domains, nonemptiness of D-automata can be reduced directly to instances of similar problems for automata on finite alphabets (see [Lut01; Lut04a; DD07]). For a lot of other concrete domains, specific developments about D-automata need to be provided (see e.g. [BG06; ST11; KW15]).

k def = {x 1 , . . . , x k } ∪ {Xx 1 , . . . , Xx k }.
The language L(A) accepted by A is a set of sequences of valuations v of the form {x 1 , . . . , x k } → D. As usual, depending on the type of D-automata (finite, B üchi, etc.) the length of the accepted sequences/words varies. For instance, given a B üchi Dautomaton A (the understanding by default herein),

v 0 v 1 • • • ∈ L(A) iff there is an infinite run q 0 C0 -→ q 1 C1 -→ • • • such that -for all i ∈ N, q i Ci - → q i+1 ∈ δ and [x j ← v i (x j ), Xx j ← v i+1 (x j )] |= C i .
q 0 ∈ I and there is some q ∈ F that occurs infinitely often in q 0 q 1 q 2 • • • .

The nonemptiness problem for D-automata, written NEP(D), takes as input a Dautomaton A and asks whether L(A) = ∅. This is a classical problem in automata theory, apart from being strongly related to satisfiability in temporal logics [VW07].

Linear-time temporal logics LTL(D)

3.2.1. The standard translation in a nutshell. We explain how to construct from a given LTL(D)-formula φ a D-automaton A φ such that L(A) corresponds to the models of φ. We fix a concrete domain D = (D; R 1 , . . . , R n ) over a finite signature and an LTL(D) formula φ whose terms are among T ≤1 k , for some k ∈ N. More general terms, such as X 3 x, could be handled in a similar fashion or eliminated if equality is part of D. Similarly, assuming the finiteness of the signature σ is not a serious restriction as a given formula always contains a finite amount of predicates. Details are omitted herein and these assumptions are intended to simplify the presentation of the approach.

We write AC k to denote the finite set of atomic constraints built over the terms in T ≤1

k . Let cl(φ) be the closure set of φ defined as the smallest set containing AC k ∪ {φ}, closed under subformulae and negation (double negations are eliminated), and if ψ 1 Uψ 2 ∈ cl(φ), then X(ψ 1 Uψ 2 ) ∈ cl(φ). Let A φ = (S, δ, I, F 1 , . . . , F α ) be the D-automaton with k variables defined as follows (generalised B üchi acceptance F 1 , . . . , F α can be easily reduced to B üchi acceptance).

-S is the set of subsets of cl(φ) that are propositionally maximally consistent, and if Y ∈ S, then for all ψUϕ ∈ cl(φ), we have ψUϕ

∈ Y iff ϕ ∈ Y or ψ, X(ψUϕ) ∈ Y . -I def = {Y ∈ S | φ ∈ Y }. -For all Y, Y ∈ S, we have Y C - → Y ∈ δ def ⇔ C = ( c∈Y ∩AC k c) ∧ ( c∈(AC k \Y ) ¬c) and for all Xψ ∈ cl(φ), we have Xψ ∈ Y iff ψ ∈ Y . -Let {ψ 1 Uϕ 1 , . . . , ψ α Uϕ α } be the set of until formulae in cl(φ). For all i ∈ [1, α], we have F i def = {Y ∈ S | ψ i Uϕ i ∈ Y or ϕ i ∈ Y }.
By using standard arguments for LTL from [VW94] and the notion of accepted language for a D-automaton, we can show the following result.

THEOREM 3.1. L(A φ ) = {v : N × {x 1 , . . . , x k } → D | v, 0 |= φ}.
The construction of A φ works for all concrete domains D; hence one can decide the satisfiability of φ by deciding the nonemptiness of L(A φ ).

One way to check nonemptiness of L(A φ ) is to see A φ as the product of an "LTLcomponent" dealing with the temporal requirements on the one side, and a "Dcomponent" dealing with the satisfiability of ω-sequences made of conjunctions of atomic constraints on the other side. In that context, a symbolic representation for LTL(D) models is essential. This is explained below with the introduction of symbolic models followed by a discussion about solving NEP(D) in general.

A symbolic model w is a map N → A k with A k def = P(AC k ). Symbolic models can be seen as standard LTL models, i.e. ω-sequences over the finite alphabet A k . Given a valuation v :

N × {x 1 , . . . , x k } → D, we write symb(v, k) to denote the symbolic model obtained from v by setting symb(v, k)(i) = {c ∈ AC k | v, i |= c} for all i ∈ N. A symbolic model w : N → A k is D-satisfiable whenever there is v : N × {x 1 , . . . , x k } → D such that symb(v, k) = w. For instance, the symbolic model {Xx < x} ω is (Q; <)-satisfiable, but it is not (N; <)-satisfiable.
Symbolic models allow us to interpret φ symbolically as an LTL-formula over A k . We write w, i |= LTL φ, where, typically, w, i |= LTL c def ⇔ c ∈ w(i), and the other connectives are interpreted as for LTL. The above example shows that the existence of a symbolic model w for φ does not guarantee the existence of an LTL(D)-model for φ, as w may not be D-satisfiable. However, if the set of all D-satisfiable symbolic models (a set of ω-sequences over A k ) is ω-regular, i.e. it can be expressed by a B üchi automaton, then we can easily solve SAT(LTL(D)) thanks to the property below. D satisfies a few reasonable assumptions omitted herein.

Nonemptiness problem for D-automata.

Let us summarize recent approaches to solve NEP(D) for D-automata. For many concrete domains D, NEP(D) can be reduced to the nonemptiness problem for B üchi automata. Following the lines of arguments from the previous subsection, this may be the case if the class of D-satisfiable symbolic models is effectively ω-regular (see e.g. [BC02; LM07]), or even if it is provably not ωregular, but D-satisfiability of symbolic models can relatively easily be identified, see e.g. [DD07; LOS20]. Some other concrete domains seem to require specific treatments (see e.g. [ST11; KW15]). Of course, another situation occurs if NEP(D) is undecidable. For instance, for D † = (N; =, 0, succ), NEP(D † ) is undecidable by a simple reduction from the halting problem for Minsky machines [Min67].

So let us start with the most favorable case, where the class of D-satisfiable symbolic models is effectively ω-regular. We reduce the problem of deciding NEP(D) to the nonemptiness problem for B üchi automata, also using the decidability of the entailment problem for D. Let A be the D-automaton with variables in {x 1 , . . . , x k } under study, and, as before, let B k D be a B üchi automaton accepting the set of D-satisfiable symbolic models restricted to the variables in {x 1 , . . . , x k }. Then one can define a B üchi automaton A ⊗ B k D by synchronising the transitions using entailments of constraints such that For the less favorable case where the class of D-satisfiable symbolic models is not effectively ω-regular -this is the case, for instance, for (N; <) -specific methods are developed for solving NEP(D). The concrete domains D in [ST11] are of the form (D; <, P 1 , . . . , P l , = d1 , . . . , = dm ), where (D; <) is a linear ordering and the P i 's are unary relations. A saturation construction on D guarantees the existence of a so-called potential function [ST11], leading to a PSPACE upper bound for NEP(D) for many concrete domains satisfying reasonable computational properties including (Q; <), (Z; <) and (N; <). The PSPACE upper bound for SAT(LTL(N; <)) can be obtained as a conse-quence of [ST11,Theorems 16 & 19]. If the class of D-satisfiable symbolic models is not necessarily ω-regular, it is also established that the D-automata for such domains can express languages as those for automata from [BC17] that go strictly beyond B üchi automata. The need to capture the class of D-satisfiable symbolic models that go beyond B üchi automata justifies the need for MSO extensions, introduced in [Boj04] and used in [CKL16] in order to settle the EHD-approach (see forthcoming Section 4).

L(A ⊗ B k D ) = {symb(v, k) | v ∈ L(A)}, the standard construction is omit- ted. Consequently, L(A ⊗ B k D ) = ∅ iff L(A) = ∅.
Besides, in [KW15], concrete domains of the form either

D Q * = (Q * ; < pre , ≤ lex , = d1 , . . . , = dm ) or D [1,α] * = ([1, α] * ; < pre , ≤ lex , = d1 , . . . , = dm ) for some α ≥ 2 are considered. Neither D Q * nor D [1,α] *
v = v 0 v 1 • • • ∈ L(A) (understood as an LTL(D) model) such that v, 0 |= φ (
this is a simple option among many definitions for the model-checking problem). An instance A, φ of MC(LTL(D)) can be solved by checking the nonemptiness of a product automaton made of A and A φ (see Section 3.2.1) that accepts exactly L(A) ∩ L(A φ ). As for plain temporal logics, MC(LTL(D)) can be solved with D-automata, leading to optimal complexity results. For instance, MC(LTL(N; <)) and MC(LTL(R; <)) are PSPACE-complete, see e.g. [BC02; ST11].

Branching-time temporal logics and description logics

In this section, we provide explanations to show how the automata-based approach can be extended to logics CTL * (D) and ALC t (D), whence handling logics whose models are D-decorated Kripke structures. If the class of D-satisfiable symbolic (linear) models is ω-regular, then the generalisation can be done smoothly, by using tree automata instead of B üchi word automata. Let us provide the key steps.

First, using similar arguments as for CTL * , one establishes that the logic under study has the tree model property (see e.g. [Lut04a, Lemma 15], [Gas09, Lemma 3.3] and [CT16, Lemma 11]). This means that the D-decorated Kripke structures can be restricted to (infinite) trees. Moreover, the branching degree, that is the maximal number of children per node, of these trees is only polynomial in the size of the instance. Let us use K to denote the branching degree of the trees.

The second step consists of introducing the notion of symbolic K-tree models, which generalize symbolic (word) models from Section 3.2.1 in a natural way. Recall that A k def = P(AC k ). A symbolic K-tree model t is a map [1, K] * → (A k ) K satisfying certain local consistency conditions. Intuitively, a letter in (A k ) K encodes constraints between a node and its K children. As in the linear case, a symbolic Ktree model t is D-satisfiable whenever there is a D-decorated Kripke tree model v : [1, K] * × {x 1 , . . . , x k } → D that corresponds to t. We omit technical details as they 7 6 7 9 5 . . . are very similar to the linear case. In Figure 3.3, we show a K-tree for k = 1 and K = 2, representing a D-decorated Kripke tree model (on top of the nodes in dotted lines) and a corresponding symbolic K-tree model (below the nodes in dashed lines), where D is (N; <, =). We remark that a constraint graph G t can be induced by any symbolic tree model t (see an early reference to such graphs in [Lut01, Section 4]) and D-satisfiability of t can be reformulated as the existence of an homomorphism between G t and D as done with CSPs. This approach with homomorphisms is extensively developed in [Car15; CKL16; CT16] (see also Section 4).

Xx < x Xx = x x < Xx Xx < x Xx < x Xx < x Xx < x Xx < x Xx = x Xx < x
3.3.1. CTL * (D) in favorable cases. Suppose that the set of D-satisfiable symbolic K-tree models can be characterised by B üchi (or Rabin) tree automata. In this case, we can solve SAT(CTL * (D)) very similarly to the linear case. In order to extend the linear case, we write t, w |= CTL * φ if φ is interpreted on some symbolic K-tree model t (and a world/node w in t) symbolically as for CTL * . The following lemma is the branching counterpart of Lemma 3.2 (with similar assumptions on the input formula φ), see also [Lut04a,Lemma 15] and [CT16, Theorem 11].

LEMMA 3.5 ([GAS09]

). φ is CTL * (D)-satisfiable iff there is a D-satisfiable symbolic K-tree model t for some K ∈ O(|φ|) such that t, ε |= CTL * φ.

Since there is a B üchi (or Rabin) tree automaton B k,K D whose accepted language is the set of D-satisfiable symbolic K-tree models, and there is a tree automaton B CTL * φ whose accepted language is the set of symbolic models t such that t, ε |= CTL * φ [KVW00], one can compute a tree automaton accepting exactly the D-satisfiable symbolic tree models t such that t, ε |= CTL * φ.

Let us name some examples of concrete domains D for which the set of D-satisfiable symbolic K-tree models can be characterised by B üchi (or Rabin) tree automata. This includes all concrete domains in Section 3.2 having this property for the linear case.

Here are a few new examples: (R n ; <, =) and (Q n ; <, =) for some n ≥ 1 and the concrete domain IPC++, see e. 3.3.2. The typical case of ALC t with rational numbers. To conclude Section 3, we present the main steps of the automata-based approach for solving TSAT(ALC t (D Q )) with D Q = (Q; <, >, ≤, ≥, =, =). Note that ALC t (D Q ) is distinct from ALC t (Q; <) as the atomic constraints in formulae occur in R(EP 1 x 1 , . . . , EP d x d ) (see Section 2.4). We present the key results from [Lut04a] and we assume that the roles are abstract features (i.e. interpreted by deterministic binary relations) in order to stick to the assumptions from [Lut04a]. Interestingly, the automata-based approach for description logics with concrete domains has been first introduced in [Lut01] (with journal version [Lut04a]).

In order to use tree automata to solve TSAT(ALC t (D Q )), the formulae involved in the instances are in normal form (negation occurs only in front of propositional variables) and in R(EP 1 x 1 , EP 2 x 2 ) both P 1 , P 2 are of length at most one and at least one P i is empty (see [Lut04a,Lemma 11]). Such restrictions only require to express atomic constraints between a node and its children, which is exactly the way transitions in tree automata are defined.

The key step in [Lut04a] is to introduce Hintikka trees that are abstract D Qdecorated Kripke structures defined as infinite K-trees with nodes labelled by finite sets of formulae , which are built from the input formula φ and the finite set of axioms T . This is a standard approach to design an automata-based approach so that the question to be solved becomes the existence of Hintikka trees for φ, T . Shortly summarizing, the nodes of such Hintikka trees are labelled by sets of formulae that are propositionally consistent, the constraints about a node and its children should be D Qsatisfiable (and of course there are standard requirements related to EX r -formulae), see e.g. [Lut04a, Section 4.3] for more details. The final step consists in showing that the satisfiability of φ with respect to a finite set of axioms T (assumed to be in normal form) is equivalent to the existence of a Hintikka tree (a standard property) [Lut04a, Lemma 15] and the class of Hintikka trees can be captured by a B üchi tree automaton [Lut04a, Lemma 17] leading to optimal complexity upper bounds.

TRANSLATION INTO DECIDABLE MSO THEORIES

In this section, we present an approach initiated in [CKL13] that consists in translating decision problems about temporal logics with concrete domains into decidable MSO-like logics, instead of using D-automata as described in Section 3.

A selection of decidable MSO-like logics

We present an overview over a selection of extensions of MSO logics that will be useful in Section 4.2. A classical result is the decidability of the satisfiability problem for MSO over infinite words, based on B üchi's famous theorem on the expressive equivalence of MSO and finite automata [B üc60]. This result has later been generalized to infinite trees by Rabin [Rab69]. There is a long history of extending MSO to gain expressiveness beyond regular languages. Here, we are interested in the logic MSO+B, introduced for infinite binary trees [Boj04] and infinite words [BC06], which extends MSO with the bounding quantifier B. A formula of the form BX.ϕ(X) expresses that there exists a finite bound on the size of the sets that satisfy ϕ(X). With MSO+B one can define nonregular languages, and the question whether the satisfiability problem for MSO+B is decidable has been part of an elaborate research program [Boj04; BC06; BT12; BGMS14; Boj14; BPT16; BDG + 20]. It turned out that the full logic MSO+B is undecidable [BGMS14; BPT16] over infinite words (and hence infinite trees, too). Undecidability can be proved even for a weaker version of MSO+B, where quantification is allowed over sets of ultimately periodic positions [BDG + 20]. In contrast, a decidability result is established for the weak version of the logic, denoted by WMSO+B, where set quantifiers are restricted to finite sets [BT12]. This result is the base for proving decidability of the satisfiability problem for the logic BMW, which is the set of all Boolean combinations of MSO and WMSO+B [CKL13], interpreted over infinite trees with finite branching degree. The decidability of this logic is the key property for the approach described in the next subsection. The proofs of the decidability for WMSO+B and BMW follow B üchi's approach by proving expressive equivalence of WMSO+B with some automaton model with decidable emptiness problem. We remark that the exact computational complexity of the emptiness problem for this automaton model is open, and so is the complexity of the satisfiability problem for WMSO+B and BMW.

EHD approach

The works based on the automaton-based approach described in Section 3 leave open the decidability status for the branching-time temporal logic over the concrete domain Z = (Z; <, =, (= n ) n∈Z ). In [CKL16], a new approach for establishing decidability results for temporal logics over concrete domains is introduced, and besides settling the question for Z positively (cf. Theorem 2.1), this approach also leads to a bunch of other new results. The gist of the method presented in [CKL16] is the establishment of two key properties of concrete domains D that guarantee the decidability of SAT(CTL * (D)): THEOREM 4.1 ([CAR15; CKL16]). Let D be a concrete domain such that D is negation-closed, and has the property EHD(BMW). Then SAT(CTL * (D)) is decidable.

Let us explain the two properties mentioned in the above theorem. Suppose that σ is the relational signature that D is defined over. We say that D is negation-closed if the complement of each of the relations in σ is definable in positive existential FO over D. For instance, the concrete domain Z is negation-closed:

-¬(x < y) if, and only if, x = y ∨ y < x, -¬(x = y) if, and only if, x < y ∨ x < y, and -¬(x = n) if, and only if, ∃y(y = n ∧ (x < y ∨ y < x)).

The second condition, called the EHD-property, means that one can establish a characterization of all structures over the signature σ that permit a homomorphism into D, and that characterization can be defined in a suitable logic L. Formally, D has the EHD(L)-property if and only if for every finite subsignature τ ⊆ σ one can compute a sentence ψ τ in L such that for every countable structure B over signature τ ∃h : B → D homomorphism ⇐⇒ B |= ψ τ .

In Theorem 4.1 we use L = BMW, and the decidability of this logic (cf. Section 4.1) is essential for yielding the result. We may of course use any other decidable logic; for Z the choice falls naturally to an MSO logic incorporating the bounding quantifier B due to the following characterization [DD07; CKL16]: for every countable structure B = (B; < B ) over signature {<}, there exists a homomorphism into (Z; <) if, and only if, -B does not contain any cycles, and, -for all a, b ∈ B, there exists some n ∈ N such that the length of each path from a to b is bounded by n. By a path from a to b we mean a sequence a 0 , a 1 , . . . , a k of elements in B such that a 0 = a, a k = b and a i < B a i+1 for all 0 ≤ i < k.

Both properties are definable in WMSO+B, and hence Z possesses EHD(WMSO+B)-property. In [CKL16] it is proved that also Z has the EHD(BMW)property. Together with the above mentioned fact that Z is negation-closed, the application of Theorem 4.1 proves Theorem 2.1, i.e., the decidability of SAT(CTL * (Z)). This illustrates the general method: given some concrete domain D, for proving decidability of SAT(CTL * (D)), it is sufficient to prove that D is negation-closed and has the EHD(BMW)-property.

A natural question is whether this approach can be applied to concrete domains other than Z. In [CFKL17], this question is answered positively for concrete domains belonging to classes of certain tree-like structures. More precisely, the EHD-method is enhanced to classes ∆ of concrete domains, and the satisfiability problem for a class of concrete domains is the question of deciding, for a given CTL * (∆)-formula, whether there exists a concrete domain D ∈ ∆ such that there exists a D-decorated model for that formula. Interestingly, in the same paper it is also proved that the concrete domain T = (N * ; < pre , ⊥, =), i.e., the set of finite words over N together with the prefix and the corresponding incomparability relation, does not have the EHD(BMW)-property. The proof is based on Ehrenfeucht-Fraïssé games which establish that BMW is not expressive enough to distinguish between structures that permit a homomorphism into T and those that do not. Recall that the satisfiability problems for LTL(T ) is decidable [KW15; DD16], so that we can conclude that the EHD property of a concrete domain provides a sufficient but not a necessary condition for a decidable satisfiability problem.

The EHD method has also been applied successfully to the description logic ALC (D): in [CT16], a theorem following the structure of Theorem 4.1 is proved for ALC (D), leading to the decidability of TSAT(ALC (Z)).

As pointed out in Section 4.1, the exact computational complexity of the logic BMW is open, so that no upper computational complexity bounds can be inferred for the decidability results presented in this section. Moreover, the logic BMW is rather expressive and may provide little insight into the studied temporal or description logics (c.f. the PSPACE-upper bound for LTL(Z) [DG08] or a recently established EXPTIME-upper bound for TSAT(ALC (Z)) [LOS20].)

ADDING GLOBAL CONSTRAINTS

In this section, we present a selection of results about the addition of global constraints in LTL(D). Bibliographical references are provided for further studies and examples.

What are global constraints?

So far, constraints between values are expressed by atomic constraints R(t 1 , . . . , t d ) or by using temporal operators. Though R(t 1 , . . . , t d ) has obviously a local scope, global properties can be also handled thanks to the propagation of local constraints. For instance, in LTL(N; =), the formula G(x = Xx) enforces that x takes a unique value all over the linear model. Similarly, the property "the value for x is equal to some future value of y" is entailed by the satisfaction of the formula

G(x = Xx ) ∧ x = x ∧ XF(x = y),
that does not assume any further condition about the values for x. However, one can show that this repeating constraint cannot be expressed in LTL(N; =), without the introduction of an auxiliary x . Note that x plays the role of a rigid variable whose interpretation is constant and its introduction is similar to an existential quantification. In this section, we present extensions of LTL(D) in which new binders or atomic formulae allow us to constrain values at unbounded distance, unlike the atomic constraints R(t 1 , . . . , t d ). To do so, we introduce a natural first-order extension of LTL(D) that is expressive enough to capture well-known explicit global constraints. Similar extensions can be designed for branching-time temporal logics (see e.g. [AFF17]), though omitted here by lack of space. Adding first-order quantification to linear models often leads to very expressive and undecidable formalisms, see e.g. [Krö90]. Presently, the first-order extension is mainly convenient for presentation purposes.

Probably, freeze binding is the best known mechanism to express global constraints. A formula of the form ↓ r=y φ states that freezing the current value of y in the rigid variable r, makes true φ (r possibly occurs in φ). Its popularity comes from its high expressive power and the possibility to use it in a restrictive way if computational properties are required. The freeze binding mechanism can be traced back to works about real-time logics to express constraints about time intervals, see e.g. [AH94], modal hybrid logics to mark states, see e.g. [Gor96; ABM01], logics for data trees, see e.g. [Fig10; JL11], or half-order modal logics in which predicate λ-abstraction permits a proper interpretation of constants in modal logics, see e.g. [Fit02; LP05]. More examples can be found in [DLN07, Section 5].

A selection of global constraints expressed in a first-order setting

Let RVAR = {r, s, t, . . .} be a set of rigid variables interpreted by elements in D. Unlike variables in VAR whose values can vary from one state to another (understood as flexible variables), the variables in RVAR take the same value for all the states, like variables in classical predicate logic. Below, we define the first-order extension of LTL(D) (written LTL ∃ (D)) and we revisit a few notions from LTL(D). For instance, now, a term is either an expression of the form X i x for some i ≥ 0 (as in LTL(D)) or a rigid variable r. The set of LTL ∃ (D) formulae is defined as follows.

φ ::= R(t 1 , . . . , t d ) | φ ∧ φ | ∃ r φ | Xφ | φUφ,
where the t i 's are (newly defined) terms, R ∈ σ is of arity d, and r ∈ RVAR.

As for LTL(D), a model of LTL ∃ (D) is a map v : N × VAR → D, but the formulae are interpreted under an environment ρ : RVAR → D. Given a model v : N × VAR → D, an environment ρ and i ∈ N, we write r v,ρ,i to denote ρ(r) and X j x v,ρ,i to denote v(i + j, x). The satisfaction relation |= for LTL ∃ (D) is defined as follows (clauses similar to LTL(D) are omitted).

-

v, i |= ρ R(t 1 , . . . , t d ) def ⇔ ( t 1 v,ρ,i , . . . , t d v,ρ,i ) ∈ R D , -v, i |= ρ ∃ r φ def ⇔ there is d ∈ D such that v, i |= ρ[r →d] φ.
A sentence φ (no free occurrences of rigid variables) is satisfiable if there is some model v such that v, 0 |= ρ φ for some arbitrary environment ρ. The model-checking problem can be adapted similary, a well-studied instance is presented in Section 5.3. Now, let us focus on several LTL ∃ (D) fragments obtained by restricting the firstorder quantification and motivated by the desire to express specific global constraints. To start with, assuming that D contains the equality predicate, we introduce the freeze operator ↓ (see e.g. [AH94; Gor96]), already met earlier, such that the formula ↓ r=y φ states that freezing the value of y in the rigid variable r makes true the formula φ. For instance, G(↓ r=y XG(¬(r = y))) expresses that y never takes twice the same value. We write LTL ↓ (D) to denote the restriction of LTL ∃ (D) such that ∃ occurs only in subformulae of the form ∃ r (r = y) ∧ φ and rigid variables occur only in equalities of the form r = z, that amounts to admit first-order quantification only to encode the freeze binder.

Unrestricted use of the freeze quantifier easily leads to undecidability (see below), which motivates the introduction of repeating constraints stating that the current value of x is equal to the value of y at a future position satisfying the formula φ, which can be captured by ↓ r=x XF(r = y ∧ φ). We write LTL (D) (see e.g. [DFP16]) to denote the restriction of LTL ↓ (D) such that ∃ and rigid variables occur only in subformulae of the form ∃ r (r = x) ∧ XF(r = y ∧ φ) (this constraint can be written x = φ y). Similarly, we write LTL (D) to denote the fragment of LTL (D) in which x = φ y is allowed only with φ = . So, x = y only states the repetition of a value. Other relevant fragments of LTL ∃ (D) have been introduced in [Car15, Chapter 8].

The complexity of freezing or repeating

The power of global constraints on simple concrete domains. As the freeze quantifier turns out to be very expressive, in this paragraph we consider simple concrete domains such as (N; =) to measure its impact on computability. For instance, SAT(LTL(N; =)) is PSPACE-complete. However, one rigid variable in LTL ↓ (N; =) leads to undecidability, see the sharp result below improving earlier works [LP05; DLN07; DL09]. THEOREM 5.1 ([FS09]). SAT(LTL ↓ (N; =)) restricted to a unique rigid variable and to the temporal operator F is undecidable.

Restricting the use of the temporal operators as well as the occurrences of the freeze quantifier has been investigated to regain decidability. The safety fragment of LTL ↓ (N; =) contains the formulae with at most one rigid variable and all the occurrences of U occur under an even number of negations. THEOREM 5.2 ([LAZ11]). The satisfiability problem for the safety fragment of LTL ↓ (N; =) is EXPSPACE-complete.

In our definition for safety LTL ↓ (N; =), multiple (flexible) variables are allowed and no propositional variables are present whereas in [Laz11] the safety fragment is inter-preted on data words [Bou02] and the language admits letters from a finite alphabet. Nevertheless, EXPSPACE-hardness in Theorem 5.2 is straightforward from [Laz11] as equalities can simulate letters. Moreover, the EXPSPACE upper bound in Theorem 5.2 can be obtained by a reduction into the safety fragment from [Laz11] that increases only polynomially the number of subformulae and the finite alphabet, which is the essential complexity measure, see e.g. the proof of [Laz11, Theorem 2.5]. Safety refers to the classification of verification properties, see e.g. [Sis94]. Typically, any ω-sequence not in some given safety property has a finite prefix such that none of its extensions belong to the property.

The freeze quantifier can easily lead to undecidability but adequate fragments may regain decidability, see Theorem 5.2. In order to illustrate the diversity of interesting fragments, below, we consider another syntactic fragment leading to decidability but this time for a model-checking problem on counter machines. LTL ↓ (N; =) models with a unique variable are ω-sequences of natural numbers. Such sequences can be extracted from accepting runs for one-counter automata. A one-counter automaton (OCA) A is a structure (Q, q I , δ, Q F ) where Q is the finite set of locations, q 0 ∈ Q, δ ⊆ Q × {-1, 0, +1, 0?} × Q and Q F ⊆ Q. The elements in {-1, 0, +1, 0?} are intructions (decrement, skip, increment, zero-test) and accepting runs (q 0 , n 0 ) -→ (q 1 , n 1 ) -→ • • • are ω-sequences of configurations in (Q × N) ω respecting δ (standard details are omitted) such that (q 0 , n 0 ) = (q I , 0) and some element of Q F occurs infinitely often. The model-checking problem takes as inputs an OCA A and a sentence φ ∈ LTL ↓ (N; =) (with a single flexible variable) and asks whether there is an accepting run (q 0 , n 0 ) -→ (q 1 , n 1 ) -→ • • • such that n 0 n 1 n 2 • • • |= φ. The flat fragment of LTL ↓ (N; =) is made of formulae such that in any positive (resp. negative) occurrence of φ 1 Uφ 2 , ↓ does not occur in φ 1 (resp. in φ 2 ). Unlike the safety fragment, U is not restricted but the occurrences of ↓ are. Though the model-checking problem over OCA is undecidable in full generality [DLS10], flatness allows us to regain decidability. OCA with parameterised tests are studied in [BQS19] to get this upper bound NEX-PTIME. Accepting runs of OCA are data words [Bou02], and many logics have data words as models, see [Kar16, Figure 4.7] for a complete recapitulation of complexity results. It is worth noting that herein, the logics LTL(D) and extensions such as LTL ↓ (D) have no propositional variables (unlike many formalisms dedicated to data words) but this can be simulated with atomic constraints when the number of variables is not bounded and the concrete domain is not trivial.

Repeating values and linearly-ordered domains. Most known decidability results with repeating constraints of the form x = y do involve concrete domains with equality only, see e.g. [DFP16]. Adding a linear ordering may have an expensive computational cost as stated below. THEOREM 5.4 ([CAR15]). SAT(LTL (N; <, =)) restricted to repetition constraints of the form x = y is undecidable.

The proof of Theorem 5.4 is by reducing the infinite accepting run problem for incrementing counter automata (incrementing errors are possible in such machines) [Car15]. By contrast, we have seen that SAT(LTL(N; <, =)) is PSPACEcomplete, and SAT(LTL (N; =)) is decidable in EXPSPACE [DFP16]. Other undecidability results for constrained LTL with repeating constraints and concrete domains with relations other than equality can be found in [Car15; Bha20] as well as the de-sign of decidable fragments. Moreover, the works [AK10; DHLT14; Kar16] have investigated richer global constraints on data words with multiple attributes (flexible variables) that can navigate along positions with identical values for some attribute.

CONCLUDING REMARKS

In this document, we have presented decidability/complexity results for logics with concrete domains, with a diversity of logical formalisms (description logics, temporal logics) and a diversity of concrete domains. For solving satisfiability and modelchecking, we have mainly described the features of the automata-based approach and the EHD-approach. Section 5 is also dedicated to more global constraints, in particular those that can be expressed with the freeze quantifier. The literature is too rich to expect to cover all the topics in a short survey, in particular the logics for the automatic verification of database-driven systems [DHPV09; DHV14] and the separation logics parameterised by theories [BBL09; KJW18] could not be developed further and compared with the formalisms described in Section 2.

As observed in the document, there is a recent tendency in the literature to understand the essential ingredients that allow to get nice computational properties. This is particularly true with the EHD-approach from [Car15; CKL16] that handles rich temporal logics such as CTL * or with the model-theoretical approach from [BR20] to characterise concrete domains having nice computational properties like the ω-admissible concrete domains from [LM07]. There is a general need to understand better many simple concrete domains when embedded in logical formalisms. For instance, the decidability status of SAT(LTL({0, 1} * ; < pre , < suf )) is still open, as far as we know.

Consequently, it should not come as a surprise that more work is required to unify the contributions from [ST11; KW15; CT16; BR20], in particular to understand better the relationships between the automata and the MSO-like formalisms, apart from the goal to provide a uniform framework leading to optimal complexity results. Finally, for many concrete domains, SAT(CTL * (D)) has been shown decidable but with no satisfactory complexity characterisation. There is room for further improvements also here.

M. Vardi and P. Wolper. Automata-theoretic techniques for modal logics of programs. Journal of Computer andSystem Sciences, 32:183-221, 1986. M. Vardi andP. Wolper. Reasoning about infinite computations. Information andComputation, 115:1-37, 1994. M. Vardi and Th. Wilke. Automata: from logics to algorithms. In Logic and Automata: History and Perspectives, number 2 in Texts in Logic and Games, pages 629-736. Amsterdam University Press, 2007. F. Wolter and M. Zakharyaschev. Spatio-temporal representation and reasoning based on RCC-8. In KR'00, pages 3-14, 2000. D. Zhuk. A proof of CSP dichotomy conjecture. In FOCS '17, pages 331-342. IEEE Computer Society, 2017.

  domains. A relational signature σ = {R 1 , R 2 , . . . } is a countable set of relation symbols, where every symbol R i has an associated positive arity. A concrete domain over a relational signature σ is a tuple D = (D; R D 1 , R D 2 , . . . ), where D is the domain, and for each R ∈ σ, R D ⊆ D k is the interpretation of the relation symbol R in D, where k is the arity of R. We often identify the relation R D with the relation symbol R; in that case we specify a concrete domain as (D; R 1 , R 2 , . . . ) or (D; σ).

Fig. 1 .

 1 Fig. 1. A selection of correspondences between DLs and TLs

  In order to handle formulae from the logic LTL(D), we introduce a class of (constrained) D-automata [Rev02] (see also [ Čer94; ST11; KW15]) generalising B üchi automata accepting languages over finite alphabets, see e.g. [Tho90]. The alphabets of D-automata are of the form D k for some k ≥ 1, so potentially infinite if D has an infinite domain. Transitions in D-automata are labelled by constraints that allow us to constrain values in D k at the current and the next position of the input valuation sequence. Formally, a D-automaton A with k variables is a structure (S, δ, I, F ) such that -S is a nonempty finite set of control states (also known as locations), -I ⊆ S is the set of initial states; F ⊆ S is the set of final states, δ is a finite subset of S × C k × S called the transition relation, where C k is the set of constraints over D and T ≤1 k , where T ≤1

  LEMMA 3.2. φ is LTL(D)-satisfiable iff there is a D-satisfiable symbolic model w such that w, 0 |= LTL φ. So let us suppose there exists a B üchi automaton B k D whose accepted language is the set of D-satisfiable symbolic models, restricted to {x 1 , . . . , x k }. By [VW94], one can compute a B üchi automaton B LTL φ whose accepted language is the set of symbolic models w such that w, 0 |= LTL φ. Then the standard product construction for B k D and B LTL φ yields a B üchi automaton accepting L(B k D ) ∩ L(B LTL φ ), i.e., the set of all D-satisfiable symbolic models of φ. This entails the decidability of SAT(LTL(D)) as soon as B k D can be effectively computed, and a PSPACE upper bound if B k

  Hence in this case, NEP(D) and SAT(LTL(D)) admit decision procedures, and complexity characterisations are possible. Let us first review a few examples of ω-regularity that have been considered under various assumptions, see e.g. the globally consistent concrete domains in [Dec92; BC02], ω-admissible concrete domains in [LM07] (see also Section 2.4) and concrete domains satisfying the completion property in [DD07]. Here is an essential property of such concrete domains. ( † †) Given a D-satisfiable conjunction of atomic constraints C, for any set of variables Y occurring in C such that C = C ∧ C with the variables in Y occur exactly in C , for any valuation Y → D satisfying C , there is a conservative extension (over all the variables in C) that satisfies C. This includes (R; <, =), (Q; <, =) and also many temporal and spatial domains from [Lut01; BC02; Lut04a]. For instance, let D A = (I Q ; (R i ) i∈[1,13] ) be the concrete domain such that I Q is the set of closed intervals [r, r ] ⊆ Q and (R i ) i∈[1,13] is the family of 13 Allen's relations [All83]. Similarly, the concrete domain RCC8 with space regions in R 2 contains topological relations between spatial regions, see e.g. [WZ00] (generalisation to more domains D possible). In general, for concrete domains D for the above classes, w : N → A k is D-satisfiable, essentially if for all i ∈ N, w(i) is Dsatisfiable, and w is locally consistent, that is for all R(Xt 1 , . . . , Xt d ) ∈ AC k , we have R(Xt 1 , . . . , Xt d ) ∈ w(i) iff R(t 1 , . . . , t d ) ∈ w(i + 1). THEOREM 3.3 ([BC02; DD07; ST11]). SAT(LTL(Q, <, =)), SAT(LTL(R, <, =)), SAT(LTL(RCC8)) and SAT(LTL(D A )) are PSPACE-complete. Strictly speaking, the PSPACE upper bound in [BC02] does not involve automata but it is possible to reformulate the results with B üchi automata, which is partially done in [DD07]. A substantial contribution in [BC02] is the design of sufficient conditions on D to get a general decidability result for SAT(LTL(D)). For instance, the PSPACE upper bound for SAT(LTL(RCC8)) in [BC02] improves the EXPSPACE bound from [WZ00].

  falls into the classes of concrete domains designed in [BC02; LM07; DD07] (see above). The problem NEP(D Q * ) is shown in PSPACE [KW15, Theorem 6] by a sophisticated analysis based on an underlying well-quasi-ordering. The crux of the proof consists in showing that in case of nonemptiness, there is a specific run with a so-called noncontracting loop [KW15, Corollary 19]. It would be worth investigating the similarities with the proof method in [ST11], although the classes of concrete domains are incomparable. As a consequence of the runs analysis, the complexity of SAT(LTL(D Q * )) can be characterised. THEOREM 3.4 ([KW15]). SAT(LTL(D Q * )) and SAT(LTL([1, α] * )) (α ≥ 2) are PSPACE-complete. The results about SAT(LTL([1, α] * )) can be reduced from those for SAT(LTL(D Q * )) and for NEP(D Q * ), see [KW15, Theorem 4] although solving the problem with a finite alphabet is more constrained.

  3.2.3. Model-checking. We write MC(LTL(D)) to denote the model-checking problem that takes as input a D-automaton A and a formula φ in LTL(D) both over the set of variables {x 1 , . . . , x k }, and asks whether there exists

Fig. 2 .

 2 Fig. 2. Part of a tree with branching degree 2. The labels in the gray dotted boxes on top of each node represent a D-decorated Kripke tree model for k = 1 and D = (N; <, =). The labels in the dashed boxes below each node represent a corresponding symbolic 2-tree model.

  g. [Dem06], whose domain is N and the relations include x ≡ k y [d, d ], x ≡ k [d, d ] (periodicity constraints), x = y and x < d. THEOREM 3.6 ([GAS09; GAS07]). SAT(CTL * (D)) is 2EXPTIME-complete for every concrete domain D in listed above. The logic CTL * (N; <) does not fall in the scope of Theorem 3.6 and the decidability of SAT(CTL * (N; <)) has been first established in [CKL13] using the EHD-approach (see Section 4). Notably, significant syntactic fragments of CTL * (N; <) are shown to admit a decidable satisfiability problem in [BG06] by using integral relational automata [ Čer94]. However, the complexity of SAT(CTL * (N; <)) remains open despite the substantial advances made in [BG06; CKL13] but the recent results from [LOS20] might help to close the gap.

  THEOREM 3.7 ([LUT04A]). TSAT(ALC t (D Q )) is EXPTIME-complete. Theorem 3.7 can be refined and extended by considering other concrete domains (for instance ω-admissible ones [LM07]) and by adding new features in the logical languages, see e.g. [Lut02b; Lut04b]. By contrast, adapting Theorem 3.7 to D N = (N; <, > , ≤, ≥, =, =), possibly enriched with constant tests, is not a trivial task. For instance, TSAT(ALC (D N )) is shown decidable in [CT16], and in EXPTIME in the follow-up paper [LOS20] (with constants encoded in unary) using an automata-based approach. Moreover, it entails decidability results for description logics in the style of those from [LM07], typically a 2EXPTIME upper bound for TSAT(ALC t (D N )) [LOS20, Theorem 29]. Interesting open problems in [LOS20] include for instance the question of EXPTIME-easiness of the logic ALC (D N ) with a concrete domain augmented with constant tests (constants encoded in binary).

  THEOREM 4.2 ( [CFKL17]). SAT(CTL * (∆)) is decidable for the following classes ∆ of concrete domains (1) the class of all semi-linear orders, (2) the class of all ordinal trees, (3) the class of all order trees of height h, for each h ∈ N.

  THEOREM 5.3 ([BQS19]). Model-checking problem over OCA for flat LTL ↓ (N; =) is NEXPTIME-complete.

  Presburger arithmetic [Pre29; Haa18]. Decidability was originally established by Presburger via a quantifier elimination procedure, but several simplifications and other decision procedures were proposed afterwards [FR98; Opp78], see [Haa18] for an exhaustive overview. For concrete domains over finite strings, the undecidability of many FO theories can easily be established, including (A * ; •) [Qui46], (A * ; < seq ) [Kus06; KS15; HSZ17], and (A * ; < sbwd ) [Kus06]. One exception is the FO theory over (A * ; < pre ), for which the decidability is established by the famous theorem by Elgot and Rabin [ER66]. The focus of most research is on restricted fragments of FO, typically the existential FO theory [Mak77; Pla04; Kus06; KS15] or a restricted variable fragment of FO [KS15; HSZ17].

ACM SIGLOG News

Vol. 0, No. 0, 0000