implied by the $\forall y\in\\{0,1\\}^{m}$ part of the problem. Finally, $r$
is defined as follows:

$\displaystyle r$ $\displaystyle=$ $\displaystyle r_{u}\ /\ r_{w}\ /\
\mathbf{N}[0,\\_]\ /\ (\neg<2\cdot M)$

We now prove that $(v,M,v,2\cdot M)\in\llbracket r\rrbracket_{C}$ if and only
if $\exists x\in\\{0,1\\}^{n}\ \forall y\in\\{0,1\\}^{m}\ x\cdot u+y\cdot
w\neq S$.

Assume that both $t$ and $t^{\prime}$ are in $\Omega$. By induction on the
definition of numerical occurrence indicators, it is easy to see that
$(v,t,v,t^{\prime})\in\llbracket\mathbf{N}[k,k]\rrbracket_{C}$ if and only if
$t^{\prime}=t+k$. Hence, by definition of $r_{u_{i}}$, we have that
$(v,t,v,t^{\prime})\in\llbracket r_{u_{i}}\rrbracket_{C}$ if and only if
$t^{\prime}=t$ (0 occurrences) or $t^{\prime}=t+u_{i}$ (1 occurrence), or what
is equivalent, if there exists $x_{i}\in\\{0,1\\}$ such that
$t^{\prime}=t+x_{i}\cdot u_{i}$. In fact, it can be proved by induction that
$(v,t,v,t^{\prime})\in\llbracket r_{u}\rrbracket_{C}$ if and only if $\exists
x\in\\{0,1\\}^{n}$ such that $t^{\prime}=t+x\cdot u$. We will demonstrate
something stronger, which is that $(v,t,v,t^{\prime})\in\llbracket r_{u_{1}}\
/\ \dots\ /r_{u_{i}}\rrbracket_{C}$ if and only if there exists
$(x_{1},\dots,x_{i})\in\\{0,1\\}^{i}$ such that
$t^{\prime}=t+\sum_{k=1}^{i}x_{i}\cdot u_{i}$.

Our base case will be checking the property for $r_{u_{1}}$, which, by the
same exact reasoning as above, satisfies that $(v,t,v,t^{\prime})\in\llbracket
r_{u_{1}}\rrbracket_{C}$ if and only if there exists $x_{1}\in\\{0,1\\}$ such
that $t^{\prime}=t+x_{1}\cdot u_{1}$. Suppose now that
$(v,t,v,t^{\prime})\in\llbracket r_{u_{1}}\ /\ \dots\
/r_{u_{i}}\rrbracket_{C}$ if and only if there exists
$(x_{1},\dots,x_{i})\in\\{0,1\\}^{i}$ such that
$t^{\prime}=t+\sum_{k=1}^{i}x_{i}\cdot u_{i}$. We also know by the previous
reasoning that $(v,t^{\prime},v,t^{\prime\prime})\in\llbracket
r_{u_{i+1}}\rrbracket_{C}$ if and only if there exists $x_{i+1}\in\\{0,1\\}$
such that $t^{\prime\prime}=t^{\prime}+x_{i+1}\cdot u_{i+1}$. Hence, by
definition of $(r_{1}/r_{2})$, we get that
$(v,t,v,t^{\prime\prime})\in\llbracket r_{u_{1}}\ /\ \dots\
/r_{u_{i+1}}\rrbracket_{C}$ if and only if there exists $(v,t^{\prime})$ such
that there exists $(x_{1},\dots,x_{i})\in\\{0,1\\}^{i}$ such that
$t^{\prime}=t+\sum_{k=1}^{i}x_{i}\cdot u_{i}$ and there exists
$x_{i+1}\in\\{0,1\\}$ such that $t^{\prime\prime}=t^{\prime}+x_{i+1}\cdot
u_{i+1}$, i.e., if and only if there exists
$(x_{1},\dots,x_{i+1})\in\\{0,1\\}^{i+1}$ such that
$t^{\prime\prime}=t+\sum_{k=1}^{i+1}x_{i}\cdot u_{i}$. This yields the result.

Moreover, by definition of $\llbracket(r_{1}/r_{2})\rrbracket_{C}$, we get
that $(v,M,v,2\cdot M)\in\llbracket r\rrbracket_{C}$ if and only if there
exists $x\in\\{0,1\\}^{n}$ such that:

$(v,M+x\cdot u,v,2\cdot M)\in\llbracket r_{v}\ /\ \mathbf{N}[0,\\_]\ /\
(\neg<2\cdot M)\rrbracket_{C}$

Notice also that the right part of this formula is built in the following way:
$(\neg<2\cdot M)$ is a test that is only satisfied by $(v,2\cdot M,v,2\cdot
M)$, whereas $\mathbf{N}[0,\\_]$ is satisfied by any tuple
$(v,t,v,t^{\prime})$ such that $t\leq t^{\prime}$. Hence,
$(v,t,v^{\prime},t^{\prime})\in\llbracket\mathbf{N}[0,\\_]\ /\ (\neg<2\cdot
M)\rrbracket_{C}$ if and only if $t$ is any time point in $\Omega$ and
$t^{\prime}=2\cdot M$. Thus, all we need to prove now is that there exists
some time point $t$ such that $(v,M+x\cdot u,v,t)\in\llbracket
r_{v}\rrbracket_{C}$ if and only if $\forall y\in\\{0,1\\}^{m}\ x\cdot
u+y\cdot w\neq S$.

First, we show by induction that if $(v,t,v,t^{\prime})\in\llbracket
r_{j}\rrbracket_{C}$, then $t=t^{\prime}$. The base case is trivial, since
$r_{0}$ is a test. For the inductive case, assume that if
$(v,t,v,t^{\prime})\in\llbracket r_{j}\rrbracket_{C}$, then $t^{\prime}=t$.
For conciseness, define $a:=w_{j+1}$. In the case of $j+1$, we know that if
$(v,t_{1},v,t_{2})\in\llbracket\mathbf{N}[a,a]\ /\ r_{j}\ /\
\mathbf{P}[2a,2a]\rrbracket_{C}$, then there exist time points $t_{3}$ and
$t_{4}$ such that
$(v,t_{1},v,t_{3})\in\llbracket\mathbf{N}[a,a]\rrbracket_{C}$,
$(v,t_{3},v,t_{4})\in\llbracket r_{j}\rrbracket_{C}$ and
$(v,t_{4},v,t_{2})\in\llbracket\mathbf{P}[2a,2a]\rrbracket_{C}$. Notice then
that these conditions only hold respectively if $t_{3}=t_{1}+a$, by definition
of operator $\mathbf{N}$ and numerical occurrence indicators, $t_{3}=t_{4}$ by
induction hypothesis and $t_{2}=t_{4}-2a$. Thus,
$t_{2}=t4-2a=t_{3}-2a=t_{1}-a$. It is clear that if
$(v,t_{1},v,t_{5})\in\llbracket(\mathbf{N}[a,a]\ /\ r_{k}\ /\
\mathbf{P}[2a,2a])[2,2]\rrbracket_{C}$, then $t_{5}=t_{1}-2a$. Finally, if
$(v,t_{5},v,t^{\prime})\in\llbracket\mathbf{N}[2a,2a]\rrbracket_{C}$, then
$t^{\prime}=t_{5}+2a$, so by definition of
$\llbracket(r_{1}/r_{2})\rrbracket_{C}$, we conclude that if
$(v,t,v,t^{\prime})\in\llbracket r_{j+1}\rrbracket_{C}$, then $t^{\prime}=t$.

Given the conclusion in the previous paragraph, all we need to prove now is
that $(v,M+x\cdot u,v,M+x\cdot u)\in\llbracket r_{v}\rrbracket_{C}$ if and
only if $\forall y\in\\{0,1\\}^{m}\ x\cdot u+y\cdot w\neq S$. In fact, we will
prove by induction a stronger condition:

$\text{for every }k\in\\{0,\dots,m\\},\text{it holds that }\forall
y\in\\{0,1\\}^{k}\ t+\sum_{j=1}^{k}y_{j}\cdot w_{j}\neq S\text{ if and only if
}(v,M+t,v,M+t)\in\llbracket r_{k}\rrbracket_{C}$

The case when $t=x\cdot u$ and $k=m$ yields $\Sigma_{2}^{p}$-hardness of
Eval(ITPG, NavL[NOI]) as a result. In the base case $k=0$, we need to prove
that $t\neq S$ if and only if $(v,M+t,v,M+t)\in\llbracket
r_{0}\rrbracket_{C}$. Recall that $r_{0}=r_{t\neq S+M}$. It can be easily
checked that $(v,t)\models r_{0}$ if and only if $t\neq S+M$. Also, $r_{0}$ is
a test, so $(v,t,v,t^{\prime})\in\llbracket r_{0}\rrbracket_{C}$ if and only
if $t=t^{\prime}$ and $t\neq S+M$. Hence, we have that
$(v,M+t,v,M+t)\in\llbracket r_{0}\rrbracket_{C}$ if and only if $M+t=M+t$
(which is trivially satisfied) and $M+t\neq M+S$, i.e., if and only if $t\neq
S$. For the inductive case, assume that for $k\in\\{0,\dots,m\\}$, it holds
that:

$\forall y\in\\{0,1\\}^{k}\ t+\sum_{j=1}^{k}y_{j}\cdot w_{j}\neq S\text{ if
and only if }(v,M+t,v,M+t)\in\llbracket r_{k}\rrbracket_{C}.$

Then we have to prove that:

$\forall y\in\\{0,1\\}^{k+1}\ t+\sum_{j=1}^{k+1}y_{j}\cdot w_{j}\neq S\text{
if and only if }(v,M+t,v,M+t)\in\llbracket r_{k+1}\rrbracket_{C}$

To prove this, define again $a:=w_{k+1}$ for conciseness. Recall that
$r_{k+1}=((\mathbf{N}[a,a]\ /\ r_{k}\ /\
\mathbf{P}[2a,2a])[2,2]/\mathbf{N}[2a,2a])$. Notice then that
$(v,M+t,v,t^{\prime})\in\llbracket\mathbf{N}[a,a]\ /\ r_{k}\ /\
\mathbf{P}[2a,2a]\rrbracket_{C}$ if and only if there exist time points
$t_{1}$ and $t_{2}$ such that
$(v,M+t,v,t_{1})\in\llbracket\mathbf{N}[a,a]\rrbracket_{C}$,
$(v,t_{1},v,t_{2})\in\llbracket r_{k}\rrbracket_{C}$ and
$(v,t_{2},v,t^{\prime})\in\llbracket\mathbf{P}[2a,2a]\rrbracket_{C}$. The
first condition is equivalent to having that $t_{1}=M+t+a$. The second
condition implies that $t_{1}=t_{2}$, given what we proved in the previous
paragraphs. Hence, given that $(v,M+t+a,v,M+t+a)\in\llbracket
r_{k}\rrbracket_{C}$, we conclude by induction hypothesis that $\forall
y\in\\{0,1\\}^{k}\ t+a+\sum_{j=1}^{k}y_{j}\cdot w_{j}\neq S$. The third
condition is equivalent to having that $t^{\prime}=t_{2}-2a$. Altogether, this
means that $(v,M+t,v,t^{\prime})\in\llbracket\mathbf{N}[a,a]\ /\ r_{k}\ /\
\mathbf{P}[2a,2a]\rrbracket_{C}$ if and only if $t^{\prime}=M+t-a$ and
$\forall y\in\\{0,1\\}^{k}$, it holds that $t+a+\sum_{j=1}^{k}y_{j}\cdot
w_{j}\neq S$. Now, this means that
$(v,M+t,v,t^{\prime})\in\llbracket(\mathbf{N}[a,a]\ /\ r_{k}\ /\
\mathbf{P}[2a,2a])[2,2]\rrbracket_{C}$ if there exists a time point
$t^{\prime\prime}$ such that $t^{\prime\prime}=M+t-a$,
$t^{\prime}=M+(t-a)-a=M+t-2a$, $\forall y\in\\{0,1\\}^{k}$, it holds that
$t+a+\sum_{j=1}^{k}y_{j}\cdot w_{j}\neq S$, and $\forall y\in\\{0,1\\}^{k}$,
it holds that $(t-a)+a+\sum_{j=1}^{k}y_{j}\cdot w_{j}\neq S$. Therefore,
$(v,M+t,v,t^{\prime})\in\llbracket(\mathbf{N}[a,a]\ /\ r_{k}\ /\
\mathbf{P}[2a,2a])[2,2]\rrbracket_{C}$ if and only if $t^{\prime}=M+t-2a$ and
for every $y\in\\{0,1\\}^{k+1}$, it holds that $t+\sum_{j=1}^{k+1}y_{j}\cdot
w_{j}\neq S$. Given that for $t_{1},t_{2}\in\Omega$, it holds that
$(v,t_{1},v,t_{2})\in\llbracket\mathbf{N}[2a,2a]\rrbracket_{C}$ if and only if
$t_{2}=t_{1}+2a$, we conclude that
$(v,M+t,v,t^{\prime})\in\llbracket(\mathbf{N}[a,a]\ /\ r_{k}\ /\
\mathbf{P}[2a,2a])[2,2]\ /\ \mathbf{N}[2a,2a]\rrbracket_{C}$ if and only if
$t^{\prime}=M+t$ and $\forall y\in\\{0,1\\}^{k+1}\
t+\sum_{j=1}^{k+1}y_{j}\cdot w_{j}\neq S$. Finally, this gives us the result
we are trying to prove, that is, $(v,M+t,v,M+t)\in\llbracket(\mathbf{N}[a,a]\
/\ r_{k}\ /\ \mathbf{P}[2a,2a])[2,2]\ /\ \mathbf{N}[2a,2a]\rrbracket_{C}$ if
and only if $\forall y\in\\{0,1\\}^{k+1}\ t+\sum_{j=1}^{k+1}y_{j}\cdot
w_{j}\neq S$.

To conclude the proof of the theorem, notice that $r$ can be constructed in
polynomial time with respect to the sizes of $u$, $v$ and $S$, so the entire
reduction can be computed in polynomial time.

###  C-D Eval(ITPG, NavL[PC,NOI]) is Pspace-complete

Consider the following well-known decision problem called True Quantified
Boolean Formula (TQBF), which is well known to be Pspace-complete
[StockmeyerMeyer1973]:

Problem: TQBF Input: A quantified Boolean formula $\psi=Q_{1}x_{1}\dots
Q_{n}x_{n}\,\varphi(x_{1},\dots,x_{n})$ in prenex normal form where
$\varphi(x_{1},\dots,x_{n})$ is a Boolean formula on variables
$x_{1},\dots,x_{n}$, and $Q_{1},\dots,Q_{n}$ are quantifiers ($\forall$ or
$\exists$). Output: true if $\psi$ is valid, and false otherwise.

