In [13] Montanari et al. proved that the satis ability problem 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 satis ability problem for the logic AA extended with metric constraints, namely MPNL , may be reduced to the reachability problem for Vector Addition Systems with States (VASS) [11] whose complexity upper bound is still unknown. In this paper we make a step forward in completing the picture by proving that the satis ability problem for the missing fragment A extended with metric constraints, namely MRPNL , is in 3EXPSPACE and it is EXPSPACE-hard.
Extending decidable fragments of rst-order logic such as the two-variable
fragment with pre-interpreted relations is a topic that has been explored in the last
two decades [
In particular, FO2[>] has a very natural counterpart in the domain of Halpern
and Shoham's modal logic of intervals [
In this paper we will prove the decidability for the satis ability problem of
MRPNL over nite linear orders by providing tighter complexity bounds. In
particular, we prove that, when interpreted over nite linear orders, the satis ability
problem for the logic MRPNL belongs to the complexity class 3EXPSPACE.
More precisely, we provide a reduction from MRPNL to the VASS
coverability 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 [
The paper is organized as follows. Section 2 provides a brief overview of the logic MRPNL as well as some basic de nitions used throughout the paper. Section 3 describes the steps for proving that the satis ability problem for MRPNL interpreted over nite linear orders belongs to the complexity class 3EXPSPACE. Section 4 describes the steps for proving that the satis ability problem for MRPNL interpreted over nite 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
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 nite linear orders. Let N be the set of natural numbers and
let N N a nite pre x of it. We denote by IN = f[x; y] : x; y 2 N; x yg
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" [
Theorem 1. For every MRPNL formula ' there exists a model M = (N; V; N ) and an interval [x; y] 2 IN such that M; [x; y] j= ' if and only if there exists a model M0 = (N 0; V0; 0N ) with N 0 N such that M0; [0; 0] j= hAi'.
Given n 2 N, we may impose that an interval has length greater than n by means of the formula V :n0. Moreover, we may force a propositional variable 0 n0 n n> to hold on all and only the intervals with length greater than n by means of the formula [G](n> $ V :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
V :n0 is exponential in the size of n and this will a ect the LOGSPACE
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 [
The MRPNL
nite satis ability problem In this section we reduce the nite satis ability 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 su x. At this point if the automaton may guarantee the consistency conditions for x (i.e., [A]formulas) and the ful lling of all the hAi-requests associated to x w.r.t. the su x 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/ful lling 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 nite set of states, is a nite set of symbols called alphabeth, m 2 N, q0 2 Q, Qf Q is the set of nal states, and Q Zn Q. Given a vector v 2 Zm and 1 j m we denote with v[j] the value of the j-th component of v, moreover we de ne its size as P jv[i]j. Given a vector 1 i m v 2 Zm it turns out to be useful to express the sum of the components until a given component 1 j m denoted as jvjj with jvjj = P jv[i]j. Moreover, 1 i j the sign of the component j is de ned as sgnj (v) = + iofthv[ejr]wise0 . Given a VASS A = (Q; ; m; q0; Qf ; we de ne its size jAj as jAj = 3 jQj j j j j m (dlog2(maxfjvj : (q; ; v; q0) 2 ge + 1).
A con guration C of a VASS A is a pair C = (q; v) where q 2 Q and v 2 Nm. Let CA be the set of all the possible con gurations of A (i.e., CA = Q Nm). We de ne the transition relation over the con gurations of A as ! CA CA where (q; v) ! (q0; v0) if and only if there exists a transition (q; ; v; q0) with q = q, q0 = q0, = and v +v = v0. Given a word w = 1 : : : k in , let !w be the re exive and transitive closure of ! using w, that is, (q; v) !w (q0; v0) if and only if one of the following two conditions holds: (i) w = and (q; v) = (q0; v0); (ii) (q; v) ! 1 : : : ! k (q0; v0). Given a VASS A = (Q; ; m; q0; F; ) the reachability problem for A consists of determining whether or not there exists a word w 2 such that (q0; 0m) !w (q; v) with q 2 F . Given a VASS A = (Q; ; m; q0; F; ) and a vector vf 2 Nm the coverability problem for the pair (A; vf ) consists of determining whether or not there exists a word w 2 such that (q0; 0m) !w (q; v) with q 2 F and v vf . The size of a coverability problem (A; vf ) is de ned as j(A; vf )j = j j m (dlog2(jvf j)e + 1).
A
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 fn; :n : 0 n n'g [ fn'>; n' g. Given an MRPNL formula ' an '-atom F C`' is a maximal consistent subset of the closure, that is: { for every formula 2 closure either 2 F or : 2 F ; { for every formula 1 _ 2 2 C`' we have 1 _ 2 2 F if and only 1 2 F or 2 2 F ; { there exists at most one 0 n n' such that n 2 F ; { if 0 2 F then for every [A] 2 F we have 2 F .
We denote the set of all possible '-atoms with Atoms', let us observe that jAtoms'j 2j'j+1 (n' + 2) 2O(j'j). Moreover, we de ne Atoms0' to be the set of atoms F with 0 2 F (i.e., Atoms0' = fF 2 Atoms' : 0 2 F g) 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 jAtoms0'j 2j'j+1 2O(j'j). We de ne the relation ) Atoms0' (Atoms' n Atoms0') Atoms0' between pair of zero-atoms and atoms as follows. For every F; F 0 2 Atoms0' and for every G 2 Atoms' n Atoms0' we have F )G F 0 if and only if for every f : [A] 2 F g [ f[A] 2 F 0g [ fhAi 2 F 0g G. Given a zero atom F a resolution for F is a minimal set resF = f(G01; G1); : : : ; (G0k; Gk)g of pairs in Atoms0' Atoms' n Atoms0' such that: { for every 1 { for every hAi
2 Gk0 ; { for every 1 k0 n
k we have F G)k0 G0k0 ; 2 F we have 2 F or there exists 1 k0 k such that n' there exists at most one k0 such that n 2 Gk0 . For every F 2 Atoms0' let ResF be the set of all its possible resolutions for F . Notice that, since the minimality constraint forces jfhAi 2 C`'gj j'j, we have that k j'j. Let Res = S ResF we have jResj jAtoms'j2j'j.
F 2Atoms0'
A '-class-witness is a multi-set W whose elements are drawn from Atoms0'. Moreover, every '-class-witness satis es the condition that for every F 2 Atoms0 ' we have W (F ) j'j + n' + 1. We denote with Witnesses' the set of all possible '-class-witnesses. We de ne 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 2 Atoms0' we have:
W 00(G) =
W (G) + W 0(G) if W (G) + W 0(G) j'j + n' + 1 otherwise j'j + n' + 1 It is easy to see that Witnesses' is closed under t', moreover Witnesses' is nite and its size is jWitnesses'j (j'j+n' +2)jAtoms0'j 2log(j'j+n'+2) 2j'j+1 22O(j'j) . A '-state is a tuple S = (W;
n' ; horn' ; witn' ) where: { W is a nite multi-set of '-class-witnesses W = fW1; : : : ; Wmg; { n' is an equivalence relation over (a pre x of) f0; : : : ; n'g (i.e., n' is a partition of a pre x of f0; : : : ; n'g); { horn' is a partial function horn' : f0; : : : ; n'g ! Atoms0' called horizon function which for every 0 n n' such that for every 0 n n' if horn' (n) is de ned then horn' (n0) is de ned for every 0 n0 n; { witn' is a partial function witn' : f0; : : : ; n'g ! Witnesses' called witnesses function such that for every 0 n n' if witn' (n) is de ned if and only if horn' (n) is de ned. Moreover for every n n' n0 for which both witn' (n) and witn' (n0) are de ned we have witn' (n) = witn' (n0); { for every 0 n n' we have fhorn' (n0) : n0 n' ng witn' (n). In the following we will use the symbol ? to denote unde ned values for functions horn' and witn' . Let us observe that the above constraints imply that for every 0 n n' we have horn' (n) 2 witn' (n). We denote with States' the set of all possible '-states. Given a '-state S = (W; n' ; horn' ; witn' ) let N S the subset N Sn' f0; : : : n'g such that n 2 N Sn' $ n = min[n] n' , thus jN Sn' j is the index of n' . We denote with W n' the multi-set fwitn' (n) : n 2 N Sn' g. Moreover, we denote Wfanr' the multi-set W n' far = fwitn' (n) n fhorn' (n0) : n0 n' n : n 2 N Sn' gg. Each element Wi in Wfanr' 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 de ne Wfanr'=0 = fwitn' (n) n fhorn' (n0) : n0 n' n : n 2 N Sn' n f0ggg (i.e., same as Wfanr' but without the multi-set for the far points in the equivalence class of 0).
Now, we de ne a reachability relation States' Atoms0' States' between '-states. Given two '-states S = (W; n' ; horn' ; witn' ), S0 = (W0; 0n' ; horn0' ; wit0n' ) and a zero atom F 2 Atoms0' we have that S F S0 if and only if there exists a resolution resF = f(G01; G1); : : : ; (G0k; Gk)g 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' fF g; (LC5) for every 0 < n
n' we have that if n 0n' 0 (resp., n 6 0n' 0) then there exists G with fn; g G (resp., fn; 6 g G) such that F )G horn' (n); (LC6) for every F 0 2 wit0n' (0) n fhorn0' (n) : n 0n' 0g we have that there exists fhorn0' (n0) : n0 0n' ng there exists G such that F )G F 0 with f6 ; n'>g G; Local Ful lling conditions: (LF1) for every 0 < n n' such that there exists 1 k0 k with fng Gk0 we have horn0' (n) = G0k0 ; (LF2) for every 0 < n n' such that there exists 1 k0 k with fn; g Gk0 (resp., fn; 6 g Gk0 ) we have n 0n' 0 (resp., n 6 0n' 0); (LF3) fG0k0 : 1 k0 k ^ fn'>; g Gk0 g (wit0n' (0) n fhorn0' (n) : n 0n' 0g); Global Consistency conditions: (GC1) if there exists 0 < n n' such that n 0n' 0 we have that W0 = (W n fwitn' (n 1)g) [ fwit0n' (0)g (i.e., we have \updated" one '-classwitness 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) = fF g we have W0 = W [ fwit0n' (0)g (i.e., we have \inserted" one new '-class-witness in W); (GC3) if we have jwit0n' (0)j > 1 and n6 0n' 0 for every 0 < n n' then there exists W 2 W n W n' such that W0 = (W n fW g) [ fW t' fF gg (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 2 W0 n W0 0n' and for every F 0 2 W we have that there (GF1) fG0k0 : 1
exists G such that F )G F 0 with f6 ; n'>g Global Ful lling condition: k0 k ^ fn'>; 6 g
Gk0 g
G; ((W0 n W0 0n' ) [ Wfanr'=0).
Given a word wf = F1 : : : Fk on the alphabeth (Atoms0') , let wf exive and transitive closure of using wf , that is, S S0 if and only if one of the following two conditions holds: (i) wf = and S = S0; (ii) S F1 : : : Fk S0. We may prove the following result on the relation .
be the rewf Theorem 2. Given an MRPNL formula ' we have that ' is nitely satis able if and only if there exists a word of zero-atoms wf = F1 : : : Fr 2 (Atoms0') and we have horn0' (n) = wit0n' (n) = ? , and S0 two '-states S0; Sf 2 SM such that hAi' 2 Fr, W0 = ;, for every 0 wf
Sf .
n n' Before encoding into a VASS we need some additional de nitions in order to deal with purely technical details in such encoding. A distinct function is any function dist' : Atoms0' ! f0; unique; distinctg. Let Dist' the set of all possible 22O(j'j) . Moredistinct functions, it is easy to prove that jDist'j = 3jAtoms0'j over, we say that a multi-set WGF whose elements are drawn from Witnesses' is a global ful lling set if and only if jWGF j j'j. Let GF ull the set of all possible global ful lling sets, it is easy to prove that jGF ullj = (j'j + n' + 2)jAtoms0'j 22O(j'j) . Let Eqn' be the set of all possible n' , that is, all the possible equivalence 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 nite and we have jEqn' j 2j'j log(j'j) + 1 2O(j'j log(j'j). Let Hor' (resp., Wit') the set of all possible horizon (resp., witness) functions, we have that jHor'j (jAtoms0'j + 1)n'+1 2O(j'j2) (resp., Wit' (jWitnesses'j + 1)n'+1 22j'j ).
Now we have all the ingredients for de ning 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; W0 whose elements are drawn from Witnesses', we will de ne the di erence W W0 operation, which is di erent from the multi-set operation W n W0, as the operation that returns the vector v 2 ZjWitnesses'j (indexed on the elements of Witnesses') which is such that v[W ] = W(W ) W0(W ) for every W 2 Witnesses'.
Given an input MRPNL formula ' we de ne the VASS A' = (Q; ; m; Qf ; ) where Q = Eqn' Hor' Wit' Dist' GF ull, = Atoms0' Res Witnesses', m = jWitnesses'j, q0 = (;; ?; ?; 0; ;), Qf = f( n' ; horn' ; witn' ; dist'; WGF ) 2 Q : hAi' 2 horn' (0)g. Moreover we have (( n' ; horn' ; witn' ; dist'; WGF ); (F; ResF ; W ); w; ( 0n' ; horn0' ; wit0n' ; gc0; dist0'; WG0F )) 2 if and only if the following conditions hold (let resF = f(G1; G01); : : : ; (Gk; G0k)g): 1. W t' fF g = wit0n' (0) and both local consistency conditions and local ful lling conditions are satis ed by horn' ; witn' ; F; resF ; horn0' and wit0n' ; 2. let Wout = WGF if n' 6= min[n'] n'
WGF [ fwitn' (n') t' horn' (n')g otherwise then we have w = Wout WG0F if 0 6= max[0] 0n' ;
Wout (WG0F [ fW g) otherwise 3. for every F 0 2 Atoms0' if dist0'(F 0) = distinct or dist0'(F 0) = unique ^ F 0 2= (wit0n' (0) n fhorn' (n) : n 0n' 0g) then there exists G with f6 ; n'>g 2 G with F )G F 0; 4. for every F 0 2 Atoms0': 8 if horn' (n') = F 0, dist'(F 0) = unique, >> distinct dist0'(F 0) = < and F 0 2= (witn' (n') n fhorn' (n) : n > unique if horn' (n') = F 0 and dist'(F 0) = 0 >: dist'(F 0) otherwise n' n'g) ; 5. fGk0 : 1 k0 k; f6 ; n'>g
Gk0 g ( S W 2WG0F
The following result basically guarantees the soundness and completeness of the above reduction.
Theorem 3. For every pair of con gurations C = (( n' ; horn' ; witn' ; dist'; WGF ); W), C0 = (( 0n' ; horn0' ; wit0n' ; dist0'; WG0F ); W0) and every symbol = (F; ResF ; W ) 2 we have that C !
C0 in A' if and only if (W n' [ WGF [
W; n' ; horn' ; witn' ) F (W0 0n' [ WG0F [ W0; 0n' ; horn0' ; wit0n' ).
Let us consider now the size of A'. According to the complexity bounds given
so far we have jQj 22O(j'j) , j j 22O(j'j) , j j 22O(j'j) , and (dlog2(maxfjvj :
(q; ; v; q0) 2 ge + 1) 2dlog2 j'je. Finally we have that:
jA'j
22O(j'j)
which is doubly exponential in the size of j'j. We may use the VASS coverability
problem on A' to see if (;; ?; ?) w (W; horn' ; witn' ) with hAi' 2 horn' (0).
Then, since the VASS coverability problem is EXPSPACE-complete [
Theorem 4. The nite satis ability problem for MRPNL belongs to the complexity class 3EXPSPACE. 4
In this section we provide a LOGSPACE reduction from the coverability problem for Vector Addition Systems with States to the ( nite) satis ability problem for MRPNL , thus proving that the latter is EXPSPACE-hard. Given a VASS A = (Q; ; m; q0; Qf ; ) and a vector vf 2 Nm we write a formula 'A, with j'Aj = O(jAj + jvf j) which is satis able if and only if (A; vf ) is a positive instance 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 nishing in a congurations (q; v) with v vf . As a matter of fact, we will encode a slightly di erent problem. Let q^f 2= Qf be a fresh state we de ne A0 = (Q0; ; m; q0; fq^f g; 0) where Q0 = Q [ fq^f g and 0 = [ f(q; ; vf ; q^f ) : q 2 Qf ; 2 g. It is easy to prove that (A; vf ) is a positive instance of the coverability problem for VASS if and only if A0 is a positive instance of the reachability problem. Let us begin by encoding the sequence of con gurations of A0. The computation is encoded backwards with respect to the temporal domain. In order to do this we make use of jQj propositional variables qi 2 Q for encoding states and 2 m propositional variables C+ = fc1+; : : : ; c+mg and C = fc1 ; : : : ; cmg, 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:
0 0 11 p02((Q[C+[C )nfpg)
:p0AA ^ p2Q[C+[C
0 In order to simplify the encoding we introduce j j, auxiliary variables, for better encoding the transition relation. Let = f(q1; 1; v1; q1); : : : ; (qh; h; vh; qh)g then we introduce h auxiliary variables = f 1; : : : ; hg, constrained as follows: 0 0 11 i2 0 0 q2Q
^ j2( nf jg)
: j0AA _ i2f j2 : qj=qg 11 iAA Basically any state but the rst one in a sequence of con gurations is labelled with the transition in that has generated it. Each transition i 2 is encoded by rst putting a point labelled with qi (i.e., the target state) on the current point x and then, according to vi, a sequence of jvij points labelled with components cj with 2 f ; +g and 1 j m, nally, point x + jvj + 1 is labelled with qi (i.e., the source state). For every i 2 this is done by means of the following formula:
0 ! hAi(jvij + 1 ^ hAiqi) ^ [A](0> ^ jvij1 ! hAi(0 ^ cs1gn1(vi)))^ 1
V [A](jvijj> 1 ^ jvijj ! hAi(0 ^ cjsgnj(vi)))) A 1<j m Notice that in case vi[j] = 0 then both conditions jvijj> 1 ^ jvijj and 0> ^ jvij1 are false and thus the case where components of vector vi 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 increment \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
^ 1 j m point labelled with cj 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 properties of are crucial. The aforementioned mapping is achieved by means of the following formula: 0 1 cj ! [A](:0^ ! [A](:0 !6 )) ^ hAi( ^hAicj+) A 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:
mmianx = 0 ^ q^f ^ hAi([A]0 ^ hAiq0) The formula 'A is de ned as 'A = ! ^ 9 ^ ! ^ Q ^
V i ^ inj ^ max min i2 It is long, tedious and trivial to prove that 'A is nitely satis able 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 j'j = O(jA0j). It is easy to prove that this translation may be done in logarithmic space and thus we have the following result.
Theorem 5. The nite satis ability problem for MRPNL is EXPSPACE-hard. 5
In this paper we proved that the satis ability problem for the logic MRPNL is decidable over nite 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 exact 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 satis ability problem for MRPNL when it is interpreted over N.