Adding two equivalence relations to the interval temporal logic AB

Abstract

The interval temporal logic AB features two modalities that make it possible to access intervals which are adjacent to the right of the current interval (modality hAi) and proper subintervals that have the same left endpoint of it (modality hBi). AB is one of the most significant interval logics, as it allows one to express meaningful (metric) properties, while maintaining decidability (undecidability rules over interval logics, AB is EXPSPACE-complete [14]). In an attempt to capture ωS-regular languages with interval logics [15], it was proved that AB extended with an equivalence relation, denoted AB ∼, is decidable (non-primitive recursive) on the class of finite linear orders and undecidable on N. The question whether the addition of two or more equivalence relations makes finite satisfiability for AB undecidable was left open. In this paper, we answer this question proving that AB∼1∼2 is undecidable.

-

Interval temporal logics (ITL) are temporal logics where time intervals/periods, instead of time points/instants as in the standard framework, are used as basic building blocks. ITL are characterized by high expressiveness and high computational complexity. The main formalization of these logics is known as HS which features one modality for each interval order relation [ 7 ] (the so-called Allen’s relations [ 1 ]). In this paper, we analyze the complexity of the finite satisfiability problem for the interval temporal logic AB of Allen’s relations meets and begun by extended with two equivalence relations. AB is one of the most significant fragments of HS since it is decidable [ 14 ] (undecidability rules over interval logics [ 5 ]) and it can express various important (metric) temporal properties. As an example, it allows one to encode the standard until operator of point-based linear temporal logic as well as to constrain the length of an interval to be less than/equal to/greater than a given value [ 14 ].

The trade-off between the increase in expressiveness and the complexity blowup induced by the addition of one or more equivalence relations to a logic has been already highlighted in the literature (see, for instance, the logics for semistructured data [ 3 ], temporal logics [ 6 ], and timed automata [ 16 ]). Finite satisfiability of the two-variable fragment of first-order logic FO2 extended with one, two, or more equivalence relations has been systematically explored in [ 8–10 ], while the extension of FO2, interpreted over finite or infinite data words, with an equivalence relation has been investigated by Bojan´czyk et al. in [ 3 ]. Similar results have been obtained by Demri and Lazic [ 6 ], that studied the extension of linear temporal logic over data words with freeze quantifiers, which allow one to store elements at the current word position into a register and then to use them in equality comparisons deeper in the formula, and by Ouaknine and Worrell [ 16 ], who showed that both satisfiability and model checking for metric temporal logic over finite timed words are decidable with a non-primitive recursive complexity.

The addition of an equivalence relation to an interval temporal logic was first investigated by Montanari and Sala in [ 15 ]. They focused their attention on the interval logic AB of Allen’s relations meets and begins extended with an equivalence relation, denoted AB∼, interpreted over finite linear orders and N, and they showed that the resulting increase in expressive power makes it possible to establish an original connection between interval temporal logics and extended regular languages of finite and infinite words [ 2 ]. As for the computational complexity, they proved that AB∼ is decidable (non-primitive recursive) on the class of finite linear orders and undecidable on N. Recently, the interval logic of temporal neighborhood PNL, which features two modalities for Allen’s relations meets and met by, and its metric variant MPNL, both extended with one equivalence relation, have been proved to be decidable over finite linear orders [ 13 ] (NEXPTIME-complete the former, EXPSPACE-hard the latter). In this paper, we answer a question left open in [ 15 ], showing that the addition of two (or more) equivalence relations makes AB undecidable also over finite linear orders.

The paper is organized as follows. Section 2 illustrates in some detail previous work on the interval temporal logic AB extended with one equivalence relation and some related work. Section 3 introduces syntax and semantics of the logic AB∼1∼2 and gives some background knowledge about counter machines. The next two sections provide a reduction from the undecidable 0-0 reachability problem for Minsky counter machines to the finite satisfiability problem for AB∼1∼2. More precisely, Section 4 outlines the general structure forced on each model (if any) by the formulas given in Section 5. Finally, in Section 6 we prove that the proposed encoding is correct. Conclusions provide an assessment of the work and outline future research directions. 2

Related work