Without loss of generality, $\varphi$ can be assumed to be in conjunctive
normal form. We will show that TQBF can be reduced to our problem Eval(ITPG,
NavL[PC,NOI]) by proceeding in three steps. Let $\psi=Q_{1}x_{1}\dots
Q_{n}x_{n}\,\varphi(x_{1},\dots,x_{n})$. First, we will show that a predicate
$\textsf{bit}(i,t)$ (defined below) can be written in our language. Then, by
using that predicate, we will show that $\varphi$ can be encoded in our
language. Finally, we will show that an expression representing the
quantifiers of $\psi$ can be added to the expression encoding $\varphi$, which
yields the result.

We start with a QBF formula $\psi$ as described above to build an input for
the problem Eval(ITPG, NavL[PC,NOI]). More precisely, the input ITPG will be
$C=\left(\Omega,N,E,\rho,\lambda,\xi,\sigma\right)$ where
$\Omega=[0,2^{n}-1]$, $N=\\{v\\}$, $E=\varnothing$, $\rho$ is an empty
function, $\lambda(v)=l$, $\xi(v)=\left\\{[0,2^{n}-1]\right\\}$ and $\sigma$
is an empty function. In other words, $C$ is an ITPG consisting of only one
node existing from time $0$ to time $2^{n}-1$, with no edges or properties.
Moreover, we will build an expression $r$ such that $(v,0,v,0)\in\llbracket
r\rrbracket_{C}$ if and only if $\psi$ is valid, which concludes the
reduction. The steps to construct $r$ are shown next.

Step 1: Expressing the predicate bit with an expression in ${\rm{\sf{\small
NavL}}}{\rm[}{\rm{\sf{\small PC}}},{\rm{\sf{\small NOI}}}{\rm]}$. Consider
predicate $\textsf{bit}(i,t)$ that tests whether the $i$-th bit of time $t$
(from right to left when written in its binary representation) is 1. For
instance, $\textsf{bit}(1,0)$ is false, and $\textsf{bit}(5,30)$ is true,
since the first bit of $0$ is $0$, whereas $30$ is $11110$ in binary, and its
fifth bit is $1$. Now, consider the following expression:

$\displaystyle r_{i}$ $\displaystyle=$
$\displaystyle?\left(\mathbf{P}\left[2^{i},2^{i}\right]\left[0,\\_\right]\ /\
\left(<2^{i}\wedge\neg<2^{i-1}\right)\right)$

Notice that $r_{i}$ is a test. Thus, for a pair of temporal objects
$(o_{1},t_{1},o_{2},t_{2})$ to satisfy $r_{i}$, $(o_{1},t_{1})$ must be equal
to $(o_{2},t_{2})$. The expression to satisfy is a path test, so there must be
some temporal object $(o_{3},t_{3})$, such that
$(o_{1},t_{1},o_{3},t_{3})\in\llbracket\mathbf{P}\left[2^{i},2^{i}\right]\left[0,\\_\right]\
/\left(<2^{i}\wedge\neg<2^{i-1}\right)\rrbracket_{C}$. Since the right part is
a test as well, we can split the expression into two parts. Firstly, we must
have that
$(o_{1},t_{1},o_{3},t_{3})\in\llbracket\mathbf{P}\left[2^{i},2^{i}\right]\left[0,\\_\right]\rrbracket_{C}$,
which implies that $t_{3}=t_{1}-k*2^{i}$ for some integer $k\geq 0$. Secondly,
we must have that $(o_{3},t_{3})\models\left(<2^{i}\wedge\neg<2^{i-1}\right)$,
which implies that $2^{i-1}\leq t_{3}<2^{i}$. This means that by writing
$t_{3}$ in its binary form, we get $1$ as its $i$-th bit. Together, these two
conditions imply that $t_{1}$ also has $1$ as its $i$-th bit, when written in
its binary form. In consequence, we get that

$\displaystyle(o,t,o,t)\in\llbracket r_{i}\rrbracket_{C}\text{ if and only if
}\textsf{bit}(i,t)\text{ is }\textit{true}$

Besides, we trivially get that:

$\displaystyle(o,t,o,t)\in\llbracket\neg r_{i}\rrbracket_{C}\text{ if and only
if }\textsf{bit}(i,t)\text{ is }\textit{false}$

Finally, notice that both $r_{i}$ and $\neg r_{i}$ have linear length with
respect to $i$, which will be important later.

Step 2: Expressing any CNF formula in ${\rm{\sf{\small
NavL}}}{\rm[}{\rm{\sf{\small PC}}},{\rm{\sf{\small NOI}}}{\rm]}$. Assume that

$\displaystyle\varphi(x_{1},\dots,x_{n})$ $\displaystyle=$
$\displaystyle\bigwedge_{j=1}^{m}\bigvee_{k=1}^{m_{j}}l_{j,k}$

where for every $j$ and $k$, $l_{j,k}$ is a literal, i.e., either a variable
in $\\{x_{1},\dots,x_{n}\\}$ or its negation. Then, for every
$j\in\\{1,\dots,m\\}$ and $k\in\\{1,\dots,m_{j}\\}$, we define:

$\displaystyle L_{j,k}$ $\displaystyle=$
$\displaystyle\begin{cases}r_{i}&\text{if }l_{j,k}=x_{i}\\\ \neg
r_{i}&\text{if }l_{j,k}=\neg x_{i}\end{cases}$

We can use these expressions to build a regular expression that tests the
satisfiability of our formula $\varphi(x_{1},\dots,x_{n})$ by any valuation
$\sigma:\left\\{x_{1},\dots,x_{n}\right\\}\rightarrow\left\\{\textit{false},\textit{true}\right\\}$.
To do this, we will use a time value $t\in\left[0,2^{n}-1\right]$ to represent
a valuation $\sigma_{t}$, where $\sigma_{t}(x_{i})=\textit{true}$ if and only
if the $i$-th bit of $t$ is $1$. We can do so by employing the expressions
$L_{i,k}$ on tests along with conjunctions ($\wedge$) and disjunctions
($\vee$), which are also present in ${\rm{\sf{\small
NavL}}}{\rm[}{\rm{\sf{\small PC}}},{\rm{\sf{\small NOI}}}{\rm]}$:

$\displaystyle r_{\varphi(x_{1},\dots,x_{n})}$ $\displaystyle=$
$\displaystyle\bigwedge_{j=1}^{m}\bigvee_{k=1}^{m_{j}}L_{j,k}$

Here again, $r_{\varphi(x_{1},\dots,x_{n})}$ is a test, so if it is satisfied
by $(o_{1},t_{1},o_{2},t_{2})$, then $(o_{1},t_{1})=(o_{2},t_{2})$
Furthermore, we show that, because of how the expressions $L_{j,k}$ are
defined, we have:

$\displaystyle(o,t,o,t)\in\llbracket
r_{\varphi(x_{1},\dots,x_{n})}\rrbracket_{C}\text{ if and only if
}\sigma_{t}\left(\varphi(x_{1},\dots,x_{n})\right)=\textit{true}$

To show the previous assertion, first assume that $(o,t,o,t)\in\llbracket
r_{\varphi(x_{1},\dots,x_{n})}\rrbracket_{C}$. Because of how the expression
is defined, for each $j\in\\{1,\dots,m\\}$ we must have that
$(o,t,o,t)\in\llbracket\bigvee_{k=1}^{m_{j}}L_{j,k}\rrbracket_{C}$. Hence, for
any arbitrary $j\in\\{1,\dots,m\\}$, we immediately get that there must exist
$k\in\\{1,\dots,m_{j}\\}$ such that $(o,t,o,t)\in\llbracket
L_{j,k}\rrbracket_{C}$. If $l_{j,k}=x_{i}$, then we must also have that
$(o,t,o,t)\in\llbracket r_{i}\rrbracket_{C}$, which, as we already showed, is
equivalent to having that $\textsf{bit}(i,t)$ is true, which in turn is
equivalent to $\sigma_{t}(x_{i})=\textit{true}$. Otherwise, if $l_{j,k}=\neg
x_{i}$, then we must have that $(o,t,o,t)\in\llbracket\neg
r_{i}\rrbracket_{C}$, which, as we also showed, is equivalent to having that
$\textsf{bit}(i,t)$ is false, which in turn is equivalent to
$\sigma_{t}(x_{i})=\textit{false}$. In both cases, we get that
${\sigma}_{t}(l_{j,k})=\textit{true}$, which means that
${\sigma}_{t}\left(\bigvee_{k=1}^{m_{j}}l_{j,k}\right)=\textit{true}$. Since
this holds for an arbitrary value $j$, it holds for the entire conjunction.
Hence, ${\sigma}_{t}\left(\varphi(x_{1},\dots,x_{n})\right)=\textit{true}$.

Now, to show that the inverse is also true, assume that there is some
$t\in\Omega$ such that
${\sigma}_{t}\left(\varphi(x_{1},\dots,x_{n})\right)=\textit{true}$. By
definition, this means that for every $j\in\\{1,\dots,m\\}$,
${\sigma}_{t}\left(\bigvee_{k=1}^{m_{j}}l_{j,k}\right)=\textit{true}$. In
turn, this means that for every $j$ there is some $k\in\\{1,\dots,m_{j}\\}$
such that ${\sigma}_{t}(l_{j,k})=\textit{true}$. As we saw earlier, this
condition is equivalent to having that $(o,t,o,t)\in\llbracket
L_{j,k}\rrbracket_{C}$, hence, for every $j\in\\{1,\dots,m\\}$, we also have
that $(o,t,o,t)\in\llbracket\bigvee_{k=1}^{m_{j}}L_{j,k}\rrbracket_{C}$. Given
that this is true for every $j$, by definition, it is also true for the
conjunction of them. Hence, we get that $(o,t,o,t)\in\llbracket
r_{\varphi(x_{1},\dots,x_{n})}\rrbracket_{C}$. This concludes the proof in
Step 2.

Observation: Notice that the previous results already implies NP-hardness and
coNP-hardness for the problem. Since every valuation
$\sigma:\\{x_{1},\dots,x_{n}\\}\rightarrow\\{\textit{false},\textit{true}\\}$
has a corresponding time point $t$ such that $\sigma=\sigma_{t}$, and a
Boolean CNF formula $\varphi(x_{1},\dots,x_{n})$ on $n$ variables
$x_{1},\dots,x_{n}$ is satisfiable if and only if there exists a valuation
$\sigma$ such that
${\sigma}\left(\varphi(x_{1},\dots,x_{n})\right)=\textit{true}$, it is also
true that $\varphi(x_{1},\dots,x_{n})$ is satisfiable if and only if
$(v,0,v,0)\in\llbracket?(\mathbf{N}[0,\\_]\ /\
r_{\varphi(x_{1},\dots,x_{n})})\rrbracket_{C}$ (that is, advance in time to an
arbitrary time point $t$ and check the condition that implies that
${\sigma}_{t}\left(\varphi(x_{1},\dots,x_{n})\right)=\textit{true}$ for the
temporal object $(v,t)$). Similarly, $\varphi(x_{1},\dots,x_{n})$ is a
tautology if and only if $(v,0,v,0)\in\llbracket\neg?(\mathbf{N}[0,\\_]\ /\
\neg r_{\varphi(x_{1},\dots,x_{n})})\rrbracket_{C}$ (there is no path to a
time point $t$ such that
${\sigma}_{t}\left(\varphi(x_{1},\dots,x_{n})\right)=\textit{false}$, hence
there is no valuation that makes $\varphi$ to be false). In what follows, we
show Pspace-hardness of the problem.

Step 3: Expressing satisfiability of quantified Boolean formulae with an
expression in NavL[PC,NOI]. Consider a quantified Boolean formula in prenex
normal form

$Q_{1}x_{1}\dots Q_{n}x_{n}\ \varphi(x_{1},\dots,x_{n})$

Since we already have a way to express $\varphi(x_{1},\dots,x_{n})$, we only
need to express the possible valuations (i.e., time points) generated by the
sequence of quantifiers $Q_{1},\dots,Q_{n}$.

First, assume $Q_{i}$ is the existential quantifier ($\exists$). This means
that we can either make $x_{i}$ take valuation true or false to satisfy our
formula. Considering time points, this is equivalent to have either $1$ or $0$
at the $i$-th bit of the time $t$ at which we are standing. The intuition is
that this can easily be expressed by starting at time $0$, and then deciding
whether to move into a future time point with the expression
$(\mathbf{N}[2^{i-1},2^{i-1}]+\mathbf{N}[0,0])$ to set the $i$-th bit of the
time point. Notice that if there are only expressions of the form
$\mathbf{N}[2^{i-1},2^{i-1}]$, and they are only mentioned once (at least, as
prefixes of our test expressions) for each $i$, they will not affect other
bits of $t$. Hence, if $s_{i+1}$ represents the part of the subformula
$Q_{i+1}x_{i+1}\dots Q_{n}x_{n}\ \varphi(x_{1},\dots,x_{n})$, then the
subformula $\exists x_{i}\ Q_{i+1}x_{i+1}\dots Q_{n}x_{n}\
\varphi(x_{1},\dots,x_{n})$ can be represented by first navigating through
time, only affecting the first $i-1$ bits, and then testing that the reached
temporal object satisfies the following test:

$\displaystyle s_{i}$ $\displaystyle=$
$\displaystyle?\left(\left(\mathbf{N}[2^{i-1},2^{i-1}]+\mathbf{N}[0,0]\right)\
/\ s_{i+1}\right).$

In turn, if $Q_{i}$ is the universal quantifier ($\forall$), we will employ
the fact that $\forall x\,\psi(x)$ is equivalent to $\neg\exists
x\,\neg\psi(x)$ for every formula $\psi(x)$ with free variable $x$. Hence, if
$s_{i+1}$ represents the part of the subformula $Q_{i+1}x_{i+1}\dots
Q_{n}x_{n}\ \varphi(x_{1},\dots,x_{n})$, then the subformula $\forall x_{i}\
Q_{i+1}x_{i+1}\dots Q_{n}x_{n}$ $\varphi(x_{1},\dots,x_{n})$ can be
represented by first only navigating through time, only affecting the first
$i-1$ bits, and then testing whether the reached temporal object satisfies the
following test:

$\displaystyle s_{i}$ $\displaystyle=$
$\displaystyle\neg\left(?\left((\mathbf{N}[2^{i-1},2^{i-1}]+\mathbf{N}[0,0])\
/\ \left(\neg s_{i+1}\right)\right)\right).$

Finally, define $s_{n+1}=r_{\varphi(x_{1},\dots,x_{n})}$. We claim that, for
$i\in\\{n+1,n,\dots,1\\}$ (i.e., $0$ to $n$ quantifiers), if $t<2^{i-1}$,
then:

$(v,t,v,t)\in\llbracket s_{i}\rrbracket_{C}\ \text{if and only if}\
Q_{i}x_{i}\dots Q_{n}x_{n}\
\varphi(\sigma_{t}(x_{1}),\dots,\sigma_{t}(x_{i-1}),x_{i},\dots,x_{n})\
\text{is valid}.$

