=Paper=
{{Paper
|id=Vol-2243/paper13
|storemode=property
|title=Metric Right Propositional Neighborhood Logic with an Equivalence Relation
|pdfUrl=https://ceur-ws.org/Vol-2243/paper13.pdf
|volume=Vol-2243
|authors=Pietro Sala
|dblpUrl=https://dblp.org/rec/conf/ictcs/Sala18
}}
==Metric Right Propositional Neighborhood Logic with an Equivalence Relation==
https://ceur-ws.org/Vol-2243/paper13.pdf
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