The present paper can be viewed as the natural completion of the work reported in [ 15 ], where Montanari and Sala proved that the satisfiability problem for AB∼ is decidable over finite linear orders, with non-primitive recursive complexity, and undecidable over N. Undecidability has been proved by a reduction from the (undecidable) 0-n reachability problem for lossy counter machines [ 11 ]. As for finite satisfiability, they initially reduced the problem of finding a model for a given AB∼ formula ϕ to the existence of a particular compass structure exploiting the correspondence that can be established between intervals and points in the positive octant of the Cartesian plane, that is, the map that links any interval [x, y] to the corresponding point (x, y). Then, by exploiting a suitable model contraction technique, they showed that if ϕ is finitely satisfiable, then a structure satisfying it can be obtained via a bottom-up generation of candidate (finite) compass structures. Since the number of pairwise incomparable rows of any candidate structure can be proved to be finite, termination easily follows. The complexity bound has been obtained by encoding in AB∼ the 0-0 reachability for lossy counter machines (LCM) which is known to be a non-primitive recursive (decidable) problem [ 17 ].

The general structure of the AB∼ encoding of the 0-0 reachability problem for LCM is similar to the one provided in this paper for (non-lossy) counter machines (CM). However, when only one equivalence relation is available, it is possible to enforce the presence of certain points in a configuration (depending on the points of the previous configuration), but not to restrict the number of points in it. This last constraint is necessary for the encoding of CM and it can be enforced only by making use of two equivalence relations.

From a technical point of view, our work presents some similarities to the one by Bojan´czyk et al. in [ 4 ], where it is shown, among other results, that the logic FO2(+1, ∼1, ∼2) over finite data words is undecidable. To prove it, they provide a reduction from the Post correspondence problem to finite satisfiability for FO2(+1, ∼1, ∼2), that exploits the interconnections between equivalence relations in a way that is similar to what we do here. However, their encoding strongly depends on constraints of the form ∀∃ which are not expressible in AB. To overcome these limitations, we will exploit some metric properties definable in AB. 3

Preliminaries

In this section, we first introduce syntax and semantics of AB∼1∼2 and then we provide background knowledge about Minsky counter machines. 3.1

The interval temporal logic AB∼1∼2 The interval temporal logic AB∼1∼2 features two modalities hAi and hBi corresponding to Allen’s relations meets and begun by, respectively, and two special binary relation symbols ∼1 and ∼2. Formally, given a set Prop of propositional variables, formulas of AB ∼1∼2 are built up from Prop and ∼1, ∼2 using the Boolean connectives ¬, ∨ and the modalities hAi and hBi. Moreover, we make use of shorthands ϕ1 ∧ ϕ2 for ¬(¬ϕ1 ∨ ¬ϕ2), [A]ϕ for ¬hAi¬ϕ, [B]ϕ for ¬hBi¬ϕ, > for p ∨ ¬p, and ⊥ for p ∧ ¬p, with p ∈ Prop.

We interpret formulas of AB∼1∼2 in interval temporal structures over (prefixes of) N endowed with the ordering relations meets (denoted by A) and begun by (denoted by B), and two equivalence relations ∼1 and ∼2. More precisely, we identify any given ordinal N < ω with the prefix of length N of N and we accordingly define I(N ) as the set of all closed intervals [i, j], with i, j ∈ N and i ≤ j. A special role will be played by point-intervals (intervals of the form [i, i], with i ∈ N ) and unit-intervals (intervals of the form [i, i + 1]), which can be respectively defined as [B] ⊥ (abbreviated π) and [B][B] ⊥ (abbreviated unit). For any pair of intervals [i, j], [i0, j0] ∈ I(N ), relations A and B are defined as follows: – meets relation: [i, j] A [i0, j0] iff j = i0; – begun by relation: [i, j] B [i0, j0] iff i = i0 and j0 < j.

The (non-strict) semantics of AB∼1∼2 is given in terms of interval models S = hI(N ), A, B, ∼1, ∼2, V i, where ∼1 and ∼2 are two equivalence relations over N and V : I(N ) → ℘(Prop) is a valuation function that assigns to every interval [i, j] ∈ I(N ) the set of propositional variables V ([i, j]) that are true on it. The truth of an AB∼1∼2 formula over a given interval [i, j] in a model S is defined by structural induction as follows: – S, [i, j] – S, [i, j] – S, [i, j] – S, [i, j]