In particular, for $n$ quantifiers, i.e., when $i=1$, this result gives us
Pspace-hardness for Eval(ITPG, NavL[PC,NOI]), since we will have that $\psi$
is true if and only if $(v,0,v,0)\in\llbracket s_{1}\rrbracket_{C}$, where $C$
and $s_{1}$ can be constructed in polynomial time in the size of $\psi$. We
will prove this claim by induction over the number of quantifiers preceding
$\varphi(x_{1},\dots,x_{n})$.

The base case consists of the formula with no quantified variables, i.e., when
$i=n+1$. We must show that if $t<2^{n}$, then $(v,t,v,t)\in\llbracket
r_{\varphi(x_{1},\dots,x_{n})}\rrbracket_{C}$ if and only if
$\varphi(\sigma(x_{1}),\dots,\sigma(x_{n}))$ is true. Notice that
$\varphi(\sigma(x_{1}),\dots,\sigma(x_{n}))$ is true is equivalent to having
that ${\sigma}_{t}(\varphi(x_{1},\dots,x_{n}))$ is true. Hence, by step 2,
this is equivalent to having that $(v,t,v,t)\in\llbracket
r_{\varphi(x_{1},\dots,x_{n})}\rrbracket_{C}$.

For the inductive case, assume that the claim holds for $k$ quantifiers, for
some $k$ such that $0\leq k\leq n$. This means that for $i=n-k+1$, if
$t<2^{i-1}$, then the following condition holds:

$(v,t,v,t)\in\llbracket s_{i}\rrbracket_{C}\ \text{if and only if}\
Q_{i}x_{i}\dots Q_{n}x_{n}\
\varphi(\sigma_{t}(x_{1}),\dots,\sigma_{t}(x_{i-1}),x_{i},\dots,x_{n})\
\text{is valid}$

We then have to prove that the condition holds for $k+1$ quantifiers, i.e.,
for $i-1=n-k$. That is, if $t^{\prime}<2^{i-2}$, then we have to show that:

$\displaystyle(v,t^{\prime},v,t^{\prime})\in\llbracket s_{i-1}\rrbracket_{C}\
\text{if and only if}\ Q_{i-1}x_{i-1}\dots Q_{n}x_{n}\
\varphi(\sigma_{t^{\prime}}(x_{1}),\dots,\sigma_{t^{\prime}}(x_{i-2}),x_{i-1},\dots,x_{n})\
\text{is valid}$ (7)

Let $t^{\prime}<2^{i-2}$, and consider the following cases.

  * •

If $Q_{i-1}=\exists$, recall that

$\displaystyle s_{i-1}$ $\displaystyle=$
$\displaystyle?\left(\left(\mathbf{N}[2^{i-2},2^{i-2}]+\mathbf{N}[0,0]\right)\
/\ s_{i}\right).$

Notice then that by definition of $s_{i-1}$, we have that
$(v,t^{\prime},v,t^{\prime})\in\llbracket s_{i-1}\rrbracket_{C}$ if and only
if there exists $t_{1}\in\Omega$ such that
$(v,t^{\prime},v,t_{1})\in\llbracket\left(\mathbf{N}[2^{i-2},2^{i-2}]+\mathbf{N}[0,0]\right)\
/\ s_{i}\rrbracket_{C}$. By definition of $s_{i}$, the previous condition
holds if and only if
$(v,t^{\prime},v,t_{1})\in\llbracket\left(\mathbf{N}[2^{i-2},2^{i-2}]+\mathbf{N}[0,0]\right)\rrbracket_{C}$
and $(v,t_{1},v,t_{1})\in\llbracket s_{i}\rrbracket_{C}$. Now, this means that
$(v,t^{\prime},v,t^{\prime})\in\llbracket s_{i-1}\rrbracket_{C}$ if and only
if there exists $t_{1}\in\\{t^{\prime},t^{\prime}+2^{i-2}\\}$ satisfying that
$(v,t_{1},v,t_{1})\in\llbracket s_{i}\rrbracket_{C}$.

To prove the direction $(\Rightarrow)$ of (7) assume that
$(v,t^{\prime},v,t^{\prime})\in\llbracket s_{i-1}\rrbracket_{C}$, which
implies that there exists $t_{1}\in\\{t^{\prime},t^{\prime}+2^{i-2}\\}$
satisfying that $(v,t_{1},v,t_{1})\in\llbracket s_{i}\rrbracket_{C}$. Given
that $t^{\prime}$ is an integer with $i-2$ bits, $t_{1}$ comes from either
putting $1$ or $0$ as the $(i-1)$-th bit of $t^{\prime}$, which means that
$t_{1}<2^{i-1}$ must hold. By induction hypothesis, this implies that
$Q_{i}x_{i}\dots
Q_{n}x_{n}\varphi(\sigma_{t_{1}}(x_{1}),\dots,\sigma_{t_{1}}(x_{i-1}),x_{i},\dots,x_{n})$
is valid. Since $t_{1}$ and $t^{\prime}$ share the same first $i-2$ bits, we
get that $\sigma_{t^{\prime}}(x_{j})=\sigma_{t_{1}}(x_{j})$ for
$j\in\\{1,...,i-2\\}$. Therefore, we conclude that $\exists
x_{i-1}Q_{i}x_{i}\dots
Q_{n}x_{n}\varphi(\sigma_{t^{\prime}}(x_{1}),\dots,\sigma_{t^{\prime}}(x_{i-2}),x_{i-1},\dots,x_{n})$
is valid.

To prove the direction $(\Leftarrow)$ of (7) suppose that $\exists
x_{i-1}Q_{i}x_{i}\dots
Q_{n}x_{n}\varphi(\sigma_{t^{\prime}}(x_{1}),\dots,\sigma_{t^{\prime}}(x_{i-2}),x_{i-1},\dots,x_{n})$
is valid. Then we know that $Q_{i}x_{i}\dots
Q_{n}x_{n}\varphi(\sigma_{t^{\prime}}(x_{1}),\dots,\sigma_{t^{\prime}}(x_{i-2}),b,x_{i},\dots,x_{n})$
is valid for some value $b\in\\{\textit{true},\textit{false}\\}$. Define
$\mathbbm{1}_{b}$ as $1$ if $b=\textit{true}$, and as $0$ otherwise. Notice
then that by taking $t_{1}=t^{\prime}+2^{i-2}\cdot\mathbbm{1}_{b}$, we get
that $\sigma_{t_{1}}(x_{i-1})=b$. Moreover,
$\sigma_{t_{1}}(x_{j})=\sigma_{t^{\prime}}(x_{j})$ for every
$j\in\\{1,\dots,i-2\\}$ since $t^{\prime}<2^{i-2}$ and $t_{1}$ shares all its
first $i-2$ bits with $t^{\prime}$. In consequence, this gives us that
$Q_{i}x_{i}\dots
Q_{n}x_{n}\varphi(\sigma_{t_{1}}(x_{1}),\dots,\sigma_{t_{1}}(x_{i-1}),x_{i},\dots,x_{n})$
is valid. By induction, this means that $(v,t_{1},v,t_{1})\in\llbracket
s_{i}\rrbracket_{C}$. Since $t_{1}=t^{\prime}+2^{i-2}\cdot\mathbbm{1}_{b}$, we
have that either $t_{1}=t^{\prime}$ or $t_{1}=t^{\prime}+2^{i-2}$. In any
case, we get that
$(v,t^{\prime},v,t_{1})\in\llbracket\mathbf{N}[2^{i-2},2^{i-2}]+\mathbf{N}[0,0]\rrbracket_{C}$,
so we have that
$(v,t,v,t_{1})\in\llbracket(\mathbf{N}[2^{i-2},2^{i-2}]+\mathbf{N}[0,0])\ /\
s_{i}\rrbracket_{C}$. By definition of $s_{i-1}$, we conclude that
$(v,t^{\prime},v,t^{\prime})\in\llbracket s_{i-1}\rrbracket_{C}$, which was to
be shown.

  * •

If $Q_{i-1}=\forall$, recall that

$\displaystyle s_{i-1}$ $\displaystyle=$
$\displaystyle\neg?\left(\left(\mathbf{N}[2^{i-2},2^{i-2}]+\mathbf{N}[0,0]\right)\
/\ \left(\neg s_{i}\right)\right).$

Now, by definition of $s_{i-1}$, we have that
$(v,t^{\prime},v,t^{\prime})\in\llbracket s_{i-1}\rrbracket_{C}$ if and only
if

$\displaystyle(v,t^{\prime})$ $\displaystyle\not\models$
$\displaystyle?\left(\left(\mathbf{N}[2^{i-2},2^{i-2}]+\mathbf{N}[0,0]\right)\
/\ \left(\neg s_{i}\right)\right).$

This, in turn, is equivalent to the fact that there is no time point
$t_{1}\in\Omega$ such that
$(v,t^{\prime},v,t_{1})\in\llbracket\left(\mathbf{N}[2^{i-2},2^{i-2}]+\mathbf{N}[0,0]\right)\
/\ \left(\neg s_{i}\right)\rrbracket_{C}$. Hence, we know that
$(v,t^{\prime},v,t^{\prime})\in\llbracket s_{i-1}\rrbracket_{C}$ if and only
if, for every time point $t_{1}\in\Omega$:

$(v,t^{\prime},v,t_{1})\notin\llbracket\left(\mathbf{N}[2^{i-2},2^{i-2}]+\mathbf{N}[0,0]\right)\
/\ \left(\neg s_{i}\right)\rrbracket_{C}.$

This condition means that each $t_{1}$ satisfies
$(v,t^{\prime},v,t_{1})\notin\llbracket\left(\mathbf{N}[2^{i-2},2^{i-2}]+\mathbf{N}[0,0]\right)\rrbracket_{C}$
or $(v,t_{1})\not\models\left(\neg s_{i}\right)$. This, in turn, is equivalent
to saying that if $t_{1}\in\\{t^{\prime},t^{\prime}+2^{i-2}\\}$ then
$(v,t_{1})\not\models\left(\neg s_{i}\right)$, i.e., $(v,t_{1})\models s_{i}$.
As a consequence, $(v,t^{\prime},v,t^{\prime})\in\llbracket
s_{i-1}\rrbracket_{C}$ if and only if $(v,t^{\prime})\models s_{i}$ and
$(v,t^{\prime}+2^{i-2})\models s_{i}$, which is equivalent to having that
$(v,t^{\prime},v,t^{\prime})\in\llbracket s_{i}\rrbracket_{C}$ and
$(v,t^{\prime}+2^{i-2},v,t^{\prime}+2^{i-2})\in\llbracket
s_{i}\rrbracket_{C}$.

To prove the direction ($\Rightarrow$) of (7) suppose that
$(v,t^{\prime},v,t^{\prime})\in\llbracket s_{i-1}\rrbracket_{C}$, so we also
have that $(v,t^{\prime},v,t^{\prime})\in\llbracket s_{i}\rrbracket_{C}$ and
$(v,t^{\prime}+2^{i-2},v,t^{\prime}+2^{i-2})\in\llbracket
s_{i}\rrbracket_{C}$. Notice then that $t^{\prime}<2^{i-2}$, so $t^{\prime}$
and $t^{\prime}+2^{i-2}$ are both smaller than $2^{i-1}$. By induction
hypothesis, we get then that both quantified Boolean formulae $Q_{i}x_{i}\dots
Q_{n}x_{n}\varphi(\sigma_{t^{\prime}}(x_{1}),\dots,\sigma_{t^{\prime}}(x_{i-1}),x_{i},\dots,x_{n})$
and $Q_{i}x_{i}\dots
Q_{n}x_{n}\varphi(\sigma_{t^{\prime}+2^{i-2}}(x_{1}),\dots,\sigma_{t^{\prime}+2^{i-1}}(x_{i-1}),x_{i},\dots,x_{n})$
are valid. Furthermore, since $t^{\prime}$ is smaller than $2^{i-2}$,
$\sigma_{t^{\prime}}(x_{i-1})=\textit{false}$, and since $t^{\prime}+2^{i-2}$
only differs from $t^{\prime}$ in its $(i-1)$-th bit, which is $1$, we get
that $\sigma_{t^{\prime}+2^{i-2}}(x_{i-1})=\textit{true}$ and, for every
$j\in\\{1,\dots,{i-2}\\}$, it holds that
$\sigma_{t^{\prime}}(x_{j})=\sigma_{t^{\prime}+2^{i-2}}(x_{j})$. Hence, both
quantified Boolean formulae $Q_{i}x_{i}\dots
Q_{n}x_{n}\varphi(\sigma_{t^{\prime}}(x_{1}),\dots,\sigma_{t^{\prime}}(x_{i-2}),\textit{false},x_{i},\dots,x_{n})$
and $Q_{i}x_{i}\dots
Q_{n}x_{n}\varphi(\sigma_{t^{\prime}}(x_{1}),\dots,\sigma_{t^{\prime}}(x_{i-2}),\textit{true},x_{i},\dots,x_{n})$
are valid. Therefore, we conclude that the quantified Boolean formula $\forall
x_{i-1}Q_{i}x_{i}\dots
Q_{n}x_{n}\varphi(\sigma_{t^{\prime}}(x_{1}),\dots,\sigma_{t^{\prime}}(x_{i-2}),x_{i-1},x_{i},\dots,x_{n})$
is valid.

To show the direction ($\Leftarrow$) of (7) suppose that $\forall
x_{i-1}Q_{i}x_{i}\dots
Q_{n}x_{n}\varphi(\sigma_{t^{\prime}}(x_{1}),\dots,\sigma_{t^{\prime}}(x_{i-2}),x_{i-1},x_{i},\dots,x_{n})$
is valid. Then we get that both quantified Boolean formulae $Q_{i}x_{i}\dots
Q_{n}x_{n}\varphi(\sigma_{t^{\prime}}(x_{1}),\dots,\sigma_{t^{\prime}}(x_{i-2}),\textit{false},x_{i},\dots,x_{n})$
and $Q_{i}x_{i}\dots
Q_{n}x_{n}\varphi(\sigma_{t^{\prime}}(x_{1}),\dots,\sigma_{t^{\prime}}(x_{i-2}),\textit{true},x_{i},\dots,x_{n})$
are valid. As before, since $t^{\prime}$ is smaller than $2^{i-2}$,
$\sigma_{t^{\prime}}(x_{i-1})=\textit{false}$, and since $t^{\prime}+2^{i-2}$
only differs from $t^{\prime}$ in its $(i-1)$-th bit, which is 1, we get that
$\sigma_{t^{\prime}+2^{i-2}}(x_{i-1})=\textit{true}$ and for every
$j\in\\{1,\dots,{i-2}\\}$, it holds that
$\sigma_{t^{\prime}}(x_{j})=\sigma_{t^{\prime}+2^{i-2}}(x_{j})$. This allows
us to conclude that both $Q_{i}x_{i}\dots
Q_{n}x_{n}\varphi(\sigma_{t^{\prime}}(x_{1}),\dots,\sigma_{t^{\prime}}(x_{i-1}),x_{i},\dots,x_{n})$
and $Q_{i}x_{i}\dots
Q_{n}x_{n}\varphi(\sigma_{t^{\prime}+2^{i-2}}(x_{1}),\dots,\sigma_{t^{\prime}+2^{i-1}}(x_{i-1}),x_{i},\dots,x_{n})$
are valid. Finally, by induction hypothesis, this implies that
$(v,t^{\prime},v,t^{\prime})\in\llbracket s_{i}\rrbracket_{C}$ and
$(v,t^{\prime}+2^{i-2},v,t^{\prime}+2^{i-2})\in\llbracket
s_{i}\rrbracket_{C}$, which, as shown before, holds if and only if
$(v,t^{\prime},v,t^{\prime})\in\llbracket s_{i-1}\rrbracket_{C}$, which
concludes the proof for this case.

