Metric Right Propositional Neighborhood Logic with an Equivalence Relation Pietro Sala1 Department of Computer Science, University of Verona, Strada le Grazie 15, Verona, Verona pietro.sala@univr.it http://profs.scienze.univr.it/ sala/ Abstract. In [13] Montanari et al. proved that the satisfiability prob- lem for the fragments A and AA of Halpern and Shoham’s modal logic of intervals extended with an equivalence relation ∼ over points, namely the logics A ∼ and AA ∼ respectively, is decidable and retains the same complexity (i.e., NEXPTIME-complete) of the same fragments deprived of the equivalence relation. In the same work the authors proved that the satisfiability problem for the logic AA ∼ extended with metric constraints, namely MPNL∼, may be reduced to the reachability problem for Vec- tor Addition Systems with States (VASS) [11] whose complexity upper bound is still unknown. In this paper we make a step forward in complet- ing the picture by proving that the satisfiability problem for the missing fragment A ∼ extended with metric constraints, namely MRPNL∼, is in 3EXPSPACE and it is EXPSPACE-hard. Keywords: Interval Temporal Logic · Metric Constraints · Equivalence Relation · Complexity 1 Introduction Extending decidable fragments of first-order logic such as the two-variable frag- ment with pre-interpreted relations is a topic that has been explored in the last two decades [8, 10]. Many of such extensions increase the expressivity of the logic while retaining the decidability of the satisfiability problem [22]. Other exten- sions push the limit too hard and the relative satisfiability problem turns out to be undecidable [6, 9]. Among series of technically beautiful results the extensions of two-variable fragment of first-order logic, namely FO2, plays a crucial role. The satisfiability problem for this fragment and for its extension with a linear order relation, namely FO2[>], has been proved decidable for the most common kind of linear orders [20] including the reals [17]. In particular, FO2[>] has a very natural counterpart in the domain of Halpern and Shoham’s modal logic of intervals [7], HS for short. It has been proved that the logic is equivalent to the fragment of HS that features both “meets” and “met by” modalities [3, 12], called propositional neighborhood logic PNL or, alternatively, AA from its two modalities A (i.e., “adjacent to the right”) and A (i.e., “adjacent to the left”). Let us consider now the logic A, such (proper) 2 Pietro Sala fragment of PNL is referred to as right propositional neighborhood logic, RPNL for short, in the literature. RPNL may be seen as a future fragment of PNL, and thus of FO2[>], and presents many desirable properties that PNL does not. For instance, the extension of RPNL with the “begin” and ”begun by” modalities, i.e., the logic ABB, retains the decidability of the satisfiability problem on the most common classes of linear orders [4, 16], while the same extension applied to AA, namely the logic AABB, turns out to be undecidable over infinite Dedekind- complete linear orders and on the finite or general linear orders it is proved to be NON-PRIMITIVE-HARD [14, 15]. When we add a pre-interpreted propositional variable ∼ that behaves like an equivalence relation the differences w.r.t. the decidability of the satisfiability problem between ABB ∼ and AABB ∼ are even more accentuated. ABB ∼ turns out to be decidable on the finite linear orders [18], even if we take into consideration the more general synthesis problem [19], while AABB ∼ turns out to be undecidable on the most common classes of linear orders. In this paper we will prove the decidability for the satisfiability problem of MRPNL∼ over finite linear orders by providing tighter complexity bounds. In par- ticular, we prove that, when interpreted over finite linear orders, the satisfiability problem for the logic MRPNL∼ belongs to the complexity class 3EXPSPACE. More precisely, we provide a reduction from MRPNL∼ to the VASS coverabil- ity problem that will lead to an 3EXPSPACE decidability procedure. By giving this result we observe that MRPNL∼ w.r.t. its super-fragment MPNL∼ admits a known complexity bound, in fact in [2] a fragment of MPNL∼ was proved capable of encoding 0-0 reachability problem for Vector Addition Systems with States (VASS) [11]. Moreover, we prove that the satisfiability problem for MRPNL∼ is EXPSPACE-hard by means of a reduction to the coverability problem for Vector Addition Systems with States which was proved to be EXPSPACE-complete in [21]. We will observe that it turns out not so intuitive as in [2] and in [13] how satisfiability of MRPNL∼ may be reduced to the coverability for VASS. The paper is organized as follows. Section 2 provides a brief overview of the logic MRPNL∼ as well as some basic definitions used throughout the pa- per. Section 3 describes the steps for proving that the satisfiability problem for MRPNL∼ interpreted over finite linear orders belongs to the complexity class 3EXPSPACE. Section 4 describes the steps for proving that the satisfiability problem for MRPNL∼ interpreted over finite linear orders is EXPSPACE-hard. Finally, Section 5 summarizes the results presented in this work and points out some interesting research directions that may be developed starting from what is proved here. 2 The logic MRPNL∼ In this section we provide the syntax and the semantics of the Metric Right Propositional Logic extended with an equivalence relation, MRPNL∼ for short, interpreted over finite linear orders. Let N be the set of natural numbers and let N ⊆ N a finite prefix of it. We denote by IN = {[x, y] : x, y ∈ N, x ≤ y} MRPNL∼ 3 the set of all possible intervals on N . MRPNL∼ is a modal logic whose possible worlds are the elements of IN and the accessibility relation is given by the Allen interval relation “meets” [1] whose semantics is captured by the unary modality hAi. Given two intervals [x, y], [w, z] we say that [x, y] meets [w, z] if and only if y = w. Let P be a countable set of propositional variables whose elements are usually denoted with p1 , p2 , . . . and so on. In addition to P, the language of MRPNL∼ includes elements of N itself as special pre-interpreted propositional variables called interval lengths used for constraining the length of the intervals. More precisely, given k ∈ N we say that k holds over an interval [x, y] ∈ N if and only if y − x = k (i.e, [x, y] has length k). Finally, the language of MRPNL∼ features a special pre-interpreted propositional variable ∼ that represents an equivalence relation over N . In order to avoid clashes between variables, we assume (N ∪ {∼}) ∩ P = ∅. From now on we will denote MRPNL ∼ formulas with greek letters ϕ, ψ, . . . and so on. The syntax for MRPNL∼ formulas is the following: ϕ ::= p | n | ∼ | ¬ψ | ψ ∨ ψ | hAiψ with p ∈ P and n ∈ N In the following we will use ψ1 ∧ ψ2 as a shorthand for ¬(¬ψ1 ∨ ¬ψ2 ), ψ1 → ψ2 for ¬ψ1 ∨ ψ2 , ψ1 ↔ ψ2 for (ψ1 → ψ2 ) ∧ (ψ2 → ψ1 ), [A]ψ for ¬hAi¬ψ, 6∼ for ¬ ∼, > for p ∨ ¬p, ⊥ for ¬>, and [G]ψ (i.e., global modality) for ψ ∧ [A]ψ ∧ [A][A]ψ. Given an MRPNL ∼ formula ϕ let us denote with nϕ the maximum interval- length (if any) that appears in ϕ, if ϕ does not feature any interval length we assume nϕ = 0. Let Φ be the set of all possible MRPNL∼ formulas. For the sake of complexity considerations that will be done in Section 3 and Section 4 we define a recursive function length : Φ → N as follows:  1 if ϕ ∈ P ∪ N ∪ {∼} length(ϕ) = 1 + length(ψ) if ϕ = ¬ψ or ϕ = hAiψ length(ψ1 ) + length(ψ2 ) if ϕ = ψ1 ∨ ψ2  By means of function length we may define, given ϕ ∈ Φ, the size of ϕ, denoted with |ϕ|, as |ϕ| = length(ϕ) + log2 (nϕ + 2) (i.e, constants are supposed to be encoded in binary). A model for MRPNL ∼ is a pair M = (N, V, ∼N ) where V : IN → 2P and ∼N is an equivalence relation (i.e, a reflexive, symmetric, and transitive binary relation) over N . The semantics of MRPNL∼ formulas ϕ is given in terms of a pair M, [x, y], where M = (N, V, ∼N ) is a finite model for MRPNL∼ and [x, y] ∈ IN , as follows: – M, [x, y] |= p with p ∈ P if and only if p ∈ V([x, y]); – M, [x, y] |= n with n ∈ N if and only if y − x = n; – M, [x, y] |=∼ if and only if x ∼N y; – M, [x, y] |= ¬ψ if and only if M, [x, y] 6|= ψ; – M, [x, y] |= ψ1 ∨ ψ2 if and only if M, [x, y] |= ψ1 or M, [x, y] |= ψ2 ; – M, [x, y] |= hAiψ if and only if there exists z ∈ N s.t. z ≥ y and M, [y, z] |= ψ. We say that a formula ϕ is satisfiable if and only if there exists a finite model M = (N, V, ∼N ) for MRPNL∼ and an interval [x, y] ∈ IN such that M, [x, y] |= ϕ. Then the (finite) satisfiability problem for MRPNL ∼ consists of, given an 4 Pietro Sala MRPNL∼ ϕ, deciding whether or not there exists a model M = (N, V, ∼N ) and an interval [x, y] ∈ IN such that M, [x, y] |= ϕ. It will turn out useful in Section 3 to impose the satisfiability of the main formula ϕ to the first interval, namely [0, 0]. This is may be done safely using the following result. Theorem 1. For every MRPNL∼ formula ϕ there exists a model M = (N, V, ∼N ) and an interval [x, y] ∈ IN such that M, [x, y] |= ϕ if and only if there exists a model M0 = (N 0 , V 0 , ∼0N ) with N 0 ⊆ N such that M0 , [0, 0] |= hAiϕ. Given n ∈ N, we mayV impose that an interval has length greater than n by means of the formula ¬n0 . Moreover, we may force a propositional variable 0≤n0 ≤n > n to hold on all and only the V intervals with length greater than n by means of the formula [G](n> ↔ ¬n0 ). We will make use of such propositional 0≤n0 ≤n variables in Section 4 where, for the sake of clarity, we will identify with n≤ the negation of n> (i.e., n≤ holds on all and only the intervals with length less or equal than n). These letters are mere syntactic sugar expressible in semantics of MRPNL∼ provided above, however we prefer to assume them as pre-interpreted propositional variables like the ones in N or ∼. This is because the encoding ¬n0 is exponential in the size of n and this will affect the LOGSPACE V 0≤n0 ≤n reduction we want to provide in Section 4. However, despite the fact that a linear encoding of n> in MRPNL∼ (without embedding them in the semantics) is possible [5] we prefer to keep the things simple by adopting n> variables as pre-interpreted ones. 3 The MRPNL∼ finite satisfiability problem In this section we reduce the finite satisfiability problem for MRPNL∼ to the coverability problem for Vector Addition System with States, VASS for short. The key idea behind this reduction is to use the VASS machinery to explore a (candidate) model for ϕ starting from its maximum point and moving backwards. Since the hAi modality can only look forward, at every step the automaton consider the introduction of a new point x at the beginning of such suffix. At this point if the automaton may guarantee the consistency conditions for x (i.e., [A]- formulas) and the fulfilling of all the hAi-requests associated to x w.r.t. the suffix already explored then it may move to the next point or, if the input formula ϕ is witnessed, it may successfully terminate. On the other hand, if the automaton cannot guarantee the aforementioned consistency/fulfilling conditions for x then the computation fails. A vector addition system with states (VASS) is a tuple A = (Q, Σ, m, q0 , Qf , ∆) where Q is a finite set of states, Σ is a finite set of symbols called alphabeth, m ∈ N, q0 ∈ Q, Qf ⊆ Q is the set of final states, and ∆ ⊆ Q × Σ × Zn × Q. Given a vector v ∈ Zm and 1 ≤ j ≤ m we denote with P v[j] the value of the j-th component of v, moreover we define its size as |v[i]|. Given a vector 1≤i≤m MRPNL∼ 5 v ∈ Zm it turns out to be useful to express the sum of theP components until a given component 1 ≤ j ≤ m denoted as |v|j with |v|j = |v[i]|. Moreover, 1≤i≤j  + if v[j] ≥ 0 the sign of the component j is defined as sgnj (v) = . − otherwise Given a VASS A = (Q, Σ, m, q0 , Qf , ∆ we define its size |A| as |A| = 3 · |Q| · |Σ| · |∆| · m · (dlog2 (max{|v| : (q, σ, v, q 0 ) ∈ ∆}e + 1). A configuration C of a VASS A is a pair C = (q, v) where q ∈ Q and v ∈ Nm . Let CA be the set of all the possible configurations of A (i.e., CA = Q × Nm ). We define the transition relation over the configurations of A as →· ⊆ CA × Σ × CA where (q, v) →σ (q 0 , v 0 ) if and only if there exists a transition (q, σ, v, q 0 ) with q = q, q 0 = q 0 , σ = σ and v +v = v 0 . Given a word w = σ1 . . . σk in Σ ∗ , let →∗w be the reflexive and transitive closure of →· using w, that is, (q, v) →∗w (q 0 , v 0 ) if and only if one of the following two conditions holds: (i) w =  and (q, v) = (q 0 , v 0 ); (ii) (q, v) →σ1 . . . →σk (q 0 , v 0 ). Given a VASS A = (Q, Σ, m, q0 , F, ∆) the reachability problem for A consists of determining whether or not there exists a word w ∈ Σ ∗ such that (q0 , 0m ) →∗w (q, v) with q ∈ F . Given a VASS A = (Q, Σ, m, q0 , F, ∆) and a vector vf ∈ Nm the coverability problem for the pair (A, vf ) consists of determining whether or not there exists a word w ∈ Σ ∗ such that (q0 , 0m ) →∗w (q, v) with q ∈ F and v ≥ vf . The size of a coverability problem (A, vf ) is defined as |(A, vf )| = |A| · m · (dlog2 (|vf |)e + 1). Given a MRPNL∼ formula ϕ let C`ϕ be the set of all the sub-formulas of ϕ together with their negations plus the formulas hAiϕ and [A]¬ϕ and the set of ≤ sub-formulas {n, ¬n : 0 ≤ n ≤ nϕ } ∪ {n> ϕ , nϕ }. Given an MRPNL∼ formula ϕ an ϕ-atom F ⊆ C`ϕ is a maximal consistent subset of the closure, that is: – for every formula ψ ∈ closure either ψ ∈ F or ¬ψ ∈ F ; – for every formula ψ1 ∨ ψ2 ∈ C`ϕ we have ψ1 ∨ ψ2 ∈ F if and only ψ1 ∈ F or ψ2 ∈ F ; – there exists at most one 0 ≤ n ≤ nϕ such that n ∈ F ; – if 0 ∈ F then for every [A]ψ ∈ F we have ψ ∈ F . We denote the set of all possible ϕ-atoms with Atomsϕ , let us observe that |Atomsϕ | ≤ 2|ϕ|+1 · (nϕ + 2) ≤ 2O(|ϕ|) . Moreover, we define Atoms0ϕ to be the set of atoms F with 0 ∈ F (i.e., Atoms0ϕ = {F ∈ Atomsϕ : 0 ∈ F }) we call such atoms zero-atoms. Notice that, since the number of constants allowed to be positive in a zero-atom (as well as any ϕ-atom) is one (0 in this case), we · have that |Atoms0ϕ | ≤ 2|ϕ|+1 ≤ 2O(|ϕ|) . We define the relation ⇒⊆ Atoms0ϕ × (Atomsϕ \ Atoms0ϕ ) × Atoms0ϕ between pair of zero-atoms and atoms as follows. G For every F, F 0 ∈ Atoms0ϕ and for every G ∈ Atomsϕ \ Atoms0ϕ we have F ⇒ F 0 if and only if for every {ψ : [A]ψ ∈ F }∪{[A]ψ ∈ F 0 }∪{hAiψ ∈ F 0 } ⊆ G. Given a zero atom F a resolution for F is a minimal set resF = {(G01 , G1 ), . . . , (G0k , Gk )} of pairs in Atoms0ϕ × Atomsϕ \ Atoms0ϕ such that: G 0 – for every 1 ≤ k 0 ≤ k we have F ⇒k G0k0 ; – for every hAiψ ∈ F we have ψ ∈ F or there exists 1 ≤ k 0 ≤ k such that ψ ∈ Gk0 ; – for every 1 ≤ n ≤ nϕ there exists at most one k 0 such that n ∈ Gk0 . 6 Pietro Sala For every F ∈ Atoms0ϕ let ResF be the set of all its possible resolutions for S constraint forces |{hAiψ ∈ C`ϕ }| ≤ 2|ϕ| F . Notice that, since the minimality |ϕ|, we have that k ≤ |ϕ|. Let Res = ResF we have |Res| ≤ |Atomsϕ | . F ∈Atoms0ϕ A ϕ-class-witness is a multi-set W whose elements are drawn from Atoms0ϕ . Moreover, every ϕ-class-witness satisfies the condition that for every F ∈ Atoms0ϕ we have W (F ) ≤ |ϕ| + nϕ + 1. We denote with Witnessesϕ the set of all possi- ble ϕ-class-witnesses. We define a witness-union tϕ operator on Witnessesϕ as follows. Let W, W 0 , and W 00 in Witnessesϕ we say that W tϕ W 0 = W 00 if and only if for every G ∈ Atoms0ϕ we have: W (G) + W 0 (G) if W (G) + W 0 (G) ≤ |ϕ| + nϕ + 1  W 00 (G) = |ϕ| + nϕ + 1 otherwise It is easy to see that Witnessesϕ is closed under tϕ , moreover Witnessesϕ is fi- 0 |ϕ|+1 nite and its size is |Witnessesϕ | ≤ (|ϕ|+nϕ +2)|Atomsϕ | ≤ 2log(|ϕ|+nϕ +2)·2 ≤ 2O(|ϕ|) 2 . A ϕ-state is a tuple S = (W, ∼nϕ , hornϕ , witnϕ ) where: – W is a finite multi-set of ϕ-class-witnesses W = {W1 , . . . , Wm }; – ∼nϕ is an equivalence relation over (a prefix of) {0, . . . , nϕ } (i.e., ∼nϕ is a partition of a prefix of {0, . . . , nϕ }); – hornϕ is a partial function hornϕ : {0, . . . , nϕ } → Atoms0ϕ called horizon function which for every 0 ≤ n ≤ nϕ such that for every 0 ≤ n ≤ nϕ if hornϕ (n) is defined then hornϕ (n0 ) is defined for every 0 ≤ n0 ≤ n; – witnϕ is a partial function witnϕ : {0, . . . , nϕ } → Witnessesϕ called wit- nesses function such that for every 0 ≤ n ≤ nϕ if witnϕ (n) is defined if and only if hornϕ (n) is defined. Moreover for every n ∼nϕ n0 for which both witnϕ (n) and witnϕ (n0 ) are defined we have witnϕ (n) = witnϕ (n0 ); – for every 0 ≤ n ≤ nϕ we have {hornϕ (n0 ) : n0 ∼nϕ n} ⊆ witnϕ (n). In the following we will use the symbol ⊥ to denote undefined values for functions hornϕ and witnϕ . Let us observe that the above constraints imply that for every 0 ≤ n ≤ nϕ we have hornϕ (n) ∈ witnϕ (n). We denote with Statesϕ the set S of all possible ϕ-states. Given a ϕ-state S = (W, ∼nϕ , hornϕ , witnϕ ) let N∼ the S S S subset N∼nϕ ⊆ {0, . . . nϕ } such that n ∈ N∼nϕ ↔ n = min[n]∼nϕ , thus |N∼nϕ | is S the index of ∼nϕ . We denote with W∼nϕ the multi-set {witnϕ (n) : n ∈ N∼ nϕ }. Moreover, we denote W∼nϕ the multi-set W∼nϕ = {witnϕ (n) \ {hornϕ (n0 ) : f ar f ar n0 ∼nϕ n : n ∈ N∼ S nϕ }}. Each element Wi in W∼ f ar nϕ witnessed the zero-atoms for points that belongs to a class of a point n in ∼nϕ but they are at distance greater than nϕ w.r.t. the current horizon, this is why we call such points far points. Moreover, we define W∼ f ar/0 nϕ = {witnϕ (n) \ {hornϕ (n0 ) : n0 ∼nϕ n : n ∈ S f ar N∼ nϕ \ {0}}} (i.e., same as W∼ nϕ but without the multi-set for the far points in the equivalence class of 0). · Now, we define a reachability relation ⊆ Statesϕ × Atoms0ϕ × Statesϕ between ϕ-states. Given two ϕ-states S = (W, ∼nϕ , hornϕ , witnϕ ), S 0 = (W 0, ∼0nϕ , F horn0 ϕ , wit0nϕ ) and a zero atom F ∈ Atoms0ϕ we have that S S 0 if and only MRPNL∼ 7 if there exists a resolution resF = {(G01 , G1 ), . . . , (G0k , Gk )} in ResF such that: Local Consistency conditions: (LC1) horn0 ϕ (0) = F and for every 0 ≤ n < nϕ we have horn0 ϕ (n+1) = hornϕ (n); (LC2) for every 0 ≤ n, n0 < nϕ we have n + 1 ∼0nϕ n0 + 1 if and only if n ∼nϕ n0 ; (LC3) for every 0 < n ≤ nϕ such that n 6∼0nϕ 0 we have wit0nϕ (n) = witnϕ (n−1); (LC4) if there exists 0 < n ≤ nϕ such n ∼0nϕ 0 we have that wit0nϕ (0) = witnϕ (n − 1) tϕ {F }; (LC5) for every 0 < n ≤ nϕ we have that if n ∼0nϕ 0 (resp., n 6∼0nϕ 0) then there G exists G with {n, ∼} ⊆ G (resp., {n, 6∼} ⊆ G) such that F ⇒ hornϕ (n); (LC6) for every F 0 ∈ wit0nϕ (0) \ {horn0 ϕ (n) : n ∼0nϕ 0} we have that there exists G G such that F ⇒ F 0 with {∼, n> ϕ } ⊆ G; (LC7) for every 0 < n ≤ nϕ such that n 6∼0nϕ 0 and for every F 0 ∈ wit0nϕ (n) \ G {horn0 ϕ (n0 ) : n0 ∼0nϕ n} there exists G such that F ⇒ F 0 with {6∼, n> ϕ } ⊆ G; Local Fulfilling conditions: (LF1) for every 0 < n ≤ nϕ such that there exists 1 ≤ k 0 ≤ k with {n} ⊆ Gk0 we have horn0 ϕ (n) = G0k0 ; (LF2) for every 0 < n ≤ nϕ such that there exists 1 ≤ k 0 ≤ k with {n, ∼} ⊆ Gk0 (resp., {n, 6∼} ⊆ Gk0 ) we have n ∼0nϕ 0 (resp., n 6∼0nϕ 0); (LF3) {G0k0 : 1 ≤ k 0 ≤ k ∧ {n> 0 0 0 ϕ , ∼} ⊆ Gk0 } ⊆ (witnϕ (0) \ {hornϕ (n) : n ∼nϕ 0}); Global Consistency conditions: (GC1) if there exists 0 < n ≤ nϕ such that n ∼0nϕ 0 we have that W 0 = (W \ {witnϕ (n − 1)}) ∪ {wit0nϕ (0)} (i.e., we have “updated” one ϕ-class- witness in W that contains a point in the last nϕ points considered); (GC2) if for every 0 < n ≤ nϕ such n6∼0nϕ 0 and wit0nϕ (0) = {F } we have W 0 = W ∪ {wit0nϕ (0)} (i.e., we have “inserted” one new ϕ-class-witness in W); (GC3) if we have |wit0nϕ (0)| > 1 and n6∼0nϕ 0 for every 0 < n ≤ nϕ then there exists W ∈ W \ W∼nϕ such that W 0 = (W \ {W }) ∪ {W tϕ {F }} (i.e., we have “updated” one ϕ-class-witness in W that does not contain a point in the last nϕ points considered); (GC4) for every W ∈ W 0 \ W∼ 0 0 n and for every F 0 ∈ W we have that there ϕ G 0 exists G such that F ⇒ F with {6∼, n> ϕ } ⊆ G; Global Fulfilling condition: (GF1) {G0k0 : 1 ≤ k 0 ≤ k ∧ {n> 0 0 f ar/0 ϕ , 6∼} ⊆ Gk0 } ⊆ ((W \ W∼0n ) ∪ W∼nϕ ). ϕ wf Given a word wf = F1 . . . Fk on the alphabeth (Atoms0ϕ )∗ , let ∗ be the re- · wf flexive and transitive closure of using wf , that is, S ∗ S 0 if and only if one 0 F1 Fk 0 of the following two conditions holds: (i) wf =  and S = S ; (ii) S ... S. · We may prove the following result on the relation . Theorem 2. Given an MRPNL∼ formula ϕ we have that ϕ is finitely satisfiable if and only if there exists a word of zero-atoms wf = F1 . . . Fr ∈ (Atoms0ϕ )∗ and 8 Pietro Sala two ϕ-states S0 , Sf ∈ SM such that hAiϕ ∈ Fr , W 0 = ∅, for every 0 ≤ n ≤ nϕ wf we have horn0 ϕ (n) = wit0nϕ (n) = ⊥ , and S0 ∗ Sf . · Before encoding into a VASS we need some additional definitions in order to deal with purely technical details in such encoding. A distinct function is any function distϕ : Atoms0ϕ → {0, unique, distinct}. Let Distϕ the set of all possible 0 O(|ϕ|) distinct functions, it is easy to prove that |Distϕ | = 3|Atomsϕ | ≤ 22 . More- over, we say that a multi-set WGF whose elements are drawn from Witnessesϕ is a global fulfilling set if and only if |WGF | ≤ |ϕ|. Let GFull the set of all possible 0 global fulfilling sets, it is easy to prove that |GFull| = (|ϕ| + nϕ + 2)|Atomsϕ | ≤ O(|ϕ|) 22 . Let Eqn∼ϕ be the set of all possible ∼nϕ , that is, all the possible equiv- alence relations (i.e., partitions) on sets with cardinalities ranging from 1 to nϕ + 1 plus the empty set which will be our starting ∼nϕ . Set Eqn∼ϕ is finite and we have |Eqn∼ϕ | ≤ 2|ϕ| log(|ϕ|) + 1 ≤ 2O(|ϕ| log(|ϕ|) . Let Horϕ (resp., Witϕ ) the set of all possible horizon (resp., witness) functions, we have that |Horϕ | ≤ 2 |ϕ| (|Atoms0ϕ | + 1)nϕ +1 ≤ 2O(|ϕ| ) (resp., Witϕ ≤ (|Witnessesϕ | + 1)nϕ +1 ≤ 22 ). Now we have all the ingredients for defining a VASS Aϕ that encodes the · relation . We begin by pointing out that the vectors w in the computation of Aϕ are indexed with the elements of Witnessesϕ since they represent a portion of multi-sets in W. Given two multi-sets W, W 0 whose elements are drawn from Witnessesϕ , we will define the difference W − W 0 operation, which is different from the multi-set operation W \ W 0 , as the operation that returns the vector v ∈ Z|Witnessesϕ | (indexed on the elements of Witnessesϕ ) which is such that v[W ] = W(W ) − W 0 (W ) for every W ∈ Witnessesϕ . Given an input MRPNL∼ formula ϕ we define the VASS Aϕ = (Q, Σ, m, Qf , ∆) where Q = Eqn∼ϕ × Horϕ × Witϕ × Distϕ × GFull, Σ = Atoms0ϕ × Res × Witnessesϕ , m = |Witnessesϕ |, q0 = (∅, ⊥, ⊥, 0, ∅), Qf = {(∼nϕ , hornϕ , witnϕ , distϕ , WGF ) ∈ Q : hAiϕ ∈ hornϕ (0)}. Moreover we have ((∼nϕ , hornϕ , witnϕ , distϕ , WGF ), (F, ResF , W ), w, (∼0nϕ , horn0 ϕ , wit0nϕ , gc0 , dist0ϕ , WGF 0 )) ∈ ∆ if and only if the following conditions hold (let resF = {(G1 , G1 ), . . . , (Gk , G0k )}): 0 1. W tϕ {F } = wit0nϕ (0) and both local consistency conditions and lo- cal fulfilling conditions are satisfied by hornϕ , witnϕ , F, resF , horn0 ϕ and wit0nϕ ;  WGF if nϕ 6= min[nϕ ]∼nϕ 2. let Wout = WGF ∪ {witnϕ (nϕ ) tϕ hornϕ (nϕ )} otherwise 0 Wout − WGF if 0 6= max[0]∼0nϕ  then we have w = 0 ; Wout − (WGF ∪ {W }) otherwise 3. for every F 0 ∈ Atoms0ϕ if dist0ϕ (F 0 ) = distinct or dist0ϕ (F 0 ) = unique ∧ F 0 ∈ / (wit0nϕ (0) \ {hornϕ (n) : n ∼0nϕ 0}) then there exists G with {6∼, n> ϕ } ∈ G G with F ⇒ F 0 ; MRPNL∼ 9 4. for every F 0 ∈ Atoms0ϕ : 0 0   distinct if horn0ϕ (nϕ ) = F , distϕ (F ) = unique,  and F ∈ / (witnϕ (nϕ ) \ {hornϕ (n) : n ∼nϕ nϕ })  dist0ϕ (F 0 ) = 0 0 ;  unique if horn ϕ (n ϕ ) = F and distϕ (F ) = 0 distϕ (F 0 ) otherwise   0 0 5. {Gk : 1 ≤ k 0 ≤ k, {6∼, n> k S S ϕ} ⊆ G } ⊆ ( W∪ W ). 0 W ∈WGF f ar/00 W ∈W∼0 nϕ The following result basically guarantees the soundness and completeness of the above reduction. Theorem 3. For every pair of configurations C = ((∼nϕ , hornϕ , witnϕ , distϕ , WGF ), W), C 0 = ((∼0nϕ , horn0 ϕ , wit0nϕ , dist0ϕ , WGF 0 ), W 0 ) and every symbol σ = (F, ResF , W ) ∈ Σ we have that C →σ C 0 in Aϕ if and only if (W∼nϕ ∪ WGF ∪ F 0 0 W, ∼nϕ , hornϕ , witnϕ ) (W∼ 0 n ∪ WGF ∪ W 0 , ∼0nϕ , horn0 ϕ , wit0nϕ ). ϕ Let us consider now the size of Aϕ . According to the complexity bounds given O(|ϕ|) O(|ϕ|) O(|ϕ|) so far we have |Q| ≤ 22 , |Σ| ≤ 22 , |∆| ≤ 22 , and (dlog2 (max{|v| : (q, σ, v, q 0 ) ∈ ∆}e + 1) ≤ 2dlog2 |ϕ|e. Finally we have that: O(|ϕ|) |Aϕ | ≤ 22 which is doubly exponential in the size of |ϕ|. We may use the VASS coverability w problem on Aϕ to see if (∅, ⊥, ⊥) ∗ (W, hornϕ , witnϕ ) with hAiϕ ∈ hornϕ (0). Then, since the VASS coverability problem is EXPSPACE-complete [21], we conclude this section with the following result. Theorem 4. The finite satisfiability problem for MRPNL∼ belongs to the com- plexity class 3EXPSPACE. 4 EXPSPACE-hardness of MRPNL∼ In this section we provide a LOGSPACE reduction from the coverability prob- lem for Vector Addition Systems with States to the (finite) satisfiability problem for MRPNL∼, thus proving that the latter is EXPSPACE-hard. Given a VASS A = (Q, Σ, m, q0 , Qf , ∆) and a vector vf ∈ Nm we write a formula ϕA , with |ϕA | = O(|A| + |vf |) which is satisfiable if and only if (A, vf ) is a positive in- stance of the coverability problem for VASS. The idea behind ϕ is to encode all the possible computations of A (if any) beginning in (q0 , 0) and finishing in a con- figurations (q, v) with v ≥ vf . As a matter of fact, we will encode a slightly differ- ent problem. Let q̂f ∈/ Qf be a fresh state we define A0 = (Q0 , Σ, m, q0 , {q̂f }, ∆0 ) where Q = Q ∪ {q̂f } and ∆0 = ∆ ∪ {(q, σ, −vf , q̂f ) : q ∈ Qf , σ ∈ Σ}. It is easy 0 to prove that (A, vf ) is a positive instance of the coverability problem for VASS 10 Pietro Sala if and only if A0 is a positive instance of the reachability problem. Let us begin by encoding the sequence of configurations of A0 . The computation is encoded backwards with respect to the temporal domain. In order to do this we make use of |Q| propositional variables qi ∈ Q for encoding states and 2 · m propositional variables C + = {c+ + 1 , . . . , cm } and C − = {c− − 1 , . . . , cm }, for encoding counters in the computation of A, we impose the uniqueness over each point in the model for all these variables by means of the following formulas:    ^ ^ ψ! = [G] 0 ↔ p → ¬p0  p∈Q∪C + ∪C − p0 ∈((Q∪C + ∪C − )\{p})   _ ψ∃ = [G] 0 ↔ p p∈Q∪C + ∪C − In order to simplify the encoding we introduce |∆|, auxiliary variables, for better encoding the transition relation. Let ∆ = {(q 1 , σ 1 , v 1 , q 1 ), . . . , (q h , σ h , v h , q h )} then we introduce h auxiliary variables ∆ = {δ1 , . . . , δh }, constrained as follows:    ^ ^ ψ!∆ = [G]  δi → q i ∧ ¬δj0  δi ∈∆ δj ∈(∆\{δj })    ^ _ ∆ q ∧ hAi> → ψQ = [G]  δi  q∈Q δi ∈{δj ∈∆: q j =q} Basically any state but the first one in a sequence of configurations is labelled with the transition in ∆ that has generated it. Each transition δi ∈ ∆ is encoded by first putting a point labelled with q i (i.e., the target state) on the current point x and then, according to v i , a sequence of |v i | points labelled with components c∗j with ∗ ∈ {−, +} and 1 ≤ j ≤ m, finally, point x + |v| + 1 is labelled with q i (i.e., the source state). For every δi ∈ ∆ this is done by means of the following formula: sgn (v i )   hAi(|v i | + 1 ∧ hAiq i ) ∧ [A](0> ∧ |v i |≤ 1 → hAi(0 ∧ c1 1 ))∧ ψ δi = [G] δ i → V i ≤ sgnj (v i ) [A](|v i |>  j−1 ∧ |v |j → hAi(0 ∧ cj ))) 1 > j−1 ∧ |v |j and 0 ∧ |v |1 i are false and thus the case where components of vector v with value 0 is treated in a transparent way. Now we have to deal with the problem of ensuring that each counter is correctly incremented/decremented along the computation. Since we are in the coverability problem the only thing that we must ensure is that a decrement of a component cannot happen if there is not a corresponding incre- ment “before” in the computation. Let us recall that in our encoding “before” means in the future with respect to the temporal domain. At this point, the equivalence relation ∼ comes into play by mapping, for each 1 ≤ j ≤ m, each MRPNL∼ 11 point labelled with c− + j into a point labelled cj in its “future”. It is worth noticing that we must guarantee that such mapping is injective. This is why the proper- ties of ∼ are crucial. The aforementioned mapping is achieved by means of the following formula:   ^ ψ inj = [G]  c− +   j → [A](¬0∧ ∼→ [A](¬0 →6∼)) ∧ hAi(∼ ∧hAicj ) 1≤j≤m Finally, we just force our model to have a q0 -labelled point as its maximum and a in q̂f -labelled point as its minimum. This is achieved by means of the following formula: max ψmin = 0 ∧ q̂f ∧ hAi([A]0 ∧ hAiq0 ) The formula ϕ is defined as ϕA = ψ! ∧ ψ∃ ∧ ψ!∆ ∧ ψQ A ∆ V δi ∧ ψ ∧ ψ inj ∧ ψmin max δi ∈∆ It is long, tedious and trivial to prove that ϕA is finitely satisfiable if and only if there q̂f is reachable from (q0 , 0m ) in A0 . Let us notice that, since the constants are expressed in binary, we have |ϕ| = O(|A0 |). It is easy to prove that this translation may be done in logarithmic space and thus we have the following result. Theorem 5. The finite satisfiability problem for MRPNL∼ is EXPSPACE-hard. 5 Conclusions In this paper we proved that the satisfiability problem for the logic MRPNL∼ is decidable over finite linear orders with elementary complexity. More precisely, we proved that such problem belongs to the complexity class 3EXPSPACE and it is EXPSPACE-hard. In the not-so-distant future we plan to address the ex- act complexity of this problem. Moreover, since MRPNL∼ represents a weaker but, in principle, computationally more treatable version of its super-fragment MPNL∼ we plan to study the properties that can be captured by MRPNL∼ as well as properties that separate the two fragments (i.e., properties expressible in MPNL ∼ that cannot be expressed in MPNL ∼). Finally, we plan to study the decidability/complexity of satisfiability problem for MRPNL ∼ when it is interpreted over N. References 1. Allen, J.F.: Maintaining knowledge about temporal intervals. Commun. ACM 26(11), 832–843 (Nov 1983). https://doi.org/10.1145/182.358434 2. Bojańczyk, M., David, C., Muscholl, A., Schwentick, T., Segoufin, L.: Two- variable logic on data words. ACM Trans. Comput. Log. 12(4), 27:1–27:26 (2011). https://doi.org/10.1145/1970398.1970403 3. Bresolin, D., Goranko, V., Montanari, A., Sciavicco, G.: Propositional interval neighborhood logics: Expressiveness, decidability, and unde- cidable extensions. Ann. Pure Appl. Logic 161(3), 289–304 (2009). https://doi.org/10.1016/j.apal.2009.07.003 12 Pietro Sala 4. Bresolin, D., Montanari, A., Sala, P., Sciavicco, G.: What’s decidable about halpern and shoham’s interval logic? the maximal fragment ABBL. In: LICS 2011. pp. 387– 396 (2011). https://doi.org/10.1109/LICS.2011.35 5. Bresolin, D., Montanari, A., Sala, P., Sciavicco, G.: Optimal decision procedures for MPNL over finite structures, the natural numbers, and the integers. Theor. Comput. Sci. 493, 98–115 (2013). https://doi.org/10.1016/j.tcs.2012.10.043 6. Grädel, E., Otto, M., Rosen, E.: Undecidability results on two-variable logics. In: STACS 97. pp. 249–260 (1997). https://doi.org/10.1007/BFb0023464 7. Halpern, J.Y., Shoham, Y.: A propositional modal logic of time intervals. J. ACM 38(4), 935–962 (Oct 1991). https://doi.org/10.1145/115234.115351 8. Kieronski, E.: Results on the guarded fragment with equivalence or transitive re- lations. In: CSL 2005. pp. 309–324 (2005). https://doi.org/10.1007/11538363 22 9. Kieronski, E., Otto, M.: Small substructures and decidability issues for first-order logic with two variables. In: (LICS 2005). pp. 448–457 (2005). https://doi.org/10.1109/LICS.2005.49 10. Kieronski, E., Pratt-Hartmann, I., Tendera, L.: Equivalence closure in the two-variable guarded fragment. J. Log. Comput. 27(4), 999–1021 (2017). https://doi.org/10.1093/logcom/exv075, https://doi.org/10.1093/logcom/exv075 11. Leroux, J.: Vector addition system reachability problem: a short self-contained proof. In: POPL 2011. pp. 307–316 (2011). https://doi.org/10.1145/1926385.1926421 12. Montanari, A., Pazzaglia, M., Sala, P.: Metric propositional neighborhood logic with an equivalence relation. In: TIME 2014. pp. 49–58 (2014). https://doi.org/10.1109/TIME.2014.26 13. Montanari, A., Pazzaglia, M., Sala, P.: Metric propositional neighborhood logic with an equivalence relation. Acta Inf. 53(6-8), 621–648 (2016). https://doi.org/10.1007/s00236-016-0256-3 14. Montanari, A., Puppis, G., Sala, P.: Maximal decidable fragments of halpern and shoham’s modal logic of intervals. In: ICALP 2010. pp. 345–356 (2010). https://doi.org/10.1007/978-3-642-14162-1 29 15. Montanari, A., Puppis, G., Sala, P.: Decidability of the interval temporal logic $\mathsf{A\bar{A}B\bar{B}}$ over the rationals. In: MFCS 2014. pp. 451–463 (2014). https://doi.org/10.1007/978-3-662-44522-8 38 16. Montanari, A., Puppis, G., Sala, P., Sciavicco, G.: Decidability of the interval temporal logic ABB over the natural numbers. In: STACS. pp. 597–608 (2010). https://doi.org/10.4230/LIPIcs.STACS.2010.2488 17. Montanari, A., Sala, P.: An optimal tableau system for the logic of tem- poral neighborhood over the reals. In: TIME 2012. pp. 39–46 (2012). https://doi.org/10.1109/TIME.2012.18 18. Montanari, A., Sala, P.: Adding an equivalence relation to the interval logic ABB: complexity and expressiveness. In: LICS 2013. pp. 193–202 (2013). https://doi.org/10.1109/LICS.2013.25 19. Montanari, A., Sala, P.: Interval-based synthesis. In: GandALF 2014. pp. 102–115 (2014). https://doi.org/10.4204/EPTCS.161.11 20. Otto, M.: Two variable first-order logic over ordered domains. J. Symb. Log. 66(2), 685–702 (2001). https://doi.org/10.2307/2695037, https://doi.org/10.2307/2695037 21. Rackoff, C.: The covering and boundedness problems for vector addition systems. Theoretical Computer Science 6(2), 223–231 (1978) 22. Szwast, W., Tendera, L.: Foˆ2 with one transitive relation is decidable. In: STACS 2013. pp. 317–328 (2013). https://doi.org/10.4230/LIPIcs.STACS.2013.317