S, [i0, j0] – S, [i, j] p iff p ∈ V ([i, j]), for all p ∈ Prop; ¬ψ iff S, [i, j] 2 ψ; ϕ ∨ ψ iff S, [i, j] ϕ or S, [i, j] ψ; hXiψ iff there exists an interval [i0, j0] such that [i, j] X [i0, j0], and ψ, for X ∈ {A, B}; ∼k iff i ∼k j, for k ∈ {1, 2}.

Given an interval structure S and a formula ϕ, we say that S satisfies ϕ if there is an interval I in S such that S, I ϕ. We say that ϕ is (finitely) satisfiable if there exists a (finite) interval structure that satisfies it. We define the (finite) satisfiability problem for AB∼1∼2 as the problem of establishing whether a given AB∼1∼2 formula ϕ is (finitely) satisfiable. 3.2

Counter machines A k counter machine (kCM) is a triple of the form M = (Q, k, δ), where Q is a finite set of control states, k is the number of counters, whose values range over N, and δ is a function that maps each state q ∈ Q to a transition rule having one of the following forms: 1. value(h) ← value(h) + 1; goto q0, for some 1 ≤ h ≤ k and q0 ∈ Q (abbreviated (q, h + +, q0)), meaning that, whenever M is at state q, it increases the counter h and it moves to state q0; 2. if value(h) = 0 then goto q0 else value(h) ← value(h) − 1; goto q00, for some 1 ≤ h ≤ k and q0, q00 ∈ Q (abbreviated (q, h?0, q0, q00)), meaning that, whenever M is at state q and the value of the counter h is 0 (resp., greater than 0), it moves to state q0 (resp., it decrements the counter h and it moves to state q00).

A computation of M is any sequence of configurations that conforms to the transition relation. The reachability problem for a counter machine M = (Q, k, δ) is the problem of deciding, given two configurations (q0, z0) and (qf , zf ), whether there is a computation that takes M from (q0, z0) to (qf , zf ). The reachability problem for counter machines is undecidable even for machines with only two counters [ 12 ]. For convenience, we will use a restricted, but equally undecidable, form of this problem, called 0-0 reachability problem, where z0 and zf are both 0. Moreover, without loss of generality, we restrict our attention to computations where q0 and qf occur only at the beginning and at the end, respectively. 4

The structure of intended models

The main contribution of the paper is the proof of the following theorem. Theorem 1. The satisfiability problem for AB∼1∼2 over the class of finite linear orders is undecidable.

To prove it, we provide a reduction from the 0-0 reachability problem for Minsky two-counter machines to the satisfiability problem for AB∼1∼2. More precisely, given a two-counter machine M = (Q, 2, δ) and two states q0, qf ∈ Q, we build a formula ψM,q0,qf such that there exists a computation in M from the configuration (q0, 0, 0) to the configuration (qf , 0, 0) if and only if ψM,q0,qf is satisfiable. First, in the present section, we delineate the structure that we want to give to each model (if any) of ψM,q0,qf (the intended model). Then, in Section 5, we show how to encode in AB∼1∼2 such a structure. We conclude the paper with the proof of the correctness of the encoding.

The structure of the models of the encoding formula can be described as follows. To start with, we partition the set of point-intervals (points for short) in two subsets: points labeled by a state in Q (state-points ) and points labeled by c1 or c2 (counter-points ). A configuration (q, v1, v2) is represented as a set of contiguous points, where the first point is a state-point with label q and the remaining ones are counter-points such that exactly v1 points have label c1 and v2 points have label c2, in any order. Counter-points with label del are points which have been “deleted” and thus do not count for the value of a counter in a configuration.

The computation of the two-counter machine M (from q0 to qf ) consists of a sequence of contiguous configurations. Counter-points with label plus and minus indicate, respectively, points added in a configuration as a result of a counter increment or eliminated in the next configuration as a result of a counter decrement. Each configuration, but the first one, is obtained from the previous one by applying a transition of M , which amounts to say that the sequence of configurations is a valid computation of M .