As we mentioned, all this together implies that Eval(ITPG, NavL[PC,NOI]) is
Pspace-hard, since ITPG $C$, expression $s_{1}$ and tuple $(v,0,v,0)$ can be
constructed in polynomial time in the size of $\psi$, and the problem of
determining whether $\psi$ is valid can be reduced to the problem of verifying
whether $(v,0,v,0)\in\llbracket s_{1}\rrbracket_{C}$.

Thus, it only remains to show that Eval(ITPG, NavL[PC,NOI]) is in Pspace. To
do this, we will provide an algorithm in Pspace that, given an ITPG C, an
expression $r$ in NavL[PC,NOI], and a tuple
$(o,t,o^{\prime},t^{\prime})\in\mathsf{PTO}(C)$, computes whether
$(o,t,o^{\prime},t^{\prime})\in\llbracket r\rrbracket_{C}$. More precisely,
Algorithm $\textsc{TupleEvalSolve}\left(C,r,(o_{1},t_{1},o_{2},t_{2})\right)$
is defined as follows.

Input : An ITPG $C=\left(\Omega,N,E,\rho,\lambda,\xi,\sigma\right)$, an
expression $r$ in ${\rm{\sf{\small NavL}}}{\rm[}{\rm{\sf{\small
PC}}},{\rm{\sf{\small NOI}}}{\rm]}$ and a pair of temporal objects
$(o_{1},t_{1},o_{2},t_{2})\in\mathsf{PTO}(C)$

Output : true if and only if $(o_{1},t_{1},o_{2},t_{2})\in\llbracket
r\rrbracket_{C}$

1 if  _$r$ is a test_ then

2 if  _$(o_{1},t_{1})\neq(o_{2},t_{2})$_ then

3 return false

4 if  _$r=\mathbf{Node}$_ then

5 return $(o_{1}\in N)$

6 else if  _$r=\mathbf{Edge}$_ then

7 return $(o_{1}\in E)$

8 else if  _$r=\ell$ for some $\ell\in\textit{Lab}$_ then

9 return $\lambda(o_{1})=\ell$

10 else if  _$r=p\mapsto v$ for some $p\in\textit{Prop}$ and
$v\in\textit{Val}$_ then

11 foreach  _valued interval $(v^{\prime},I)\in\sigma(o_{1},p)$_ do

12 if  _$t_{1}\in I$_ then

13 return $(v^{\prime}=v)$

14

15 else if  _$r=\, <k$ with $k\in\Omega$_ then

16 return $(t_{1}<k)$

17 else if  _$r=\exists$_ then

18 foreach  _interval $I\in\xi(o_{1})$_ do

19 if  _$t_{1}\in I$_ then

20 return true

21

22 else if  _$r=(?r^{\prime})$_ then

23 foreach  _$(o^{\prime},t^{\prime})\in(N\cup E)\times\Omega$_ do

24 if
_$\textsc{TupleEvalSolve}\left(C,r^{\prime},(o_{1},t_{1},o^{\prime},t^{\prime})\right)$_
then

25 return true

26

27 else if  _$r=(\mathsf{test}_{1}\vee\mathsf{test}_{2})$_ then

28 return
$\textsc{TupleEvalSolve}\left(C,\mathsf{test}_{1},(o_{1},t_{1},o_{1},t_{1})\right)\
\textbf{or}\
\textsc{TupleEvalSolve}\left(C,\mathsf{test}_{2},(o_{1},t_{1},o_{1},t_{1})\right)$

29 else if  _$r=(\mathsf{test}_{1}\wedge\mathsf{test}_{2})$_ then

30 return
$\textsc{TupleEvalSolve}\left(C,\mathsf{test}_{1},(o_{1},t_{1},o_{1},t_{1})\right)\
\textbf{and}\
\textsc{TupleEvalSolve}\left(C,\mathsf{test}_{2},(o_{1},t_{1},o_{1},t_{1})\right)$

31 else if  _$r=\left(\neg r^{\prime}\right)$_ then

32 return $\textbf{not}\
\textsc{TupleEvalSolve}\left(C,r^{\prime},(o_{1},t_{1},o_{1},t_{1})\right)$

33

34 else if  _$r=\mathbf{N}$_ then

35 return $o_{1}=o_{2}\ \textbf{and}\ t_{2}=t_{1}+1$

36 else if  _$r=\mathbf{P}$_ then

37 return $o_{1}=o_{2}\ \textbf{and}\ t_{2}=t_{1}-1$

38 else if  _$r=\mathbf{F}$_ then

39 return $t_{1}=t_{2}\ \textbf{and}\ \left(\left(o_{1}\in E\ \textbf{and}\
o_{2}=\mathsf{tgt}(o_{1})\right)\ \textbf{or}\ \left(o_{2}\in E\ \textbf{and}\
o_{1}=\mathsf{src}(o_{2})\right)\right)$

40 else if  _$r=\mathbf{B}$_ then

41 return $t_{1}=t_{2}\ \textbf{and}\ \left(\left(o_{1}\in E\ \textbf{and}\
o_{2}=\mathsf{src}(o_{1})\right)\ \textbf{or}\ \left(o_{2}\in E\ \textbf{and}\
o_{1}=\mathsf{tgt}(o_{2})\right)\right)$

42 else if  _$r=\left(r_{1}+r_{2}\right)$_ then

43 return
$\textsc{TupleEvalSolve}\left(C,r_{1},(o_{1},t_{1},o_{2},t_{2})\right)\
\textbf{or}\
\textsc{TupleEvalSolve}\left(C,r_{2},(o_{1},t_{1},o_{2},t_{2})\right)$

44 else if  _$r=\left(r_{1}\ /\ r_{2}\right)$_ then

45 foreach  _$(o^{\prime},t^{\prime})\in(N\cup E)\times\Omega$_ do

46 if
_$\textsc{TupleEvalSolve}\left(C,r_{1},(o_{1},t_{1},o^{\prime},t^{\prime})\right)\textbf{and}\
\textsc{TupleEvalSolve}\left(C,r_{2},(o^{\prime},t^{\prime},o_{2},t_{2})\right)$_
then

47 return true

48

Algorithm 4
$\textsc{TupleEvalSolve}\left(C,r,(o_{1},t_{1},o_{2},t_{2})\right)$ (part I)

44 else if  _$r=r^{\prime}\left[n,m\right]$_ then

45 if  _$m=n$_ then

46 if  _$n=0$_ then

47 return $(o_{1},t_{1})=(o_{2},t_{2})$

48 else if  _$n=1$_ then

49 return
$\textsc{TupleEvalSolve}\left(C,r^{\prime},(o_{1},t_{1},o_{2},t_{2})\right)$

50 $l\leftarrow\lfloor n/2\rfloor$

51 if  _$m$ is even_ then

52 foreach  _$(o^{\prime},t^{\prime})\in(N\cup E)\times\Omega$_ do

53 if
_$\textsc{TupleEvalSolve}\left(C,r^{\prime}[l,l],(o_{1},t_{1},o^{\prime},t^{\prime})\right)\textbf{and}\
\textsc{TupleEvalSolve}\left(C,r^{\prime}[l,l],(o^{\prime},t^{\prime},o_{2},t_{2})\right)$_
then

54 return true

55

56 else if  _$m$ is odd_ then

57 foreach  _$(o^{\prime},t^{\prime})\in(N\cup E)\times\Omega$_ do

58 foreach  _$(o^{\prime\prime},t^{\prime\prime})\in(N\cup E)\times\Omega$_ do

_59_ _ _ if  _$($_

_60_ __
$\qquad\textsc{TupleEvalSolve}\left(C,r^{\prime}[l,l],(o_{1},t_{1},o^{\prime},t^{\prime})\right)\textbf{and}$

_61_ __
$\qquad\textsc{TupleEvalSolve}\left(C,r^{\prime},(o^{\prime},t^{\prime},o^{\prime\prime},t^{\prime\prime})\right)\textbf{and}$

_62_ __
$\qquad\textsc{TupleEvalSolve}\left(C,r^{\prime}[l,l],(o^{\prime},t^{\prime},o_{2},t_{2})\right)$

63  __ $)$ then

64 return true

65

66

67 else if  _$n=0$_ then

68 if  _$m=1$_ then

69 $\textnormal{{return}}(o_{1},t_{1})=(o_{2},t_{2})\ \ \textbf{or}\ \
\textsc{TupleEvalSolve}\left(C,r^{\prime},(o_{1},t_{1},o_{2},t_{2})\right)$

70 $l\leftarrow\lfloor m/2\rfloor$

71 if  _$m$ is even_ then

72 foreach  _$(o^{\prime},t^{\prime})\in(N\cup E)\times\Omega$_ do

73 if
_$\textsc{TupleEvalSolve}\left(C,r^{\prime}[0,l],(o_{1},t_{1},o^{\prime},t^{\prime})\right)\textbf{and}\
\textsc{TupleEvalSolve}\left(C,r^{\prime}[0,l],(o^{\prime},t^{\prime},o_{2},t_{2})\right)$_
then

74 return true

75

76 else if  _$m$ is odd_ then

77 foreach  _$(o^{\prime},t^{\prime})\in(N\cup E)\times\Omega$_ do

78 foreach  _$(o^{\prime\prime},t^{\prime\prime})\in(N\cup E)\times\Omega$_ do

_79_ _ _ if  _ $($ _

_80_ __
$\qquad\textsc{TupleEvalSolve}\left(C,r^{\prime}[0,l],(o_{1},t_{1},o^{\prime},t^{\prime})\right)\
\textbf{and}$

_81_ __
$\qquad\textsc{TupleEvalSolve}\left(C,r^{\prime}[0,1],(o^{\prime},t^{\prime},o^{\prime\prime},t^{\prime\prime})\right)\
\textbf{and}$

_82_ __
$\qquad\textsc{TupleEvalSolve}\left(C,r^{\prime}[0,l],(o^{\prime},t^{\prime},o_{2},t_{2})\right)$

83  __ $)$ then

84 return true

85

86

87 else

88 foreach  _$(o^{\prime},t^{\prime})\in(N\cup E)\times\Omega$_ do

89 if
_$\textsc{TupleEvalSolve}\left(C,r^{\prime}[n,n],(o_{1},t_{1},o^{\prime},t^{\prime})\right)\textbf{and}\
\textsc{TupleEvalSolve}\left(C,r^{\prime}[0,m-n],(o^{\prime},t^{\prime},o_{2},t_{2})\right)$_
then

90 return true

91

92

93 else if  _$r=r^{\prime}\left[n,\\_\right]$_ then

94 $m\leftarrow n+(\left|\Omega\right|\cdot\left|N\cup E\right|)^{2}$

95 return
$\textsc{TupleEvalSolve}\left(C,r^{\prime}[n,m],(o_{1},t_{1},o_{2},t_{2})\right)$

return false

Algorithm 5
$\textsc{TupleEvalSolve}\left(C,r,(o_{1},t_{1},o_{2},t_{2})\right)$ (part II)

Next we show that for every ITPG
$C=\left(\Omega,N,E,\rho,\lambda,\xi,\sigma\right)$, expression $r$ in
${\rm{\sf{\small NavL}}}{\rm[}{\rm{\sf{\small PC}}},{\rm{\sf{\small
NOI}}}{\rm]}$ and tuple $(o_{1},t_{1},o_{2},t_{2})\in\mathsf{PTO}(C)$, it
holds that $(o_{1},t_{1},o_{2},t_{2})\in\llbracket r\rrbracket_{C}$ if and
only if $\textsc{TupleEvalSolve}\left(C,r,(o_{1},t_{1},o_{2},t_{2})\right)$
returns true. Besides, we will prove that TupleEvalSolve works in polynomial
space in the size of the input.

Notice firstly that the algorithm is recursive, and that the depth of the
recursion is polynomial, since at every step on which the algorithm is called,
the size of the path expression strictly decreases. There is one exception,
that happens when $r$ is of the form $\mathsf{path}[n,\\_]$. Notice that here
this expression is treated as if it was $\mathsf{path}[n,m]$, where
$m=n+\left|\Omega\right|\cdot\left|N\cup E\right|$ (a term with polynomial
size with respect to the input). Thus, the whole expression $r$ can be thought
as an equivalent expression $r^{\prime}$ where all terms of the form
$\mathsf{path}[n,\\_]$ are replaced with similar ones, in a manner that makes
the whole input remain polynomial to the original. Although it might seem that
$\mathsf{path}[n,m]$ could reach an exponential number of recursive calls,
notice that this expression is always parsed as two expressions,
$\mathsf{path}[n,n]$ and $\mathsf{path}[0,m-n]$, and then each of those is
solved in a way similar to that of exponentiation by squaring, which allows to
always get rid of the numerical occurrence indicator $[n,m]$ after at most
$O(\log m)$ recursive calls, a number that is polynomial in the size of the
input. Hence the recursion tree has polynomial height.

Secondly, assume that conjunctions ($\wedge$) and disjunctions ($\vee$) are
computed from left to right, i.e., $A(x)\wedge A(y)$ first computes $A(x)$ and
then computes $A(y)$. Hence, at the most, we will need to have in memory as
many calls to the algorithm as the recursion tree height. This number is
polynomial, and since every non-recursive step is either a non-deterministic
guess or clearly in polynomial time in the size of the input, we get that the
whole algorithm gives an answer in Pspace.

Now, let $C=\left(\Omega,N,E,\rho,\lambda,\xi,\sigma\right)$ be an ITPG, let
$r$ be an expression in ${\rm{\sf{\small NavL}}}{\rm[}{\rm{\sf{\small
PC}}},{\rm{\sf{\small NOI}}}{\rm]}$ and let
$(o_{1},t_{1},o_{2},t_{2})\in\mathsf{PTO}(C)$ be a tuple concatenating two
temporal objects. First suppose that $(o_{1},t_{1},o_{2},t_{2})\in\llbracket
r\rrbracket_{C}$. We will show, by induction on the recursion level of the
recursion tree, that there exists an execution of algorithm
$\textsc{TupleEvalSolve}\left(C,r,(o_{1},t_{1},o_{2},t_{2})\right)$ that
returns true. Notice that the base case is given for those cases where there
is no recursion. The base test cases, i.e., when $r$ is equal to either
$\mathbf{Node}$, $\mathbf{Edge}$, $\ell$, $p\mapsto v$, $<k$, or $\exists$,
are easily checked, since all the algorithm does is checking their definitions
over the temporal object $(o_{1},t_{1})$ after checking that it is equal to
the temporal object $(o_{2},t_{2})$. Notice that for property-value checking
and existence checking, the default value is false, returned at the end of the
algorithm. The base navigation operators $\mathbf{N}$, $\mathbf{P}$,
$\mathbf{F}$ and $\mathbf{B}$ are also easily checked by their definitions.
For time navigation, we check that the objects are the same and that their
associated times are consecutive, whereas for spatial navigation, we check
that the times are equal, and that the respective objects are consecutive, by
looking at the functions $\mathsf{tgt}$ and $\mathsf{src}$, as defined by the
operators.

As for the recursive cases, assume that the property holds up to recursion
level $n$ and we want to prove that it holds at recursion level $n-1$ (one
level higher in the recursion tree). Firstly, a path expression matching any
of the regular expressions $(\mathsf{test}\wedge\mathsf{test})$,
$(\mathsf{test}\vee\mathsf{test})$ or $(\neg\mathsf{test})$ can also be
checked quite straightforwardly by definition, and since the flow is
deterministic, we will omit further formal proofs. Secondly, if the path
expression $r$ is of the form $(?r^{\prime})$, then we know that
$(o_{1},t_{1},o_{2},t_{2})\in\llbracket r\rrbracket_{C}$ if and only
$(o_{1},t_{1})=(o_{2},t_{2})$ and there exists a temporal object
$(o^{\prime},t^{\prime})\in\mathsf{PTO}(C)$ such that
$(o_{1},t_{1},o^{\prime},t^{\prime})\in\llbracket r^{\prime}\rrbracket_{C}$.
In such case, the algorithm iterates one by one over the possible temporal
objects to find one that satisfies the condition. If such temporal object
exists, the call to TupleEvalSolve returns true, since we then know that the
tuple $(o_{1},t_{1},o^{\prime},t^{\prime})$ satisfies $r^{\prime}$ if and only
if there exist an execution of the call that returns true. Conversely, if no
such temporal object exists, all recursive calls to TupleEvalSolve will return
false by induction hypothesis. In this case, the algorithm will finish the
loop without returning and it will then reach the last line (in part II),
returning false.

As for regular path expressions $r$ of the form $(r_{1}+r_{2})$ where $r_{1}$
and $r_{2}$ are also regular path expressions, we know that by definition
$\llbracket(r_{1}+r_{2})\rrbracket_{C}=\llbracket
r_{1}\rrbracket_{C}\cup\llbracket r_{2}\rrbracket_{C}$. Hence,
$(o_{1},t_{1},o_{2},t_{2})\in\llbracket r\rrbracket_{C}$ if and only if
$(o_{1},t_{1},o_{2},t_{2})\in\llbracket r_{1}\rrbracket_{C}$ or
$(o_{1},t_{1},o_{2},t_{2})\in\llbracket r_{2}\rrbracket_{C}$. By induction
hypothesis, this means that $(o_{1},t_{1},o_{2},t_{2})\in\llbracket
r\rrbracket_{C}$ if and only if either
$\textsc{TupleEvalSolve}(C,r_{1},(o_{1},t_{1},o_{2},t_{2}))$ returns true or
$\textsc{TupleEvalSolve}(C,r_{2},(o_{1},t_{1},o_{2},t_{2}))$ returns true. As
the algorithm returns the disjunction of this two results, we get that
$(o_{1},t_{1},o_{2},t_{2})\in\llbracket r\rrbracket_{C}$ if and only if
$\textsc{TupleEvalSolve}(C,r,(o_{1},t_{1},o_{2},t_{2}))$ returns true

For regular path expressions $r$ of the form $(r_{1}\ /\ r_{2})$ where $r_{1}$
and $r_{2}$ are also TRPQs, we know that if
$(o_{1},t_{1},o_{2},t_{2})\in\llbracket r\rrbracket_{C}$, then there must
exist a temporal object $(o^{\prime},t^{\prime})\in\mathsf{PTO}(C)$ such that
$(o_{1},t_{1},o^{\prime},t^{\prime})\in\llbracket r_{1}\rrbracket_{C}$ and
$(o^{\prime},t^{\prime},o_{2},t_{2})\in\llbracket r_{2}\rrbracket_{C}$. Thus,
by iterating over all temporal object $(o^{\prime},t^{\prime})$, when we reach
that exact temporal object, both
$\textsc{TupleEvalSolve}(C,r_{1},(o_{1},t_{1},o^{\prime},t^{\prime}))$ and
$\textsc{TupleEvalSolve}(C,r_{2},(o^{\prime},t^{\prime},o_{2},t_{2}))$ will be
true, so the algorithm will return $\textit{true}\ \textbf{and}\
\textit{true}=\textit{true}$. On the other hand, if
$(o_{1},t_{1},o_{2},t_{2})\notin\llbracket r\rrbracket_{C}$, then no matter
what temporal object $(o^{\prime},t^{\prime})$ is being considered, we will
either have that $(o_{1},t_{1},o^{\prime},t^{\prime})\notin\llbracket
r_{1}\rrbracket_{C}$ or $(o^{\prime},t^{\prime},o_{2},t_{2})\notin\llbracket
r_{2}\rrbracket_{C}$. By induction hypothesis, this means that, for every
execution, either the first call will be false or the second will, so the
condition that makes the algorithm return true will not be met. Hence, the
last line is reached and the algorithm returns false.

For expressions $r$ matching regular expressions with numerical occurrence
indicators of the form $r^{\prime}[n,m]$, recall that, by definition,
$\llbracket r^{\prime}[n,m]\rrbracket_{C}=\bigcup_{k=n}^{m}\llbracket
r^{\prime k}\rrbracket_{C}$. This implies that
$(o_{1},t_{1},o_{2},t_{2})\in\llbracket r^{\prime}[n,m]\rrbracket_{C}$ if and
only if there exists an integer $k\in[n,m]$ such that
$(o_{1},t_{1},o_{2},t_{2})\in\llbracket r^{\prime k}\rrbracket_{C}$. We split
this case into three cases.

  1. 1.

When $n=m$, then $(o_{1},t_{1},o_{2},t_{2})\in\llbracket
r^{\prime}[n,m]\rrbracket_{C}$ if and only if
$(o_{1},t_{1},o_{2},t_{2})\in\llbracket r^{\prime n}\rrbracket_{C}$. Recall
that the concatenation operator is associative, and that $\llbracket r^{\prime
n}\rrbracket_{C}=\llbracket r^{\prime}\ /\ r^{\prime
n-1}\rrbracket_{C}=\llbracket r^{\prime}\ /\ \dots\ /\
r^{\prime}\rrbracket_{C}$ ($n$ repetitions). Hence, if we define $l=\lfloor
n/2\rfloor$, then if $n$ is even, $\llbracket r^{\prime
n}\rrbracket_{C}=\llbracket(r^{\prime l}\ /\ r^{\prime l})\rrbracket_{C}$,
whereas if $n$ is odd, $\llbracket r^{\prime
n}\rrbracket_{C}=\llbracket(r^{\prime l}\ /\ r^{\prime}\ /\ r^{\prime
l})\rrbracket_{C}$.

In the first case then, by the definition of concatenation,
$(o_{1},t_{1},o_{2},t_{2})\in\llbracket(r^{\prime l}\ /\ r^{\prime
l})\rrbracket_{C}$ if and only if there exists a temporal object
$(o^{\prime},t^{\prime})$ such that
$(o_{1},t_{1},o^{\prime},t^{\prime})\in\llbracket r^{\prime l}\rrbracket_{C}$
and $(o^{\prime},t^{\prime},o_{2},t_{2})\in\llbracket r^{\prime
l}\rrbracket_{C}$. By induction hypothesis this is equivalent to having that
there exists a temporal object $(o^{\prime},t^{\prime})$ such that both
$\textsc{TupleEvalSolve}(C,r^{\prime}[l,l],(o_{1},t_{1},o^{\prime},t^{\prime}))$
and
$\textsc{TupleEvalSolve}(C,r^{\prime}[l,l],(o^{\prime},t^{\prime},o_{2},t_{2}))$
return true, since $\llbracket r^{\prime l}\rrbracket_{C}=\llbracket
r^{\prime}[l,l]\rrbracket_{C}$. Since the algorithm iterates over all possible
temporal objects to check this condition, if such temporal object exists, it
will return true, if it does not, then it will reach the last line and return
false.

The second case is similar, except that now we need two temporal objects as
there are two concatenations, which means that
$(o_{1},t_{1},o_{2},t_{2})\in\llbracket(r^{\prime l}\ /\ r^{\prime}\ /\
r^{\prime l})\rrbracket_{C}$ if and only if there exist two temporal objects
$(o^{\prime},t^{\prime})$ and $(o^{\prime\prime},t^{\prime\prime})$ such that
$(o_{1},t_{1},o^{\prime},t^{\prime})\in\llbracket r^{\prime l}\rrbracket_{C}$,
$(o^{\prime},t^{\prime},o^{\prime\prime},t^{\prime\prime})\in\llbracket
r^{\prime}\rrbracket_{C}$ and
$(o^{\prime\prime},t^{\prime\prime},o_{2},t_{2})\in\llbracket r^{\prime
l}\rrbracket_{C}$. By induction hypothesis, and recalling again that
$\llbracket r^{\prime l}\rrbracket_{C}=\llbracket
r^{\prime}[l,l]\rrbracket_{C}$, that means that
$(o_{1},t_{1},o_{2},t_{2})\in\llbracket r\rrbracket_{C}$ if and only if there
exist two temporal objects $(o^{\prime},t^{\prime})$ and
$(o^{\prime\prime},t^{\prime\prime})$ such that the calls
$\textsc{TupleEvalSolve}(C,r^{\prime}[l,l],(o_{1},t_{1},o^{\prime},t^{\prime}))$,
$\textsc{TupleEvalSolve}(C,r^{\prime},(o^{\prime},t^{\prime},o^{\prime\prime},t^{\prime\prime}))$
and
$\textsc{TupleEvalSolve}(C,r^{\prime}[l,l],(o^{\prime\prime},t^{\prime\prime},o_{2},t_{2}))$
return true. Again, since the algorithm iterates over all possible pairs of
temporal objects $(o^{\prime},t^{\prime})$ and
$(o^{\prime\prime},t^{\prime\prime})$ to check this condition, if such
temporal objects exist, it will return true, if it does not, then it will
reach the last line and return false.

Since this recursion must stop at some point, the base case $n=1$ is included,
in which case $r$ is $r^{\prime}[1,1]$, which is equivalent to $r^{\prime}$,
since in such case we know that $(o_{1},o_{2},t_{1},t_{2})\in\llbracket
r\rrbracket_{C}$ if and only if $(o_{1},t_{1},o_{2},t_{2})\in\llbracket
r^{\prime}\rrbracket_{C}$. By hypothesis induction, this happens if and only
if $\textsc{TupleEvalSolve}(C,r^{\prime},(o_{1},t_{1},o_{2},t_{2}))$ returns
true, which is why the algorithm returns that result.

Finally, the recursion works for $n\geq 2$. The case when $n=1$ is covered as
a base case, so it only remains to look for the case when $n=0$. For such
case, recall that $r^{\prime 0}=(\exists\vee\neg\exists)$, i.e., a test that
is a tautology. Hence, $(o_{1},t_{1},o_{2},t_{2})\in\llbracket
r\rrbracket_{C}$ if and only if $(o_{1},t_{1})=(o_{2},t_{2})$, which is what
the algorithm tests.

  2. 2.

When $n=0$, the base case will be slightly different. We can assume that
$n\neq m$ since the case where $n=m$ was already covered. Hence, the base case
only needs to consider the value $m=1$. In this case, we have that $\llbracket
r\rrbracket_{C}=\llbracket r^{\prime}[0,1]\rrbracket_{C}=\llbracket r^{\prime
0}\rrbracket_{C}\cup\llbracket r^{\prime 1}\rrbracket_{C}$. As we already
discussed, checking whether $(o_{1},t_{1},o_{2},t_{2})\in\llbracket r^{\prime
0}\rrbracket_{C}$ comes down to checking whether
$(o_{1},t_{1})=(o_{2},t_{2})$, and also $\llbracket r^{\prime
1}\rrbracket_{C}=\llbracket r^{\prime}\rrbracket_{C}$. By induction, we know
that $(o_{1},t_{1},o_{2},t_{2})\in\llbracket r^{\prime}\rrbracket_{C}$ if and
only if $\textsc{TupleEvalSolve}(C,r^{\prime},(o_{1},t_{1},o_{2},t_{2}))$
returns true. Since the algorithm returns true if either of these conditions
hold, this case is correctly covered.

As for the recursive case, it is very similar to the previous one. If we
define again $l=\lfloor m/2\rfloor$, we can notice that, if $m$ is even, then
$\llbracket r^{\prime}[0,m]\rrbracket_{C}=\llbracket(r^{\prime}[0,l]\ /\
r^{\prime}[0,l])\rrbracket_{C}$, whereas if $m$ is odd, then $\llbracket
r^{\prime}[0,m]\rrbracket_{C}=\llbracket(r^{\prime}[0,l]\ /\ r^{\prime}\ /\
r^{\prime}[0,l])\rrbracket_{C}$.

To show the part when $m$ is even, notice that
$(o_{1},t_{1},o_{2},t_{2})\in\llbracket r\rrbracket_{C}$ if and only if
$(o_{1},t_{1},o_{2},t_{2})\in\llbracket r^{\prime i}\rrbracket_{C}$ for some
$i\in[0,m]$. For every $i\in[0,m]$ there exist two integers, $j_{i}:=\lfloor
i/2\rfloor$ and $k_{i}:=\lceil i/2\rceil$, both in the interval $[0,l]$, that
satisfy that $j_{i}+k_{i}=i$. Since the concatenation operator is associative,
this means that $\llbracket r^{\prime}_{i}\rrbracket_{C}=\llbracket(r^{\prime
j_{i}}\ /\ r^{\prime k_{i}})\rrbracket_{C}$, which in turn implies that
$\llbracket r\rrbracket_{C}=\bigcup_{i=0}^{m}\llbracket
r^{\prime}_{i}\rrbracket_{C}=\bigcup_{i=0}^{m}\llbracket(r^{\prime j_{i}}\ /\
r^{\prime k_{i}})\rrbracket_{C}$.