In Figure 1, we give an example of the proposed model representation for the computation (q, 1, 1) → (q0, 1, 0) → (q00, 2, 0). The second configuration (q0, 1, 0) is obtained from the initial configuration (q, 1, 1) by decrementing the second counter; the third configuration is obtained from the second one by incrementing the first counter. Notice that points with label minus are deleted, that is, labeled by del, in the configuration that immediately follows the one in which the decrement of the counter takes place.

q c1 minus c2 del c2 q0 c1 q00 c1 del c2 plus c1 ψM,q0,qf ≡ ψ0→0 ∧ [G](ψpoints ∧ ψδ ∧ ψ∼), where [G]ϕ is an shorthand for [B]ϕ ∧ ϕ ∧ [B][A]ϕ ∧ [A][A]ϕ (universal modality) and – ψ0→0 forces the initial and final configurations of the computation to be respectively (q0, 0, 0) and (qf , 0, 0); – ψpoints specifies conditions on points: (i) points are partitioned in statepoints and counter-points, (ii) labels plus and minus can label counterpoints only, and (iii) in a configuration, there is at most one point with label minus and at most one point with label plus; – ψδ ensures the consistency of state-points and plus/minus points with the transitions in M , that is, if a configuration τ 0, with state-point q0, immediately follows a configuration τ , with state-point q, then one of the following three cases must hold: (i) there is a transition δi = (q, h + +, q0) ∈ δ, there is no point with label minus in τ , and there is one point with labels ch and plus in τ 0; (ii) there is a transition δi = (q, h?0, q0, q00), there is no point with label ch and without label del in τ , and there is no point with label plus in τ 0; (iii) there is a transition δi = (q, h?0, q00, q0), there is one point with label ch and without label del in τ , and there is no point with label plus in τ 0; – ψ∼ guarantees that each configuration is obtained from the previous one by an increment/decrement/no-action transition (notice that the fact that the transition actually belongs to M is checked by ψδ and not by ψ∼).

Formulas ψ0→0, ψpoints, and ψδ can be easily expressed in AB, that is, equivalence relations play no role in the encoding of the corresponding conditions. The main component of the encoding is the formula ψ∼, which acts like a controller of the form of configurations by preventing the addition of any unwanted counter-point. More precisely, it forces each configuration to be an isomorphic copy of the previous configuration, that is, to feature the same counter-points in the same order, plus at most one extra point with label plus.

We now show how to express each of above conditions in AB∼1∼2. To facilitate the reading of the formulas, we make use of the following abbreviations: we denote the formula Wn i=1 ci by the i=1 qi by the symbol q and the formula W2 symbol c. Moreover, we define the following formula, parametric in ϕ: succ(ϕ) ≡ hAi(unit ∧ hAi(π ∧ ϕ)) which states the truth of ϕ at the point immediately after the current interval, that is, at the successor of the right endpoint of the current interval. Finally, we introduce a derived modality hPi, which is defined in terms of modalities hAi and hBi, that allows one to force a given formula ϕ to be true at some point of the current interval, endpoints included. The modality hPi is formally defined as follows:

P ϕ ≡ hBihAi(π ∧ ϕ) ∨ hAi(π ∧ ϕ).

h i The dual of the above modality is defined as usual, that is, [P]ϕ ≡ ¬hPi¬ϕ, and it states that ϕ holds at each point of the current interval (endpoints included).

The initial and final configurations are encoded by the formula: ψ0→0 ≡ q0 ∧ succ(q) ∧ hAihAiqf ∧ [A][A](qf → succ([A][A](¬q ∧ (c → del)))). It states that the initial configuration is (q0, 0, 0) (the first state-point q0 is followed by a state-point) and that the final configuration is (qf , 0, 0) (the last state-point is qf and every counter-point after it, if any, is deleted).

The formula ψpoints is defined as the conjunction of the following conditions (hereafter, we explicitly provide the encoding of the most complex conditions only): (A1) every point of the domain has one and only one label from the set

Q ∪ {c1, c2}; (A2) labels in Q ∪ {c1, c2} ∪ {plus, minus, last, del} are given to points only; (A3) at most one counter-point per configuration can be labeled with plus and at most one with minus; (A4) the label last is associated with the points of the final configuration only:

(last → π) ∧ (last ↔ [A](¬π → [A]¬q)); (A5) only counter-points can be labeled with del and a point can not have both label del and label plus (or minus).

The formula ψδ is defined as the conjunction of the following conditions: (B1) all configurations but the initial one (and only them) have one (and only one) label in δ = {δ1, ..., δm}. We label the first configuration with a dummy transition δ0. If a configuration is labeled with δi, for some i > 0, it means that it is obtained from the previous configuration by the application of the transition δi; (B2) transition labels are consistent with state-points of each configuration: ^ δi=(q,h++,q0)∈δ ∧ ∧

^ δi=(q,h?0,q0,q00)∈δ

^ δi=(q,h?0,q0,q00)∈δ (δ ∧ succ(hAiδi)) →

(hBiq ∧ succ(q0 ∧ hAi(δi ∧ hPi(ch ∧ plus)))) (δ ∧ [P](ch → del) ∧ succ(hAiδi)) → (hBiq ∧ succ(q0)) (δ ∧ hPi(ch ∧ ¬del) ∧ succ(hAiδi)) →

(hBiq ∧ succ(q00) ∧ hPi(ch ∧ minus)), where δ is a shorthand for the formula Wim=0 δi; (B3) there are no points labeled with plus in configurations labeled with non-increment transitions or point labeled with minus in configurations that precede configurations labeled with non-decrement transitions; (B4) every (non-final) configuration devoid of counter-points is followed by a configuration with at most one counter-point (labeled with plus).

In order to define the formula ψ∼, it turns out to be useful to introduce the following formula:

ψ∃!q ≡ ([B](hAiq → [B]hAi¬q) ∧ hBihAiq ∧ hAi¬q) ∨ (hAiq ∧ [B][A]¬q), which guarantees the existence of a unique state-point inside the current interval (endpoints included).

We call an interval labeled with both ∼1 and ∼2 and containing exactly one state-point a linking interval, that is, a linking interval is an interval that satisfies the formula ∼1 ∧ ∼2 ∧ψ∃!q, and we say that its endpoints are linked together (the use of linking intervals in the encoding will be explained in Section 6).

The formula ψ∼ is defined as the conjunction of the following conditions: (C1) a unit interval can not be labeled with both ∼1 and ∼2:

unit → ¬(∼1 ∧ ∼2); (C2) there is no interval, whose endpoints belong to the same configuration, which is neither a point interval nor a unit interval and is labeled with ∼1 or ∼2: (¬π ∧ ¬unit ∧ [P]¬q) → ¬(∼1 ∨ ∼2); (C3) two consecutive counter-points are in relation ∼1 or ∼2: (unit ∧ hBic ∧ hAic) → (∼1 ∨ ∼2) (c ∧ ¬last) → hAi(∼1 ∧ ∼2 ∧ψ∃!q); (C4) each counter-point, which does not belong to the last configuration, starts a linking interval: (C5) the labels of the endpoints of a linking interval must satisfy the following constraints: (∼1 ∧ ∼2 ∧ψ∃!q) → ((hBic1 ∧ hAic1) ∨ (hBic2 ∧ hAic2)) ∧ (hBidel → hAidel) ∧ (hBiminus → hAidel) ∧ (hBi(¬minus ∧ ¬del) → hAi¬del) ∧ (hAi¬plus) ; (C6) the first point of all configurations, but the final one, is linked to the first point of the next configuration: (unit ∧hBi(q ∧ ¬last) ∧ hAic)

→ hAi(∼1 ∧ ∼2 ∧ψ∃!q ∧ [B](hAiq ∨ [P]¬q)).