Then, by definition of the concatenation operator,
$(o_{1},t_{1},o_{2},t_{2})\in\bigcup_{i=0}^{m}\llbracket(r^{\prime j_{i}}\ /\
r^{\prime k_{i}})\rrbracket_{C}$ if and only if there exists a temporal object
$(o^{\prime},t^{\prime})$ such that
$(o_{1},t_{1},o^{\prime},t^{\prime})\in\llbracket r^{\prime
j_{i}}\rrbracket_{C}$ and $(o^{\prime},t^{\prime},o_{2},t_{2})\in\llbracket
r^{k_{i}}\rrbracket_{C}$.

Since both $j_{i}$ and $k_{i}$ are bounded by $l$, $\llbracket r^{\prime
j_{i}}\rrbracket_{C}\subseteq\llbracket\bigcup_{i=0}^{l}r^{\prime
i}\rrbracket_{C}$, and $\llbracket r^{\prime
k_{i}}\rrbracket_{C}\subseteq\llbracket\bigcup_{i=0}^{l}r^{\prime
i}\rrbracket_{C}$, so any tuple $(o,t,o^{\prime},t^{\prime})$ in $\llbracket
r^{\prime k_{i}}\rrbracket_{C}$ or $\llbracket r^{\prime j_{i}}\rrbracket_{C}$
will also be in $\llbracket\bigcup_{i=0}^{l}r^{\prime
i}\rrbracket_{C}=\llbracket r^{\prime}[0,l]\rrbracket_{C}$. Hence,
$(o_{1},t_{1},o^{\prime},t^{\prime})\in\llbracket r^{\prime
j_{i}}\rrbracket_{C}$ implies that
$(o_{1},t_{1},o^{\prime},t^{\prime})\in\llbracket
r^{\prime}[0,l]\rrbracket_{C}$ and
$(o^{\prime},t^{\prime},o_{2},t_{2})\in\llbracket r^{\prime
k_{i}}\rrbracket_{C}$ implies that
$(o^{\prime},t^{\prime},o_{2},t_{2})\in\llbracket
r^{\prime}[0,l]\rrbracket_{C}$. It can then be inferred that having that
$(o_{1},t_{1},o_{2},t_{2})\in\bigcup_{i=0}^{m}\llbracket(r^{\prime j_{i}}\ /\
r^{\prime k_{i}})\rrbracket_{C}$ can only hold if there exists a temporal
object $(o^{\prime},t^{\prime})$ satisfying that
$(o_{1},t_{1},o^{\prime},t^{\prime})\in\llbracket
r^{\prime[}0,l]\rrbracket_{C}$ and
$(o^{\prime},t^{\prime},o_{2},t_{2})\in\llbracket
r^{\prime}[0,l]\rrbracket_{C}$. As a result,
$(o_{1},t_{1},o_{2},t_{2})\in\bigcup_{i=0}^{n}\llbracket(r^{\prime j_{i}}\ /\
r^{\prime k_{i}})\rrbracket_{C}$ implicates that
$(o_{1},t_{1},o_{2},t_{2})\in\llbracket(r^{\prime}[0,l]\ /\
r^{\prime}[0,l])\rrbracket_{C}$. In consequence, we get that
$\bigcup_{i=0}^{n}\llbracket(r^{\prime j_{i}}\ /\ r^{\prime
k_{i}})\rrbracket_{C}\subseteq\llbracket(r^{\prime}[0,l]\ /\
r^{\prime}[0,l])\rrbracket_{C}$.

For the inverse inclusion, notice that if
$(o_{1},t_{1},o_{2},t_{2})\in\llbracket(r^{\prime}[0,l]\ /\
r^{\prime}[0,l])\rrbracket_{C}$, then there must exist a temporal object
$(o^{\prime},t^{\prime})$ and two integers $j$ and $k$ in $[0,l]$ such that
$(o_{1},t_{1},o^{\prime},t^{\prime})\in\llbracket r^{\prime j}\rrbracket_{C}$
and $(o^{\prime},t^{\prime},o_{2},t_{2})\in\llbracket r^{\prime
k}\rrbracket_{C}$, which implies that
$(o_{1},t_{1},o_{2},t_{2})\in\llbracket(r^{\prime j}\ /\ r^{\prime
k})\rrbracket_{C}$. Again, since concatenation is associative,
$\llbracket(r^{\prime i}\ /\ r^{\prime j})\rrbracket_{C}=\llbracket r^{\prime
i+j}\rrbracket_{C}$, and because $i+j$ is at most $n$,
$(o_{1},t_{1},o_{2},t_{2})\in\bigcup_{i=0}^{n}\llbracket r^{\prime
i}\rrbracket_{C}$, i.e., $(o_{1},t_{1},o_{2},t_{2})\in\llbracket
r\rrbracket_{C}$. As a result, we get that $\llbracket(r^{\prime}[0,l]\ /\
r^{\prime}[0,l])\rrbracket_{C}\subseteq\bigcup_{i=0}^{n}\llbracket(r^{\prime
j_{i}}\ /\ r^{\prime k_{i}})\rrbracket_{C}$.

Combining these two inclusions with the equality $\llbracket
r\rrbracket_{C}=\bigcup_{i=0}^{n}\llbracket(r^{\prime j_{i}}\ /\ r^{\prime
k_{i}})\rrbracket_{C}$, we get that $\llbracket
r\rrbracket_{C}=\llbracket(r^{\prime}[0,l]\ /\
r^{\prime}[0,l])\rrbracket_{C}$.

To show the part where $n$ is odd, notice that
$(o_{1},t_{1},o_{2},t_{2})\in\llbracket r\rrbracket_{C}$ if and only if there
exists an integer $i\in[0,m]$ such that
$(o_{1},t_{1},o_{2},t_{2})\in\llbracket r^{\prime i}\rrbracket_{C}$. Notice
then that $i$ can be written as the sum of three integers, $k_{i}:=\lfloor
i/2\rfloor$ ($\in[0,l]$), $j_{i}=:\lfloor i/2\rfloor$ ($\in[0,l]$) and
$s_{i}:=(imod2)$ ($\in[0,1]$). Since the concatenation operator is
associative, this means that $\llbracket
r^{\prime}_{i}\rrbracket_{C}=\llbracket(r^{\prime j_{i}}\ /\ r^{\prime s_{i}}\
/\ r^{\prime k_{i}})\rrbracket_{C}$, which in turn implies that $\llbracket
r\rrbracket_{C}=\bigcup_{i=0}^{m}\llbracket
r^{\prime}_{i}\rrbracket_{C}=\bigcup_{i=0}^{m}\llbracket(r^{\prime j_{i}}\ /\
r^{\prime s_{i}}\ /\ r^{\prime k_{i}})\rrbracket_{C}$.

Then, by definition of the concatenation operator,
$(o_{1},t_{1},o_{2},t_{2})\in\bigcup_{i=0}^{m}\llbracket(r^{\prime j_{i}}\ /\
r^{\prime s_{1}}\ /\ r^{\prime k_{i}})\rrbracket_{C}$ if and only if there
exist two temporal objects $(o^{\prime},t^{\prime})$ and
$(o^{\prime\prime},t^{\prime\prime})$ such that
$(o_{1},t_{1},o^{\prime},t^{\prime})\in\llbracket r^{\prime
j_{i}}\rrbracket_{C}$,
$(o^{\prime},t^{\prime},o^{\prime\prime},t^{\prime\prime})\in\llbracket
r^{\prime s_{i}}\rrbracket_{C}$ and
$(o^{\prime\prime},t^{\prime\prime},o_{2},t_{2})\in\llbracket r^{\prime
k_{i}}\rrbracket_{C}$.

Since both $j_{i}$ and $k_{i}$ are bounded by $l$, $\llbracket r^{\prime
j_{i}}\rrbracket_{C}\subseteq\llbracket\bigcup_{i=0}^{l}r^{\prime
i}\rrbracket_{C}$, and $\llbracket r^{\prime
k_{i}}\rrbracket_{C}\subseteq\llbracket\bigcup_{i=0}^{l}r^{\prime
i}\rrbracket_{C}$, so any tuple $(o,t,o^{\prime},t^{\prime})$ in $\llbracket
r^{\prime k_{i}}\rrbracket_{C}$ or $\llbracket r^{\prime j_{i}}\rrbracket_{C}$
will also be in $\llbracket\bigcup_{i=0}^{l}r^{\prime
i}\rrbracket_{C}=\llbracket r^{\prime}[0,l]\rrbracket_{C}$. Similarly, any
tuple in $\llbracket r^{\prime s_{1}}\rrbracket_{C}$ will also be in
$\llbracket r^{\prime}[0,1]\rrbracket_{C}$. Hence,
$(o_{1},t_{1},o^{\prime},t^{\prime})\in\llbracket r^{\prime
j_{i}}\rrbracket_{C}$ implies that
$(o_{1},t_{1},o^{\prime},t^{\prime})\in\llbracket
r^{\prime}[0,l]\rrbracket_{C}$,
$(o^{\prime},t^{\prime},o^{\prime\prime},t^{\prime\prime})\in\llbracket
r^{\prime s_{i}}\rrbracket_{C}$ implies that
$(o^{\prime},t^{\prime},o^{\prime\prime},t^{\prime\prime})\in\llbracket
r^{\prime}[0,1]\rrbracket_{C}$ and
$(o^{\prime\prime},t^{\prime\prime},o_{2},t_{2})\in\llbracket
r^{k_{i}}\rrbracket_{C}$ implies that
$(o^{\prime\prime},t^{\prime\prime},o_{2},t_{2})\in\llbracket
r[0,l]\rrbracket_{C}$. It can then be inferred that having that
$(o_{1},t_{1},o_{2},t_{2})\in\bigcup_{i=0}^{m}\llbracket(r^{\prime j_{i}}\ /\
r^{\prime s_{i}}\ /\ r^{\prime k_{i}})\rrbracket_{C}$ can only hold if there
exist two temporal objects $(o^{\prime},t^{\prime})$ and
$(o^{\prime\prime},t^{\prime\prime})$ satisfying that
$(o_{1},t_{1},o^{\prime},t^{\prime})\in\llbracket
r^{\prime[}0,l]\rrbracket_{C}$,
$(o^{\prime},t^{\prime},o^{\prime\prime},t^{\prime\prime})\in\llbracket
r^{\prime}[0,1]\rrbracket_{C}$ and
$(o^{\prime\prime},t^{\prime\prime},o_{2},t_{2})\in\llbracket
r[0,l]\rrbracket_{C}$. As a result,
$(o_{1},t_{1},o_{2},t_{2})\in\bigcup_{i=0}^{n}\llbracket(r^{\prime j_{i}}\ /\
r^{\prime k_{i}})\rrbracket_{C}$ implicates that
$(o_{1},t_{1},o_{2},t_{2})\in\llbracket(r^{\prime}[0,l]\ /\ r^{\prime}[0,1]\
/\ r^{\prime}[0,l])\rrbracket_{C}$. In consequence, we get that
$\bigcup_{i=0}^{n}\llbracket(r^{\prime j_{i}}\ /\ r^{\prime
k_{i}})\rrbracket_{C}\subseteq\llbracket(r^{\prime}[0,l]\ /\ r^{\prime}[0,1]\
/\ r^{\prime}[0,l])\rrbracket_{C}$.

For the inverse inclusion, notice that if
$(o_{1},t_{1},o_{2},t_{2})\in\llbracket(r^{\prime}[0,l]\ /\ r^{\prime}[0,1]\
/\ r^{\prime}[0,l])\rrbracket_{C}$, then there must exist two temporal objects
$(o^{\prime},t^{\prime})$ and $(o^{\prime\prime},t^{\prime\prime})$, and three
integers $j\in[0,l]$, $s\in[0,1]$ and $k\in[0,l]$ such that
$(o_{1},t_{1},o^{\prime},t^{\prime})\in\llbracket r^{\prime j}\rrbracket_{C}$,
$(o^{\prime\prime},t^{\prime\prime})\in\llbracket r^{\prime s}\rrbracket_{C}$
and $(o^{\prime\prime},t^{\prime\prime},o_{2},t_{2})\in\llbracket r^{\prime
k}\rrbracket_{C}$, which implies that
$(o_{1},t_{1},o_{2},t_{2})\in\llbracket(r^{\prime j}\ /\ r^{\prime s}\ /\
r^{\prime k})\rrbracket_{C}$. Again, since concatenation is associative,
$\llbracket(r^{\prime i}\ /\ r^{\prime s}\ /\ r^{\prime
j})\rrbracket_{C}=\llbracket r^{\prime i+s+j}\rrbracket_{C}$, and because
$i+s+j$ is at most $n$,
$(o_{1},t_{1},o_{2},t_{2})\in\bigcup_{i=0}^{n}\llbracket r^{\prime
i}\rrbracket_{C}$, i.e., $(o_{1},t_{1},o_{2},t_{2})\in\llbracket
r\rrbracket_{C}$. As a result, we get that $\llbracket(r^{\prime}[0,l]\ /\
r^{\prime}[0,1]\ /\
r^{\prime}[0,l])\rrbracket_{C}\subseteq\bigcup_{i=0}^{n}\llbracket(r^{\prime
j_{i}}\ /\ r^{\prime k_{i}})\rrbracket_{C}$.

As before, combining these two inclusions with the equality $\llbracket
r\rrbracket_{C}=\bigcup_{i=0}^{n}\llbracket(r^{\prime j_{i}}\ /\ r^{\prime
l_{i}}\ /\ r^{\prime k_{i}})\rrbracket_{C}$, we get that $\llbracket
r\rrbracket_{C}=\llbracket(r^{\prime}[0,l]\ /\ r^{\prime}[0,1]\ /\
r^{\prime}[0,l])\rrbracket_{C}$. With these two results in mind then, i.e.,
that $\llbracket r^{\prime}[0,m]\rrbracket_{C}=\llbracket(r^{\prime}[0,l]\ /\
r^{\prime}[0,l])\rrbracket_{C}$ when $m$ is even, whereas if $m$ is odd, then
$\llbracket r^{\prime}[0,m]\rrbracket_{C}=\llbracket(r^{\prime}[0,l]\ /\
r^{\prime}\ /\ r^{\prime}[0,l])\rrbracket_{C}$, we know that
$(o_{1},t_{1},o_{2},t_{2})\in\llbracket r^{\prime}[0,m]\rrbracket_{C}$ if and
only if (i) $m$ is even and there exists a temporal object
$(o^{\prime},t^{\prime})$ such that
$(o_{1},t_{1},o^{\prime},t^{\prime})\in\llbracket
r^{\prime}[0,l]\rrbracket_{C}$ and
$(o^{\prime},t^{\prime},o_{2},t_{2})\in\llbracket
r^{\prime}[0,l]\rrbracket_{C}$, or (ii) $m$ is odd and there exist two
temporal objects $(o^{\prime},t^{\prime})$ and
$(o^{\prime\prime},t^{\prime\prime})$ such that
$(o_{1},t_{1},o^{\prime},t^{\prime})\in\llbracket
r^{\prime}[0,l]\rrbracket_{C}$,
$(o^{\prime},t^{\prime},o^{\prime\prime},t^{\prime\prime})\in\llbracket
r^{\prime}[0,1]\rrbracket_{C}$ and
$(o^{\prime\prime},t^{\prime\prime},o_{2},t_{2})\in\llbracket
r^{\prime}[0,l]\rrbracket_{C}$.