We would like to observe that the formula [B](hAiq ∨ [P]¬q)) enforces the second to last point of the linking interval to be the only state-point. Let [x, y] be this interval. If y0, with x < y0 < y − 1, were a state-point (it can not be the final point y since [x, y] is a linking-interval, and, by C5, linking intervals have counter-points as their endpoints), then [x, y − 1] would satisfy neither hAiq (there can only be one state-point between x and y) nor [P]¬q (since y0 is between x and y − 1 and it is a state-point); (C7) the last point of every configuration, but the final one, is linked to a point that is followed by a state-point or by a counter-point with label plus followed by a state-point: (δi ∧ hBi¬last) →hAi ∼1 ∧ ∼2 ∧ ψ∃!q ∧

(succ(q) ∨ succ(plus ∧ succ(q))) .

We would like to emphasize the crucial role of condition (C5). First of all, it constrains linking intervals to connect counter-points with the same label (either c1 or c2). Moreover, it transfers logical deletion (counter-points labeled by del) from one configuration to the next one, it forces the actual execution of a new deletion by connecting a counter-point labeled by minus to a counter-point labeled by del, and it prevents unwanted deletions or insertions to take place. 6

Proof of correctness of the encoding

The proof of correctness for the formulas ψpoints, ψδ, and ψ0→0 is straightforward. The only thing that we really need to show is that the behavior of the formula ψ∼ is actually the one we described in Section 5, that is, we need to prove that ψ∼ forces each configuration to be the result of the application of a transition of a (generic) counter machine to the previous configuration. To this end, we show that each configuration τi+1 contains an exact copy of the counter-points of the previous configuration τi in its initial part plus possibly an additional point labeled with plus at the end (if it is obtained from the previous configuration by an increment transition).

Let S = (I(N ), A, B, ∼1, ∼2, V ) be a model of ψM,q0,qf and q0, q1, . . . , qm be the enumeration of its state-points according to the order of the domain (therefore, by ψ0→0, q0 = q0 and qm = qf ). The configuration τi is defined as the set of points from qi (included) to qi+1 (excluded). τm consists of qm and the points that follows it, till the end of the domain I(N ). We denote by ∼k any of the relations ∼1 or ∼2. If τ is an ordered set of points, we write τ j to denote the j-th point of τ .

Let f be the set of all and only those pairs of points, belonging to two consecutive configurations τi and τi+1, which are connected by a linking interval, that is, (x, y) ∈ f if and only if there exist τi, τi+1 such that x ∈ τi, y ∈ τi+1, x ∼1 y, and x ∼2 y.

First of all, we observe that for each counter-point x in τi there exists a counter-point y in τi+1 such that (x, y) ∈ f (by (C4)). Moreover, by condition (C5), every pair in f consists of counter-points with the same label ck. We now prove that f is (the map of) an injective function that preserves adjacency between points, that is, if x, x0 are consecutive counter-points, then f (x), f (x0) are consecutive counter-points as well: – f is a function: suppose that there exist y, y0, with y < y0, in τi+1 which have the same counter-image x, with x ∈ τi, in f , then y ∼1 x ∼1 y0 and y ∼2 x ∼2 y0, and thus y ∼1 y0 and y ∼2 y0, which violates condition (C1) or condition (C2), depending on the distance between y and y0 (if |y0 − y| = 1, then it violates (C1); otherwise, it violates (C2)); – f is injective: the proof is similar to the one given for the previous point.

Suppose that there exist x, x0, with x < x0, in τi which have the same image y, with y ∈ τi+1, in f , then x ∼1 y ∼1 x0 and x ∼2 y ∼2 x0, and thus x ∼1 x0 and x ∼2 x0, that violates condition (C1) or condition (C2); – f preserves adjacency: let x, x0 be two consecutive points in τi, that is, x0 is the successor of x, and let y and y0 be their respective images (since f is a injective function, it immediately follows that they are unique). By condition (C3), it holds that ∼k∈ V ([x, x0]), and thus y ∼k x ∼k x0 ∼k y0 and ∼k∈ V ([y, y0]), which, by condition (C2), implies that y, y0 are consecutive.

By the properties of f and condition (C6), it follows that f (τij ) = τij+1 for j = 2, . . . , |τi| (order preservation). A graphical account of the relationships between pairs of counter-points belonging to two consecutive configurations is given in q p1 c1 p2 ∼1

∼2 c2 p3 c1 p4 ∼1∼2 q0 p5 ∼1∼2 c1 p6 ∼1

∼2 c2 p7 c1 p8 ∼1∼2 In [ 15 ], Montanari and Sala studied complexity and expressiveness of the interval temporal logic AB∼, that extends AB with an equivalence relation. Complexity and (un)decidability results are given by means of suitable reductions from reachability problems for lossy counter machines. The resulting picture is as follows: one gets decidability over finite linear orders with nonprimitive recursive complexity and undecidability over N. In addition, they showed that decidability can be recovered by suitably restricting the class of models over which AB∼ formulas are interpreted. In this paper, we proved that decidability of finite satisfiability is lost when two or more equivalence relations are added to AB.

As for future work, in analogy to what Montanari and Sala did for AB ∼ over the natural numbers, we are thinking of possible ways of restricting the class of models over which AB ∼1∼2 formulas are interpreted in order to recover finite satisfiability. We are also studying the effects of the addition of two or more equivalence relations to other interval logics, such as (metric) propositional neighborhood logic, which preserves decidability when extended with one equivalence relation only [ 13 ].

References

1. J. Allen . Maintaining knowledge about temporal intervals . Communications of the ACM , 26 ( 11 ): 832 - 843 , 1983 .

2. M. Bojan ´czyk. Weak MSO with the unbounding quantifier . Theory of Computing Systems , 48 ( 3 ): 554 - 576 , 2011 .

3. M. Bojan´czyk, C. David , A. Muscholl , T. Schwentick , and L. Segoufin . Twovariable logic on data words . ACM Transactions on Computational Logic , 12 ( 4 ): 27 , 2011 .

4. M. Bojanczyk , C. David , A. Muscholl , T. Schwentick , and L. Segoufin . Twovariable logic on data words . ACM Transactions on Computational Logic , 12 ( 4 ): 27 , 2011 .

5. D. Della Monica , V. Goranko , A. Montanari , and G. Sciavicco . Interval temporal logics: a journey . Bulletin of the EATCS , 105 : 73 - 99 , 2011 .

6. S. Demri and R. Lazic . LTL with the freeze quantifier and register automata . ACM Transactions on Computational Logic , 10 ( 3 ), 2009 .

7. J. Halpern and Y. Shoham . A propositional modal logic of time intervals . Journal of the ACM , 38 ( 4 ): 935 - 962 , 1991 .

8. E. Kieronski , J. Michaliszyn , I. Pratt-Hartmann , and L. Tendera . Two-variable first-order logic with equivalence closure . In Proc. of the 27th LICS , pages 431 - 440 . IEEE, 2012 .

9. E. Kieronski and M. Otto . Small substructures and decidability issues for firstorder logic with two variables . In Proc. of the 20th LICS , pages 448 - 457 . IEEE, 2005 .

10. E. Kieronski and L. Tendera . On finite satisfiability of two-variable first-order logic with equivalence relations . In Proc. of the 24th LICS , pages 123 - 132 . IEEE, 2009 .

11. R. Mayr . Undecidable problems in unreliable computations . Theoretical Computer Science , 297 ( 1-3 ): 337 - 354 , 2003 .

12. M. L. Minsky . Computation: finite and infinite machines , 1967 . Cited on, page 54 , 1967 .

13. A. Montanari , M. Pazzaglia , and P. Sala . Metric propositional neighborhood logic with an equivalence relation . In Proc. of the 21st TIME. IEEE , 2014 .

14. A. Montanari , G. Puppis, P. Sala , and G. Sciavicco . Decidability of the interval temporal logic ABB¯ on natural numbers . In Proc. of the 27th STACS , pages 597 - 608 , 2010 .

15. A. Montanari and P. Sala . Adding an equivalence relation to the interval logic ABB¯: Complexity and expressiveness . In Proc. of the 28th LICS , pages 193 - 202 . IEEE, 2013 .

16. J. Ouaknine and J. Worrell . On the decidability and complexity of metric temporal logic over finite words . Logical Methods in Computer Science , 3 ( 1 ), 2007 .

17. P. Schnoebelen . Verifying lossy channel systems has nonprimitive recursive complexity . Information Processing Letters , 83 ( 5 ): 251 - 261 , 2002 .