By induction, (i) holds if and only if there exists a temporal object
$(o^{\prime},t^{\prime})$ such that both
$\textsc{TupleEvalSolve}(C,r^{\prime}[0,l],(o_{1},t_{1},o^{\prime},t^{\prime}))$
and
$\textsc{TupleEvalSolve}(C,r^{\prime}[0,l],(o^{\prime},t^{\prime},o_{2},t_{2}))$
return true. Since the algorithm iterates over all temporal objects
$(o^{\prime},t^{\prime})$ for this case, and then checks that both those
conditions are met to return true, it will return true if $(i)$ holds, and it
will reach the last line and return false if no such pair existed.

Also by induction, (ii) holds if and only if there exist two temporal objects
$(o^{\prime},t^{\prime})$ and $(o^{\prime\prime},t^{\prime\prime})$ such that
the three calls
$\textsc{TupleEvalSolve}(C,r^{\prime}[0,l],(o_{1},t_{1},o^{\prime},t^{\prime}))$,
$\textsc{TupleEvalSolve}(C,r^{\prime}[0,l],(o^{\prime},t^{\prime},o^{\prime\prime},t^{\prime\prime}))$
and
$\textsc{TupleEvalSolve}(C,r^{\prime}[0,l],(o^{\prime\prime},t^{\prime\prime},o_{2},t_{2}))$
return true. Here again, since the algorithm iterates over all pairs of
temporal objects $(o^{\prime},t^{\prime})$ and
$(o^{\prime\prime},t^{\prime\prime})$ and sees if these three conditions are
met to return true, it will return true if (ii) holds, and it will reach the
last line and return false otherwise.

Hence, when $n=0$, the algorithm also returns true if and only if
$(o_{1},t_{1},o_{2},t_{2})\in\llbracket r\rrbracket_{C}$

  3. 3.

When $m\neq n$ and $n\neq 0$, then $(o_{1},t_{1},o_{2},t_{2})\llbracket
r^{\prime}[n,m]\rrbracket_{C}$ if and only if there exists $i\in[n,m]$ such
that $(o_{1},t_{1},o_{2},t_{2})\llbracket r^{\prime i}\rrbracket_{C}$. In this
case, $i=n+d$ for some $d\in[0,m-n]$, and since the concatenation operator is
associative, $(o_{1},t_{1},o_{2},t_{2})\llbracket r^{\prime i}\rrbracket_{C}$
if and only if there exists $(o^{\prime},t^{\prime})$ such that
$(o_{1},t_{1},o^{\prime},t^{\prime})\in\llbracket r^{\prime n}\rrbracket_{C}$
and $(o^{\prime},t^{\prime},o_{2},t_{2})\in\llbracket r^{\prime
d}\rrbracket_{C}$. By induction, and since $\llbracket r^{\prime
n}\rrbracket_{C}=\llbracket r^{\prime}[n,n]\rrbracket_{C}$,
$(o_{1},t_{1},o^{\prime},t^{\prime})\in\llbracket r^{\prime n}\rrbracket_{C}$
if and only if
$\textsc{TupleEvalSolve}(C,r^{\prime}[n,n],(o_{1},t_{1},o^{\prime},t^{\prime}))$.
Similarly, $(o^{\prime},t^{\prime},o_{2},t_{2})\in\llbracket r^{\prime
d}\rrbracket_{C}$ for some $d\in[0,m-n]$ if and only if
$(o^{\prime},t^{\prime},o_{2},t_{2})\in\llbracket
r^{\prime}[0,m-n]\rrbracket_{C}$, which by induction holds if and only if
$\textsc{TupleEvalSolve}(C,r^{\prime}[0,m-n],(o^{\prime},t^{\prime},o_{2},t_{2}))$.

Together, this means that $(o_{1},t_{1},o_{2},t_{2})\in\llbracket
r\rrbracket_{C}$ if and only if there exists a temporal object
$(o^{\prime},t^{\prime})$ such that
$\textsc{TupleEvalSolve}(C,r^{\prime}[n,n],(o_{1},t_{1},o^{\prime},t^{\prime})$
and
$\textsc{TupleEvalSolve}(C,r^{\prime}[0,m-n],(o^{\prime},t^{\prime},o_{2},t_{2}))$.
Since the algorithm iterates over all temporal objects
$(o^{\prime},t^{\prime})$ and checks if these conditions are met to return
true, it will return true if $(o_{1},t_{1},o_{2},t_{2})\in\llbracket
r\rrbracket_{C}$ and it will reach the last line and return false otherwise.

Finally, for an expression $r$ matching a regular expressions with numerical
occurrence indicators of the form $r^{\prime}[n,\\_]$, recall that we showed
in Section C-A that $\llbracket r^{\prime}[n,\\_]\rrbracket_{C}=\llbracket
r^{\prime}[n,m]\rrbracket_{C}$, where the expression $m:=n+(|\Omega|+|V\cup
E|)^{2}$ is polynomial in the size of the original input. By induction,
$(o_{1},t_{1},o_{2},t_{2})\in\llbracket r^{\prime}[n,m]\rrbracket_{C}$ if and
only if $\textsc{TupleEvalSolve}(C,r^{\prime}[n,m],(o_{1},t_{1},o_{2},t_{2}))$
returns true, which is what the algorithm returns for this case. Altogether,
we proved that TupleEvalSolve works in polynomial space, and that
$\textsc{TupleEvalSolve}(C,r,(o_{1},t_{1},o_{2},t_{2}))$ returns true if and
only if $(o_{1},t_{1},o_{2},t_{2})\in\llbracket r\rrbracket_{C}$. This
concludes the proof of the theorem.

##  Appendix D Allowing numerical occurrence indicators only in the axes:
additional complexity results

A natural question is whether there is a restriction on ${\rm{\sf{\small
NavL}}}{\rm[}{\rm{\sf{\small NOI}}}{\rm]}$ that can reduce the complexity of
the evaluation problem but is still expressive enough to represent some useful
queries. At this point, a restriction used in the study of XPath comes to the
rescue [M05]. In what follows, we show that the complexity of the evaluation
problem is lower if numerical occurrence indicators are only allowed in the
axes.

######  Theorem D.1.

Eval(ITPG, NavL[ANOI]) is NP-complete.

###### Proof.

To show NP-hardness, consider the following decision problem called Subset Sum
(SUBSET-SUM), which is known to be NP-complete [SubsetSum1990]:

Problem: SUBSET-SUM Input: A finite set of integers $A\subsetneq\mathbb{N}$,
and a positive integer $S\in\mathbb{N}$ Output: true if there exists a subset
$A^{\prime}\subseteq A$ of $A$ such that $\sum_{a\in A^{\prime}}a=S$.

Given a set $A\subsetneq\mathbb{N}$, and an integer $S\in\mathbb{N}$, the goal
is to provide a polynomial-time algorithm that returns an ITPG $C$, a tuple
$(o_{1},t_{1},o_{2},t_{2})$, and an expression $r$ in ${\rm{\sf{\small
NavL}}}{\rm[}{\rm{\small{\sf ANOI}}}{\rm]}$ such that
$(o_{1},t_{1},o_{2},t_{2})\in\llbracket r\rrbracket_{C}$ if and only if there
exists $A^{\prime}\subseteq A$ such that $\sum_{a\in A^{\prime}}a=S$. More
specifically, $C$ will be the ITPG
$\left(\Omega,N,E,\rho,\lambda,\xi,\sigma\right)$ where $\Omega=[0,S]$,
$N=\\{v\\}$, $E=\varnothing$, $\rho$ is an empty function, $\lambda(v)=l$,
$\xi(v)=\left\\{[0,S]\right\\}$ and $\sigma$ is an empty function. In other
words, $C$ is an ITPG consisting of only one node existing from time $0$ to
time $S$, with no edges or properties. The tuple $(o_{1},t_{1},o_{2},t_{2})$
in our reduction will be given by $(v,0,v,S)$. Moreover, assuming that
$A=\\{a_{1},\dots,a_{n}\\}$, expression $r$ is defined as follows:

$\displaystyle r$ $\displaystyle=$
$\displaystyle\left(\mathbf{N}[a_{1},a_{1}]+\mathbf{N}[0,0]\right)\ /\ \cdots\
/\ \left(\mathbf{N}[a_{n},a_{n}]+\mathbf{N}[0,0]\right)$

Notice that ITPG $C$, expression $r$ in ${\rm{\sf{\small
NavL}}}{\rm[}{\rm{\small{\sf ANOI}}}{\rm]}$ and tuple $(v,0,v,S)$ can be
computed in polynomial time in the sizes of $A$ and $S$. Besides, it is
straightforward to prove that $(v,0,v,S)\in\llbracket r\rrbracket_{C}$ if and
only if there exists $A^{\prime}\subseteq A$ such that $\sum_{a\in
A^{\prime}}a=S$. This concludes the of NP-hardness of Eval(ITPG, NavL[ANOI]).

To show that this problem is NP-complete, it only remains to show that the
problem is also in NP. We present a nondeterministic algorithm that works in
polynomial time, TupleEvalSolve_ANOI, that, given an ITPG $C$, an expression
$r$ in ${\rm{\sf{\small NavL}}}{\rm[}{\rm{\small{\sf ANOI}}}{\rm]}$ and a pair
of temporal objects $(o_{1},t_{1},o_{2},t_{2})$, has a run that returns true
if and only if $(o,t,o^{\prime},t^{\prime})\in\llbracket r\rrbracket_{C}$.
This procedure is presented in Algorithm 6.

Input : An ITPG $C=\left(\Omega,N,E,\rho,\lambda,\xi,\sigma\right)$, an
expression $r$ in ${\rm{\sf{\small NavL}}}{\rm[}{\rm{\small{\sf ANOI}}}{\rm]}$
and a pair of temporal objects $\left(o_{1},t_{1},o_{2},t_{2}\right)$

Output : true if $\left(o,t,o^{\prime},t^{\prime}\right)\in\llbracket
r\rrbracket_{C}$

1 if  _$r$ is a $\mathsf{test}$_ then

2 if  _$(o_{1},t_{1})\neq(o_{2},t_{2})$_ then

3 return false

4 else if  _$r=\mathbf{Node}$_ then

5 return $(o_{1}\in N)$

6 else if  _$r=\mathbf{Edge}$_ then

7 return $(o_{1}\in E)$

8 else if  _$r=\ell$ for some $\ell\in\textit{Lab}$_ then

9 return $(\lambda(o_{1})=\ell)$

10 else if  _$r=p\mapsto v$ for some $p\in\textit{Prop}$ and
$v\in\textit{Val}$_ then

11 foreach  _valued interval $(v^{\prime},I)\in\sigma(o_{1},p)$_ do

12 if  _$t_{1}\in I$_ then

13 return $v^{\prime}=v$

14

15 return false

16 else if  _$r\,=\, <k$ with $k\in\Omega$_ then

17 return $(t_{1}<k)$

18 else if  _$r=\exists$_ then

19 foreach  _interval $I\in\xi(o_{1})$_ do

20 if  _$t_{1}\in I$_ then

21 return true

22

23 return false

24 else if  _$r=(\mathsf{test}_{1}\vee\mathsf{test}_{2})$_ then

25 return
$\textsc{TupleEvalSolve}\left(C,(o_{1},t_{1},o_{1},t_{1}),\mathsf{test}_{1}\right)$
or
$\textsc{TupleEvalSolve}\left(C,(o_{1},t_{1},o_{1},t_{1}),\mathsf{test}_{2}\right)$

26 else if  _$r=(\mathsf{test}_{1}\wedge\mathsf{test}_{2})$_ then

27 return
$\textsc{TupleEvalSolve}\left(C,(o_{1},t_{1},o_{1},t_{1}),\mathsf{test}_{1}\right)$
and
$\textsc{TupleEvalSolve}\left(C,(o_{1},t_{1},o_{1},t_{1}),\mathsf{test}_{2}\right)$

28 else if  _$r=\left(\neg r^{\prime}\right)$_ then

29 return not
$\textsc{TupleEvalSolve}\left(C,(o_{1},t_{1},o_{1},t_{1}),r^{\prime}\right)$

30

31 else if  _$r=\mathbf{N}$_ then

32 return $\left(o_{1}=o_{2}\ \textbf{and}\ t_{2}=t_{1}+1\right)$

33 else if  _$r=\mathbf{P}$_ then

34 return $\left(o_{1}=o_{2}\ \textbf{and}\ t_{2}=t_{1}-1\right)$

35 else if  _$r=\mathbf{F}$_ then

36 return $\left(t_{1}=t_{2}\ \textbf{and}\ \left(\left(o_{1}\in E\
\textbf{and}\ o_{2}=\mathsf{tgt}\left(o_{1}\right)\right)\ \textbf{or}\
\left(o_{2}\in E\ \textbf{and}\
o_{1}=\mathsf{src}\left(o_{2}\right)\right)\right)\right)$

37 else if  _$r=\mathbf{B}$_ then

38 return $\left(t_{1}=t_{2}\ \textbf{and}\ \left((o_{1}\in E\ \textbf{and}\
o_{2}=\mathsf{src}(o_{1}))\ \textbf{or}\ (o_{2}\in E\ \textbf{and}\
o_{1}=\mathsf{tgt}(o_{2}))\right)\right)$

Algorithm 6 $\textsc{TupleEvalSolve\\_ANOI}(C,(o_{1},t_{1},o_{2},t_{2}),r)$
(part I)

TupleEvalSolve_ANOI is very similar to TupleEvalSolve, so we will not discuss
in detail what it does. Instead, we give an intuition of what the differences
are that allow to return the right answer in non-deterministic polynomial
time, instead of polynomial space. First, notice that if $r$ is a test, then
the algorithm works by solving basic tests efficiently, and then conjunctions,
disjunctions and negations of tests are solved just by using directly the
definition of these Boolean connectives. Hence, unlike what happens in the
presence of path conditions, where we can have nested expressions with
existential conditions and negations of existential conditions, sub-
expressions for tests are efficiently solved by TupleEvalSolve_ANOI. Second,
notice that for spatial navigation, we write the problem in terms of the
reachability problem for graphs in a number of steps in a set
$\\{n,\ldots,m\\}$. This problem can be efficiently solved by using
exponentiation by squaring on the adjacency matrix. Besides, notice that for
spatial navigation expressions in ${\rm{\sf{\small
NavL}}}{\rm[}{\rm{\small{\sf ANOI}}}{\rm]}$, we need to consider as many new
objects as there are in $V\cup E$ since the time is fixed, which is why
expressions $\mathbf{F}[n,\\_]$ and $\mathbf{B}[n,\\_]$ are equivalent to
$\mathbf{F}[n,m]$ and $\mathbf{B}[n,m]$, respectively, with $m=n+|N\cup
E|=n+|N|+|E|$. Finally, polynomial time executions are ensured by the non-
deterministic guess for $(o^{\prime},t^{\prime})$ in Line $64$, and the fact
that the depth of the recursion tree is linear with respect to the size of the
input expression $r$. In particular, we do a single non-deterministic guess in
Line $64$, instead of an exponential number of attempts (with respect to the
size of the representation of $\Omega$) that would be necessary to find the
right pair $(o^{\prime},t^{\prime})$ in a deterministic algorithm.

36 else if  _$r=\mathbf{N}[n,m]$_ then

37 return $\left(o_{1}=o_{2}\ \textbf{and}\ n\leq(t_{2}-t_{1})\leq m\right)$

38 else if  _$r=\mathbf{P}[n,m]$_ then

39 return $\left(o_{1}=o_{2}\ \textbf{and}\ n\leq(t_{1}-t_{2})\leq m\right)$

40 else if  _$r=\mathbf{F}[n,m]$_ then

41 if  _$t_{1}\neq t_{2}$_ then

42 return false

43 else

44 Let $G=(N^{\prime},E^{\prime})$ be the graph where:

45

  * •

$N^{\prime}=(N\cup E)$

  * •

$E^{\prime}=\\{(v,e)\in N\times E\ |\ \mathsf{src}(e)=v\\}\cup\\{(e,v)\in
E\times N\ |\ \mathsf{tgt}(e)=v\\}$

return $o_{2}$ is reachable from $o_{1}$ in $k$ steps in $G$, where
$k\in\\{n,\ldots,m\\}$

46

47 else if  _$r=\mathbf{B}[n,m]$_ then

48 if  _$t_{1}\neq t_{2}$_ then

49 return false

50 else

51 Let $G=(N^{\prime},E^{\prime})$ be the graph where:

52

  * •

$N^{\prime}=(N\cup E)$

  * •

$E^{\prime}=\\{(v,e)\in N\times E\ |\ \mathsf{tgt}(e)=v\\}\cup\\{(e,v)\in
E\times N\ |\ \mathsf{src}(e)=v\\}$

return $o_{2}$ is reachable from $o_{1}$ in $k$ steps in $G$, where
$k\in\\{n,\ldots,m\\}$

53

54 else if  _$r=\mathbf{N}[n,\\_]$_ then

55 return $\left(o_{1}=o_{2}\ \textbf{and}\ n\leq(t_{2}-t_{1})\right)$

56 else if  _$r=\mathbf{P}[n,\\_]$_ then

57 return $\left(o_{1}=o_{2}\ \textbf{and}\ n\leq(t_{1}-t_{2})\right)$

58 else if  _$r=\mathbf{F}[n,\\_]$_ then

59 $m\leftarrow n+|N|+|E|$

60 return
$\textsc{TupleEvalSolve\\_ANOI}(C,(o_{1},t_{1},o_{2},t_{2}),\mathbf{F}[n,m])$

61 else if  _$r=\mathbf{B}[n,\\_]$_ then

62 $m\leftarrow n+|N|+|E|$

63 return
$\textsc{TupleEvalSolve\\_ANOI}(C,(o_{1},t_{1},o_{2},t_{2}),\mathbf{B}[n,m])$

64 else if  _$r=(r_{1}+r_{2})$_ then

65 Guess $i\in\\{1,2\\}$

66 return $\textsc{TupleEvalSolve\\_ANOI}(C,(o_{1},t_{1},o_{2},t_{2}),r_{i})$

67 else if  _$r=(r_{1}\ /\ r_{2})$_ then

68 Guess $(o^{\prime},t^{\prime})\in(N\cup E)\times\Omega$

69 return
$\textsc{TupleEvalSolve\\_ANOI}(C,(o_{1},t_{1},o^{\prime},t^{\prime}),r_{1})$
and
$\textsc{TupleEvalSolve\\_ANOI}(C,(o^{\prime},t^{\prime},o_{2},t_{2}),r_{2})$

70

Algorithm 7 $\textsc{TupleEvalSolve\\_ANOI}(C,(o_{1},t_{1},o_{2},t_{2}),r)$
(part II)

∎

We have that Eval(ITPG, NavL[PC]) can be solved in polynomial time by Theorem
V.1, and we know that Eval(ITPG, NavL[PC]) is NP-complete by Theorem D.1. A
natural question then is whether the complexity remains the same if these
functionalities are combined. Notice that Eval(ITPG, NavL[PC,NOI]) is Pspace-
complete, so a positive answer to this question means a significant decrease
in the complexity of the query evaluation problem. Unfortunately, we show that
the complexity of the entire language does not decrease by restricting
numerical occurrence indicators to occur only in the axes.

######  Theorem D.2.

Eval(ITPG, NavL[PC,ANOI]) is Pspace-complete.

###### Proof.

Notice that every expression in ${\rm{\sf{\small NavL}}}{\rm[}{\rm{\sf{\small
PC}}},{\rm{\small{\sf ANOI}}}{\rm]}$ is also an expression in ${\rm{\sf{\small
NavL}}}{\rm[}{\rm{\sf{\small PC}}},{\rm{\sf{\small NOI}}}{\rm]}$, so Pspace-
membership follows immediately from Theorem V.1. Hence, we only need to prove
Pspace-hardness for ${\rm{\sf{\small NavL}}}{\rm[}{\rm{\sf{\small
PC}}},{\rm{\small{\sf ANOI}}}{\rm]}$.

To show this, we replace test expressions $r_{i}$ in the proof in Section C-D
by an expression in ${\rm{\sf{\small NavL}}}{\rm[}{\rm{\sf{\small
PC}}},{\rm{\small{\sf ANOI}}}{\rm]}$ that will be denoted by $q_{i}$.
Expression $q_{i}$ is defined in such a way that, for every time $t$, it holds
that $(v,t,v,t)\in\llbracket q_{i}\rrbracket_{C}$ if and only if
$(v,t,v,t)\in\llbracket r_{i}\rrbracket_{C}$, i.e., if and only if
$\textsf{bit}(i,t)$ is true, where $\textsf{bit}(i,t)$ holds if the $i$-th bit
of time $t$ (from right to left when written in its binary representation) is
1. More precisely, expression $q_{i}$ is defined as follow:

$\displaystyle q_{i}$ $\displaystyle=$
$\displaystyle?\left(\left((\mathbf{P}[0,0]+\mathbf{P}[2^{n},2^{n}])\ /\
\ldots\ /\ (\mathbf{P}[0,0]+\mathbf{P}[2^{i},2^{i}])\right)\ /\
\left(<2^{i}\wedge\neg<2^{i-1}\right)\right)$

Notice that the length of the representation $2^{k}$ is $k$, so the whole
expression $q_{i}$ has length $O(n^{2})$, which is polynomial with respect to
the size of $\psi$. Also, notice that as before, we only need a polynomial
number of these expressions for the reduction, and no further nesting of
numerical occurrence indicators is required for the proof. Hence, we only need
to prove that $(v,t,v,t)\in\llbracket q_{i}\rrbracket_{C}$ if and only if
$\textsf{bit}(i,t)$ is true. Recall that for this reduction, $C$ is an ITPG
consisting of only one node $v$, existing from time $0$ to time $2^{n}-1$,
with no edges or properties, so any temporal object considered will be of the
form $(v,t)$.

First, notice that $q_{i}$ is a path test, so $(v,t,v,t)\in\llbracket
q_{i}\rrbracket_{C}$ if and only if there exists a time point $t^{\prime}$
such that

$\displaystyle(v,t,v,t^{\prime})$ $\displaystyle\in$
$\displaystyle\llbracket\left((\mathbf{P}[0,0]+\mathbf{P}[2^{n},2^{n}])\ /\
\ldots\ /\ (\mathbf{P}[0,0]+\mathbf{P}[2^{i},2^{i}])\right)\ /\
\left(<2^{i}\wedge\neg<2^{i-1}\right)\rrbracket_{C}$

As in Step 1 of Section C-D, since the last part of the expression is a test,
this is equivalent to the existence of a time point $t^{\prime}$ such that
$(v,t^{\prime})\models\left(<2^{i}\wedge\neg<2^{i-1}\right)$, i.e., the $i$-th
bit of $t^{\prime}$ is $1$ and

$\displaystyle(v,t,v,t^{\prime})$ $\displaystyle\in$
$\displaystyle\llbracket(\mathbf{P}[0,0]+\mathbf{P}[2^{n},2^{n}])\ /\ \ldots\
/\ (\mathbf{P}[0,0]+\mathbf{P}[2^{i},2^{i}])\rrbracket_{C}$ (8)

We now prove that $(v,t,v,t)\in\llbracket q_{i}\rrbracket_{C}$ if and only if
$\textsf{bit}(i,t)$ is true. To show direction ($\Leftarrow$), suppose that
$\textsf{bit}(i,t)$ is true. Notice then that
$(v,t_{1},v,t_{2})\in\llbracket(\mathbf{P}[0,0]+\mathbf{P}[2^{k},2^{k}])\rrbracket_{C}$,
if and only if $t_{2}=t_{1}$ or $t_{2}=t_{1}-2^{k}$. In particular, if the
$(k+1)$-th bit of $t_{1}$ is $1$, then $t_{2}=t_{1}-2^{k}$ has a binary
representation that is equal to that of $t_{1}$ except on the $(k+1)$-th bit,
and
$(v,t_{1},v,t_{2})\in\llbracket(\mathbf{P}[0,0]+\mathbf{P}[2^{k},2^{k}])\rrbracket_{C}$.
Similarly, if the $(k+1)$-th bit of $t_{1}$ is $0$, then $t_{2}=t_{1}$ has a
binary representation that is equal to that of $t_{1}$, and also
$(v,t_{1},v,t_{2})\in\llbracket(\mathbf{P}[0,0]+\mathbf{P}[2^{k},2^{k}])\rrbracket_{C}$.
As in Section C-D, given $b\in\\{\textit{true},\textit{false}\\}$, let
$\mathbbm{1}_{b}$ be $1$ if $b=\textit{true}$, and be $0$ otherwise. Moreover,
define the sequence of time points $t_{n+1},\dots,t_{i}$ such that $t_{n+1}=t$
and $t_{k}=t_{k+1}-\mathbbm{1}_{\textsf{bit}(k+1,t)}\cdot 2^{k}$ for
$k\in\\{i,\dots,n\\}$. Then for every $k\in\\{i,\dots,n\\}$, it holds that
$(v,t_{k},v,t_{k+1})\in\llbracket(\mathbf{P}[0,0]+\mathbf{P}[2^{k},2^{k}])\rrbracket_{C}$,
and in particular,
$t^{\prime}=t-\sum_{k=i}^{n}\mathbbm{1}_{\textsf{bit}(k+1,t)}\cdot 2^{k}$
satisfies (8). Therefore, if the $i$-th bit of $t$ is $1$, then the $i$-th bit
of $t^{\prime}$ will be 1 as well. Hence, given $\textsf{bit}(i,t)$ is true,
we conclude that $(v,t,v,t)\in\llbracket q_{i}\rrbracket_{C}$, since for
$t^{\prime}=t-\sum_{k=i}^{n}\mathbbm{1}_{\textsf{bit}(k+1,t)}\cdot 2^{k}$,
equation (8) holds and $(v,t^{\prime})\models(<2^{i}\wedge\neg<2^{i-1})$.

To show direction ($\Rightarrow$), suppose that $(v,t,v,t)\in\llbracket
q_{i}\rrbracket_{C}$. Then there exists a time point $t^{\prime}$ such that
(8) holds, which only holds if there exists a sequence of time points
$t_{n+1},\dots,t_{i}$ where $t_{n+1}=t$ and either $t_{k}=t_{k+1}$ or
$t_{k}=t_{k+1}-2^{k}$ for $k\in\\{i,\dots,n\\}$, and $t_{i}=t^{\prime}$.
Notice that for such values for $k$, $2^{k}$ is a multiple of $2^{i}$, so
$t^{\prime}=t+d\cdot 2^{i}$ for some integer $d$. We conclude that the $i$-th
bit of $t$ is equal to $1$ if and only if the $i$-th bit of $t^{\prime}$ is
equal to $1$. Moreover, $(v,t^{\prime})\models(<2^{i}\wedge\neg<2^{i-1})$, so
the $i$-th bit of $t^{\prime}$ is indeed equal to $1$, so $\textsf{bit}(i,t)$
must be equal to true.

From the previous paragraphs, we conclude that $(v,t,v,t)\in\llbracket
q_{i}\rrbracket_{C}$ if and only if $\textsf{bit}(i,t)$ is true. Hence, by
replacing $r_{i}$ with $q_{i}$ in the proof of Section C-D, we deduce that
${\rm{\sf{\small NavL}}}{\rm[}{\rm{\sf{\small PC}}},{\rm{\small{\sf
ANOI}}}{\rm]}$ is also Pspace-hard, which was to be shown. ∎

##  Appendix E Supplementary Experimental Result

In section VII-A we discussed the impact of TGraphs size on query execution,
and pointed out that the trends presented in Figure 2 can be explained by the
size of output. To study this, we computed the increase in output size for
graphs G2-G6 (with between 2,000 and 10,000 nodes, as summarized in Table I)
relative to the size of the output for G1 (with 1,000 nodes), for each query.
Figures 7 (a) and (b) show this result. In these figures, the $x$-axis shows
the number of nodes in each graph, and the $y$-axis shows the relative size of
output bindings table, in comparison to the output of the same query over G1.
Similarly to Figure 2, it can be observed that the output size for all queries
except Q5, Q9, Q10, Q11, and Q12 follows a linear trend. For Q5, Q9, Q10, Q11
and Q12, the output size increases quadratically.

Figures 7 (c) gives another presentation of these results. Here, in addition
to computing the output size relative to G1 for each query (shown on the
$y$-axis), we also computed the execution time relative to G1 (shown on the
$x$-axis). This plot show that relative query execution time and relative
increase in output size are highly correlated for all queries, and for the
majority of our queries we have perfect correlation.

Figure 7: Relationship between input size, output size, and query execution
time for all queries. Execution time and output size are computed for graphs
G2-G6 (with between 2,000 and 10,000 nodes) in Table I, in proportion to these
quantities for graph G1 (with 1,000 nodes).