$\begin{array}[]{rl}mZ_{{\sf md}(\varphi)}s([m])&\text{if }d(m)\leq
d(\Delta_{i})\\\ mZ_{\max({\sf
md}(\varphi)-(d(\Delta_{i})-d(m)),0)}s([m])&\text{if
}d(m)>d(\Delta_{i}).\end{array}$

We claim

$(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})}^{IT},\Delta_{i}\leftrightarroweq_{{\sf
md}(\varphi)}(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})}^{FT},s([\Delta_{i}]),$

therefore (by Propositions 2.2 and 4.13),
$(\mathcal{M}_{\Gamma})_{\upharpoonright({\sf
md}(\varphi),\mathsf{Nom}(\varphi)\cup\\{i\\})}^{FT},s([\Delta_{i}])\models\varphi$.

As a consequence we get:

######  Theorem 4.18.

$\text{HXPath}_{=}$ on trees has the bounded model property.

The model constructed in Definition 4.17 has size at most exponential in the
input formula. Moreover, the algorithm below shows that model checking for
$\text{HXPath}_{=}$ can be solved in polynomial time. Thus, for a given
formula we can guess a model of exponential size and do model checking in
polynomial time, solving the problem in NExpSpace (which coincides with the
class ExpSpace).

Let $\mathcal{M}=\langle M,$
$\\{\sim_{e}\\}_{e\in\mathsf{Eq}},\\{R_{\mathsf{a}}\\}_{\mathsf{a}\in\mathsf{Mod}},\mathit{V},\mathit{nom}\rangle$
be a model and $\varphi$ a formula in $\text{HXPath}_{=}$, let
$e_{1},\ldots,e_{n}$ be an enumeration, ordered by size, of the subexpressions
of $\varphi$. Define the functions $\textit{Label}_{ne}$ and
$\textit{Label}_{pe}$ inductively as follows. Initially, set
$\textit{Label}_{ne}(m)$ = $\textit{Label}_{pe}(m_{1},m_{2})=\\{\\}$ for any
$m$, $m_{1}$, $m_{2}$. Then extend these labeling functions using the
following rules.

  1. (1)

$e_{i}=\mathsf{a}\in\mathsf{Mod}$:
$\textit{add}(\textit{Label}_{pe}(m_{1},m_{2}),a)$ iff
$R_{\mathsf{a}}(m_{1},m_{2})$.

  2. (2)

$e_{i}=@_{i}$: $\textit{add}(\textit{Label}_{pe}(m_{1},m_{2}),@_{i})$ iff
$m_{2}=\mathit{nom}(i)$.

  3. (3)

$e_{i}=[\psi]$: $\textit{add}(\textit{Label}_{pe}(m,m),[\psi])$ iff
$m\in\textit{Label}_{ne}(\psi)$.

  4. (4)

$e_{i}=\mathsf{a}\alpha$:
$\textit{add}(\textit{Label}_{pe}(m_{1},m_{2}),\mathsf{a}\alpha)$ iff there is
$m_{3}$ s.t. $R_{\mathsf{a}}(m_{1},m_{3})$ and
$\alpha\in\textit{Label}_{pe}(m_{3},m_{2})$.

  5. (5)

$e_{i}=@_{i}\alpha$:
$\textit{add}(\textit{Label}_{pe}(m_{1},m_{2})@_{i}\alpha)$ iff
$\alpha\in\textit{Label}_{pe}(\mathit{nom}(i),m_{2})$.

  6. (6)

$e_{i}=[\psi]\alpha$:
$\textit{add}(\textit{Label}_{pe}(m_{1},m_{2}),[\psi]\alpha)$ iff
$\psi\in\textit{Label}_{ne}(m_{1})$ and
$\alpha\in\textit{Label}_{pe}(m_{1},m_{2})$.

  7. (7)

$e_{i}=p\in$: $\textit{add}(\textit{Label}_{ne}(m),p)$ iff $p\in V(m)$.

  8. (8)

$e_{i}=i\in\mathsf{Nom}$: $\textit{add}(\textit{Label}_{ne}(m),i)$ iff
$m=\mathit{nom}(i)$.

  9. (9)

$e_{i}=\neg\psi$: $\textit{add}(\textit{Label}_{ne}(m),\neg\psi)$ iff
$\psi\not\in\textit{Label}_{ne}(m)$.

  10. (10)

$e_{i}=\psi_{1}\wedge\psi_{2}$:
$\textit{add}(\textit{Label}_{ne}(m),\psi_{1}\wedge\psi_{2})$ iff
$\psi_{1},\psi_{2}\in\textit{Label}_{ne}(m)$.

  11. (11)

$e_{i}=\langle\alpha_{1}=_{e}\alpha_{2}\rangle$:
$\textit{add}(\textit{Label}_{ne}(m),\langle\alpha_{1}=_{e}\alpha_{2}\rangle)$
iff there are $m_{1},m_{2}$ s.t. $\alpha_{1}\in\textit{Label}_{pe}(m,m_{1})$,
$\alpha_{2}\in\textit{Label}_{pe}(m,m_{2})$ and $m_{1}\sim_{e}m_{2}$.

  12. (12)

$e_{i}=\langle\alpha_{1}\not=_{e}\alpha_{2}\rangle$:
$\textit{add}(\textit{Label}_{ne}(m),\langle\alpha_{1}\not=_{e}\alpha_{2}\rangle)$
iff there are $m_{1},m_{2}$ s.t. $\alpha_{1}\in\textit{Label}_{pe}(m,m_{1})$,
$\alpha_{2}\in\textit{Label}_{pe}(m,m_{2})$ and it is not the case that
$m_{1}\sim_{e}m_{2}$.

As a result we obtain the following upper bound for
$\text{HXPath}_{=}$-satisfiability in $\mathfrak{C}_{tree}$.

######  Corollary 4.19.

The satisfiability problem for $\text{HXPath}_{=}$ on trees is decidable in
ExpSpace.

##  5\. Decidability via Filtrations

In the previous section we already obtained decidability for
$\text{HXPath}_{=}$ on trees. In this section we introduce _filtrations_ , a
notion which will help us to establish a bounded finite model property and an
upper bound for the complexity of satisfiability for
$\text{HXPath}_{=}(\shortminus)$333In [AFS17] it has been proved that the
satisfiability problem for $\text{HXPath}_{=}$ with a single accessibility
relation and a single data relation is PSpace-complete. However, for multiple
relations the exact complexity is unknown. over the class of all abstract
hybrid data models. Recall that $\text{HXPath}_{=}(\shortminus)$ is the
extension of $\text{HXPath}_{=}$ with inverse modalities.

In Section 2 we introduced path expressions of the form $\alpha\cup\beta$ as
an abbreviation, but this definition potentially leads to an exponential blow
up in the size of the formula. In this section we will consider $\cup$ as part
of the language of $\text{HXPath}_{=}(\shortminus)$ to avoid this blow up.

######  Definition 5.1.

Let $\Sigma$ be a set of formulas of $\text{HXPath}_{=}$. We say that $\Sigma$
is closed if:

  * •

$\neg\varphi\in\Sigma$ implies $\varphi\in\Sigma$

  * •

$\varphi\wedge\psi\in\Sigma$ implies $\varphi,\psi\in\Sigma$

  * •

$\langle\alpha*\beta\rangle\in\Sigma$ implies
$\langle\alpha\rangle\top,\langle\beta\rangle\top\in\Sigma$

  * •

$\langle[\varphi]\rangle\top\in\Sigma$ implies $\varphi\in\Sigma$

  * •

$\langle@_{i}\rangle\top\in\Sigma$ implies $i\in\Sigma$

  * •

$\langle\alpha\beta\rangle\top\in\Sigma$ implies
$\langle\alpha\rangle\top,\langle\beta\rangle\top\in\Sigma$

  * •

$\langle\alpha\cup\beta\rangle\top\in\Sigma$ implies
$\langle\alpha\rangle\top,\langle\beta\rangle\top\in\Sigma$.

######  Definition 5.2.

Let $\Sigma$ be a closed set of formulas, and $\mathcal{M}$ be an abstract
hybrid data model with $m,n$ states in $\mathcal{M}$. We define
$m\leftrightsquigarrow_{\Sigma}n$ if and only if for all $\varphi\in\Sigma$
($\mathcal{M},m\models\varphi$ iff $\mathcal{M},n\models\varphi$).

Now let us introduce filtration, the construction that will help us to obtain
a _small model property_ and give us decidability.

######  Definition 5.3 (Filtrations).

Let $\mathcal{M}=\langle
M,\\{\sim_{e}\\}_{e\in\mathsf{Eq}},\\{R_{\mathsf{a}}\\}_{\mathsf{a}\in\mathsf{Mod}},\mathit{V},\mathit{nom}\rangle$,
be an abstract hybrid data model, and $\Sigma$ a closed set of formulas. A
filtration of $\mathcal{M}$ via $\Sigma$ is any $\mathcal{M}^{f}=\langle
M^{f},\\{\sim^{f}_{e}\\}_{e\in\mathsf{Eq}},\\{R^{f}_{\mathsf{a}}\\}_{\mathsf{a}\in\mathsf{Mod}},\mathit{V}^{f},\mathit{nom}^{f}\rangle$,
such that

  * •

$M^{f}=M_{/\leftrightsquigarrow_{\Sigma}}$

  * •

If $mR_{\mathsf{a}}n$ then $[m]R^{f}_{\mathsf{a}}[n]$

  * •

If $[m]R_{\mathsf{a}}^{f}[n]$ then for all
$\langle\mathsf{a}\rangle\top\in\Sigma$, for all $m^{\prime}\in[m]$ there
exists $n^{\prime}\in[n]$ such that
$\mathcal{M},m^{\prime},n^{\prime}\models\mathsf{a}$

  * •

$[m]\sim_{e}^{f}[n]$ iff $m\sim_{e}n$

  * •

$\mathit{nom}^{f}(i)=[\mathit{nom}(i)]$

  * •

$\mathit{V}^{f}([m])=\\{p\mid p\in\mathit{V}(m)\\}$.

The _smallest filtration_ is a filtration that satisfies

$[m]R_{\mathsf{a}}^{f}[n]\text{ iff there exist
}m^{\prime}\in[m],n^{\prime}\in[n]\text{ such that
}m^{\prime}R_{\mathsf{a}}n^{\prime}.$

######  Theorem 5.3.

Let $\mathcal{M}$ be an abstract hybrid data model and $\mathcal{M}^{f}$ a
filtration of $\mathcal{M}$ for a closed set $\Sigma$. Then

  1. (1)

For all $\varphi\in\Sigma$, for all $m\in\mathcal{M}$,
$\mathcal{M}^{f},[m]\models\varphi$ iff $\mathcal{M},m\models\varphi$, and

  2. (2)

For all $\langle\alpha\rangle\top\in\Sigma$, for all $m,n\in\mathcal{M}$,
$\mathcal{M}^{f},[m],[n]\models\alpha$ iff for all $m^{\prime}\in[m]$ there
exists $n^{\prime}\in[n]$ such that
$\mathcal{M},m^{\prime},n^{\prime}\models\alpha$.

######  Proof 5.4.

By structural induction. First we prove $1$. The base and Boolean cases are
simple. Let us consider $\langle\alpha=_{e}\beta\rangle\in\Sigma$.
$\mathcal{M}^{f},[m]\models\langle\alpha=_{e}\beta\rangle$ iff there are
$[n],[u]$ such that

  1. (1)

$\mathcal{M}^{f},[m],[n]\models\alpha$ iff (by IH and
$\langle\alpha\rangle\top\in\Sigma$) there exist
$m^{\prime}\in[m],n^{\prime}\in[n]$ such that
$\mathcal{M},m^{\prime},n^{\prime}\models\alpha$,

  2. (2)

$\mathcal{M}^{f},[m],[u]\models\beta$ iff (by IH and
$\langle\beta\rangle\top\in\Sigma$) there exist
$m^{\prime\prime}\in[m],u^{\prime}\in[u]$ such that
$\mathcal{M},m^{\prime\prime},u^{\prime}\models\beta$, and

  3. (3)

$[n]\sim_{e}^{f}[u]$ iff (definition of $\mathcal{M}^{f}$) $n\sim_{e}u$. Since
$[n]=[n]^{\prime}$ and $[u]=[u]^{\prime}$ we have
$n^{\prime}\sim_{e}u^{\prime}$.

Notice that the problem is that $m^{\prime}$ might be different from
$m^{\prime\prime}$. Suppose for contradiction that
$\mathcal{M},m^{\prime},u^{\prime}\not\models\beta$. Since
$\langle\beta\rangle\top\in\Sigma$, $m^{\prime}\in[m]$, and
$u^{\prime}\in[u]$, by using $(ii)$ above we get
$\mathcal{M}^{f},[m],[u]\not\models\beta$, which is a contradiction.
Therefore, $\mathcal{M},m^{\prime}\models\langle\alpha=_{e}\beta\rangle$. The
case for $\langle\alpha\neq_{e}\beta\rangle$ is similar.

Now let us prove $2$:

\- Case $\langle[\varphi]\rangle\top\in\Sigma$. For the left to the right
direction, suppose $\mathcal{M}^{f},[m],[n]\models[\varphi]$, iff $[m]=[n]$
and $\mathcal{M}^{f},[m]\models\varphi$. By $1$ we have
$\mathcal{M},m\models\varphi$, then by definition of $[m]$,
$\mathcal{M},m^{\prime}\models\varphi$, for all $m^{\prime}\in[m]$. Hence
$\mathcal{M},m^{\prime},m^{\prime}\models[\varphi]$ as wanted, since
$m^{\prime}\in[n]$.

For the other direction, suppose that for all $m^{\prime}\in[m]$ there exists
$n^{\prime}\in[n]$ s.t. $\mathcal{M},m^{\prime},n^{\prime}\models[\varphi]$.
Then $m^{\prime}=n^{\prime}$ and $\mathcal{M},m^{\prime}\models\varphi$. By
$1$, $\mathcal{M}^{f},[m^{\prime}]\models\varphi$, and since
$[m]=[m^{\prime}]$, $\mathcal{M}^{f},[m]\models\varphi$. Therefore
$\mathcal{M}^{f},[m],[n]\models[\varphi]$, because $n^{\prime}=m^{\prime}$
implies $[n]=[n^{\prime}]=[m^{\prime}]=[m]$.

\- Case $\langle@_{i}\rangle\top\in\Sigma$. For the left to the right
direction suppose $\mathcal{M}^{f},[m],[n]\models@_{i}$, iff
$\mathit{nom}^{f}(i)=[n]$. By definition of $\mathit{nom}^{f}$, we have
$\mathit{nom}^{f}(i)=[\mathit{nom}(i)]$, then $\mathit{nom}(i)=n$. Hence
$\mathcal{M},m,n\models@_{i}$.

For the other direction, suppose that for all $m^{\prime}\in[m]$ there exists
$n^{\prime}\in[n]$ s.t. $\mathcal{M},m^{\prime},n^{\prime}\models@_{i}$, iff
$\mathit{nom}(i)=n^{\prime}$. Then $[n^{\prime}]=\\{n^{\prime}\\}=[n]$,
therefore $\mathcal{M}^{f},[m],[n]\models@_{i}$.

\- Case $\langle\mathsf{a}\rangle\top\in\Sigma$. For the left to the right
direction suppose $\mathcal{M}^{f},[m],[n]\models\mathsf{a}$, iff
$[m]R_{\mathsf{a}}^{f}[n]$. Then, since
$\langle\mathsf{a}\rangle\top\in\Sigma$, for all $m^{\prime}\in[m]$ there
exists $n^{\prime}\in[n]$ s.t.
$\mathcal{M},m^{\prime},n^{\prime}\models\mathsf{a}$ (by the second condition
on the definition of $R_{\mathsf{a}}^{f}$), as wanted.

For the right to the left direction, suppose for all $m^{\prime}\in[m]$ there
exists $n^{\prime}\in[n]$ s.t.
$\mathcal{M},m^{\prime},n^{\prime}\models\mathsf{a}$. Then
$m^{\prime}R_{\mathsf{a}}n^{\prime}$, and by the first condition of the
definition of $R_{\mathsf{a}}^{f}$ we have
$[m^{\prime}]R_{\mathsf{a}}^{f}[n]$, iff $[m]R_{\mathsf{a}}^{f}[n]$. Hence,
$\mathcal{M}^{f},[m],[n]\models\mathsf{a}$.

\- Case $\langle\alpha\beta\rangle\top\in\Sigma$. For the left to the right
direction suppose $\mathcal{M}^{f},[m],[n]\models\alpha\beta$, iff there
exists $[z]$ such that $\mathcal{M}^{f},[m],[z]\models\beta$ and
$\mathcal{M}^{f},[z],[n]\models\alpha\beta$. By IH, for all $m^{\prime}\in[m]$
there exists $z^{\prime}\in[z]$ s.t.
$\mathcal{M},m^{\prime},z^{\prime}\models\alpha$ and for all
$z^{\prime}\in[z]$ there exists $n^{\prime}\in[n]$ s.t.
$\mathcal{M},z^{\prime},n^{\prime}\models\beta$. This implies that for all
$m^{\prime}\in[m]$ there exists $n^{\prime}\in[n]$ s.t.
$\mathcal{M},m^{\prime},n^{\prime}\models\alpha\beta$.

For the other direction, suppose for all $m^{\prime}\in[m]$ there exists
$n^{\prime}\in[n]$ s.t. $\mathcal{M},m^{\prime},n^{\prime}\models\alpha\beta$.
Then there exists $z^{\prime}$ s.t.
$\mathcal{M},m^{\prime},z^{\prime}\models\alpha$ and
$\mathcal{M},z^{\prime},n^{\prime}\models\beta$. By IH we have
$\mathcal{M}^{f},[m],[z^{\prime}]\models\alpha$ and
$\mathcal{M}^{f},[z^{\prime}],[n]\models\beta$. Hence
$\mathcal{M}^{f},[m],[n]\models\alpha\beta$.

\- Case $\langle\alpha\cup\beta\rangle\top\in\Sigma$. For the left to the
right direction suppose $\mathcal{M}^{f},[m],[n]\models\alpha\cup\beta$, iff
$\mathcal{M}^{f},[m],[n]\models\alpha$ or
$\mathcal{M}^{f},[m],[n]\models\beta$. By IH, for all $m^{\prime}\in[m]$ there
exists $n^{\prime}\in[n]$ s.t.
$\mathcal{M},m^{\prime},n^{\prime}\models\alpha$ or
$\mathcal{M},m^{\prime},n^{\prime}\models\beta$. This implies that for all
$m^{\prime}\in[m]$ there exists $n^{\prime}\in[n]$ s.t.
$\mathcal{M},m^{\prime},n^{\prime}\models\alpha\cup\beta$.

For the other direction, suppose for all $m^{\prime}\in[m]$ there exists
$n^{\prime}\in[n]$ s.t.
$\mathcal{M},m^{\prime},n^{\prime}\models\alpha\cup\beta$, iff
$\mathcal{M},m^{\prime},n^{\prime}\models\alpha$ or
$\mathcal{M},m^{\prime},n^{\prime}\models\beta$. By IH we have
$\mathcal{M}^{f},[m],[n]\models\alpha$ or
$\mathcal{M}^{f},[m],[n]\models\beta$. Hence
$\mathcal{M}^{f},[m],[n]\models\alpha\cup\beta$.

As it happens for many modal logics the previous result gives us a bounded
model property for satisfiability: if a formula $\varphi$ is satisfiable it is
satisfiable in a model of size at most exponential in the size of $\varphi$.
Moreover, filtrations preserve some structural properties of the accessibility
relations. In particular the following is true:

######  Proposition 5.5.

Let $\mathcal{M}=\langle
M,\\{\sim_{e}\\}_{e\in\mathsf{Eq}},\\{\rightarrow_{a}\\}_{a\in\mathsf{Mod}},\mathit{V},\mathit{nom}\rangle$
be a model, and let $\mathcal{M}^{f}$ be the smallest filtration of
$\mathcal{M}$. Then, $\mathsf{a}=(\mathsf{a})^{-1}$ implies
$(\mathsf{a})^{f}=(\mathsf{a}^{f})^{-1}$

######  Proof 5.6.

Suppose that $\mathsf{a}=(\mathsf{a})^{-1}$. We want to prove that
$(\mathsf{a})^{f}=(\mathsf{a}^{f})^{-1}$. Then suppose
$[m]R_{\mathsf{a}}^{f}[n]$. Since $f$ is the smallest filtration, there exist
$m^{\prime}\in[m],n^{\prime}\in[n]$ such that
$m^{\prime}R_{\mathsf{a}}n^{\prime}$. But by hypothesis, we have
$n^{\prime}R_{\mathsf{a}}m^{\prime}$, and by definition of filtration we get
$[n^{\prime}]R_{\mathsf{a}}^{f}[m^{\prime}]$. Since $[m^{\prime}]=[m]$ and
$[n^{\prime}]=[n]$, we obtain $[n]R_{\mathsf{a}}^{f}[m]$.

As a result we obtain an upper bound for the complexity of satisfiability.

######  Corollary 5.7.

The satisfiability problem of $\text{HXPath}_{=}(\shortminus)$ is in NExpTime.

On the other hand, if we consider sibling navigation the argument does not
work. In the figure below we represent a relation $R_{\mathsf{a}}$ by black
arrows, and the sibling relation $R_{\mathsf{s}}$ by dotted arrows. Let
$\Sigma=\\{\langle\mathsf{a}\rangle\top\\}$. The model on the right is the
filtration by $\Sigma$ of the model on the left. As we can see, any filtration
collapses $v$ and $u$ into a unique equivalence class with a reflexive arrow,
but the sibling relation must be irreflexive. Hence the notion of filtration
we introduced is not appropriate to handle siblings.

$\mathcal{M}$$w$$v$$u$ |  $\mathcal{M}^{f}$$\\{w\\}$$\\{v,u\\}$
---|---

Finally, we show that filtration does not work for proving that the
satisfiability problem for $\text{HXPath}_{=}$ over $\mathfrak{C}_{tree}$ is
decidable. This is why, in order to show Corollary 4.19 we used a more
specialized method. Consider again
$\Sigma=\\{\langle\mathsf{a}\rangle\top\\}$. The model on the right is the
filtration by $\Sigma$ of the model on the left (assuming all nodes are equal
for the data relation). Any filtration collapses all nodes from $\mathcal{M}$
into a single reflexive node. Clearly,
$\mathcal{M}^{f}\notin\mathfrak{C}_{tree}$.

$\mathcal{M}$$\ldots$$w$ |  $\mathcal{M}^{f}$[$w$]
---|---

##  6\. Discussion

We introduced a sound and strongly complete axiomatization for
$\text{HXPath}_{=}$, i.e., the language XPath with forward navigation for
multiple accessibility relations; multiple equality/ inequality data
comparisons; and where node expressions are extended with nominals, and path
expressions are extended with the hybrid operator $@$. The hybridization of
XPath allowed us to apply a completeness argument similar to the one used for
the hybrid logic $\mathcal{HL}(@)$ shown in, e.g., [BtC06]. This ensures that
certain extensions of the axiomatic system we introduce are also strongly
complete. The axiomatic systems that can be obtained in this way cover a large
family of hybrid XPath languages over different classes of frames.

Our system extends the calculus introduced previously in [AF16]. The most
important improvement is that we provide a minimal system which can be
extended with axioms and rules of certain kind, such that strong completeness
immediately follows. The kind of axioms and rules we allow in the extensions
ensures completeness with respect to a large family of frame classes. We
showed interesting examples of such extensions. In particular, we obtain a
strongly complete axiomatization for the logic extended with backward and
sibling navigation, and for data equality inclusion.

One particularly interesting class of structures used in practice is the class
of _tree models_ , since the main applications of XPath in, e.g., web
semantics are related to XML documents. From a mathematical point of view, XML
documents are trees. In this respect, we investigate axiomatizations for
$\text{HXPath}_{=}$ on tree models. First, we showed that there is no finitary
first-order axiomatization which is strongly complete for $\text{HXPath}_{=}$
on trees. Then we discussed two alternatives for dealing with tree-like
structures. On the one hand, it is possible to relax some condition on the
models. We consider the class $\mathfrak{C}_{forest^{-}}$, which are forest-
like models but possibly with infinite chains with respect to the predecessor
relation. More precisely, we extend the basic axiom system with an infinite
set of pure axioms to strongly axiomatize the class
$\mathfrak{C}_{forest^{-}}$. Another alternative is giving up _strong_
completeness. We showed weak completeness for the class $\mathfrak{C}_{tree}$,
using pure axioms.

We also investigated the status of decidability for the satisfiability problem
of $\text{HXPath}_{=}$ and some extensions. We used a standard technique in
modal logics named _filtrations_ [BvB06]. The filtration method is a way to
build finite models by taking a large model and collapsing as many states as
possible. We replicate this technique for $\text{HXPath}_{=}(\shortminus)$,
and obtain a NExpTime upper bound for its satisfiability problem. We showed
that filtrations do not work on some extensions of $\text{HXPath}_{=}$. In
particular, for the case of tree models we proved that the satisfiability
problem is decidable in ExpSpace using a more specialized approach.

As future work, it would be interesting to investigate $\text{XPath}_{=}$
fragments with the reflexive-transitive path $\mathsf{a}^{*}$. One of the main
limitations of the framework we introduced in this paper is that it can only
axiomatize first-order languages. For that reason, transitive closure
operators cannot be accounted for, and a different proof strategy is needed.
We conjecture that it is possible to adapt the results from [HKT00] for
Propositional Dynamic Logic (PDL) to obtain a weakly complete axiom system for
$\text{HXPath}_{=}(*)$ (i.e., $\text{HXPath}_{=}$ extended with
$\mathsf{a}^{*}$) over the class of all models. However, for axiomatizing
$\text{HXPath}_{=}(*)$ over trees, the filtration technique used in [HKT00]
does not seem to work, and new developments are needed, as for other logics
with fix point operators over tree-like structures (see, e.g., the case of
${\rm CTL}^{*}$ in [Rey01]).

The exact computational complexity of the logics we considered has not been
investigated yet. It has been proved that $\text{XPath}_{=}$ with single
accessibility and data relations extended with hybrid operators is PSpace-
complete [AFS17]. Moreover, we provided upper bounds for multi-modal
$\text{HXPath}_{=}(\shortminus)$ over arbitrary models and for
$\text{HXPath}_{=}$ on trees, but without giving a tight lower bound. It would
be also interesting to investigate the complexity of the multi-modal languages
we studied in this article, enriched with backward and sibling navigation,
reflexive-transitive closures, and over the class of trees. We conjecture that
we can adapt the automata proof given in [Fig10], with the method used to
account for hybrid operators presented in [SV01] to get exact bounds.

#### Acknowledgments

We would like to thank the two anonymous reviewers for their helpful comments
and suggestions. This work is supported by projects ANPCyT-PICTs-2017-1130,
Stic-AmSud 20-STIC-03 ‘DyLo-MPC’, Secyt-UNC, GRFT Mincyt-Cba, and by the
Laboratoire International Associé SINFIN.

## References

  * [ABFF16] S. Abriola, P. Barceló, D. Figueira, and S. Figueira.  Bisimulations on data graphs.  In Principles of Knowledge Representation and Reasoning: Proceedings of the Fifteenth International Conference, KR, pages 309–318, 2016\.
  * [ABFF18] S. Abriola, P. Barceló, D. Figueira, and S. Figueira.  Bisimulations on data graphs.  Journal of Artificial Intelligence Research, 61:171–213, 2018.
  * [ABM01] C. Areces, P. Blackburn, and M. Marx.  Hybrid logics: characterization, interpolation and complexity.  The Journal of Symbolic Logic, 66(3):977–1010, 2001.
  * [ADF14] S. Abriola, M. Descotte, and S. Figueira.  Definability for downward and vertical XPath on data trees.  In 21th Workshop on Logic, Language, Information and Computation, volume 6642 of LNCS, pages 20–34, 2014.
  * [ADF17] S. Abriola, M. Descotte, and S. Figueira.  Model theory of xpath on data trees. part II: binary bisimulation and definability.  Information and Computation, 255:195–223, 2017.
  * [ADFF17] S. Abriola, M. E. Descotte, R. Fervari, and S. Figueira.  Axiomatizations for downward XPath on data trees.  Journal of Computer and System Sciences, 89:209–245, 2017.
  * [AF16] C. Areces and R. Fervari.  Hilbert-style axiomatization for hybrid XPath with data.  In L. Michael and A. Kakas, editors, Logics in Artificial Intelligence - 15th European Conference, JELIA 2016, Larnaca, Cyprus, November 9-11, 2016, Proceedings, volume 10021 of Lecture Notes in Computer Science, pages 34–48, 2016.
  * [AFL02] M. Arenas, W. Fan, and L. Libkin.  On verifying consistency of xml specifications.  In Proceedings of the Twenty-first ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS ’02, pages 259–270, New York, NY, USA, 2002. ACM.
  * [AFS17] C. Areces, R. Fervari, and N. Seiler.  Tableaux for hybrid XPath with data.  In E. Oliveira, J. Gama, Z. Vale, and H. Lopes Cardoso, editors, Progress in Artificial Intelligence - 18th EPIA Conference on Artificial Intelligence, EPIA 2017, Porto, Portugal, September 5-8, 2017, Proceedings, volume 10423 of Lecture Notes in Computer Science, pages 611–623. Springer, 2017.
  * [AG08] R. Angles and C. Gutiérrez.  Survey of graph database models.  ACM Comput. Surv., 40(1):1:1–1:39, 2008.
  * [BdRV01] P. Blackburn, M. de Rijke, and Y. Venema.  Modal Logic, volume 53 of Cambridge Tracts in Theoretical Computer Science.  Cambridge University Press, 2001.
  * [BFG08] M. Benedikt, W. Fan, and F. Geerts.  XPath satisfiability in the presence of DTDs.  Journal of the ACM, 55(2):1–79, 2008.
  * [BK08] M. Benedikt and C. Koch.  XPath leashed.  ACM Computing Surveys, 41(1), 2008.
  * [BLS16] D. Baelde, S. Lunel, and S. Schmitz.  A sequent calculus for a modal logic on finite data trees.  In 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, pages 32:1–32:16, 2016.
  * [BMSS09] M. Bojańczyk, A. Muscholl, T. Schwentick, and L. Segoufin.  Two-variable logic on data trees and XML reasoning.  Journal of the ACM, 56(3), 2009.
  * [Bra11] T. Brauner.  Hybrid Logic and Its Proof-Theory.  Springer, 2011.
  * [BtC06] P. Blackburn and B. ten Cate.  Pure extensions, proof rules, and hybrid axiomatics.  Studia Logica, 84(2):277–322, 2006.
  * [BvB06] P. Blackburn and J. van Benthem.  Modal Logic: A Semantic Perspective.  In Handbook of Modal Logic [BvBW06], pages 1–84.
  * [BvBW06] P. Blackburn, J. van Benthem, and F. Wolter.  Handbook of Modal Logic, Volume 3 (Studies in Logic and Practical Reasoning).  Elsevier Science Inc., New York, NY, USA, 2006.
  * [CD99] J. Clark and S. DeRose.  XML path language (XPath).  Website, 1999.  W3C Recommendation, url = http://www.w3.org/TR/xpath.
  * [End01] H. Enderton.  A Mathematical Introduction to Logic.  Academic Press, 2nd edition, 2001.
  * [FCG04] W. Fan, C. Chan, and M. Garofalakis.  Secure XML querying with security views.  In Proceedings of the 2004 ACM SIGMOD International Conference on Management of Data, pages 587–598. ACM, 2004.
  * [FFA14] D. Figueira, S. Figueira, and C. Areces.  Basic model theory of XPath on data trees.  In International Conference on Database Theory, pages 50–60, 2014\.
  * [FFA15] D. Figueira, S. Figueira, and C. Areces.  Model theory of XPath on data trees. Part I: Bisimulation and characterization.  Journal of Artificial Intelligence Research, 53:271–314, 2015.
  * [Fig10] D. Figueira.  Reasoning on Words and Trees with Data.  PhD thesis, Laboratoire Spécification et Vérification, ENS Cachan, France, 2010.
  * [Fig12] D. Figueira.  Decidability of downward XPath.  ACM Transactions on Computational Logic, 13(4):34, 2012.
  * [Fig18] D. Figueira.  Satisfiability of xpath on data trees.  ACM SIGLOG News, 5(2):4–16, 2018.
  * [Fin75] K. Fine.  Normal forms in modal logic.  Notre Dame Journal of Formal Logic, 16(2):229–237, 1975.
  * [FS11] D. Figueira and L. Segoufin.  Bottom-up automata on data trees and vertical XPath.  In 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011), pages 93–104, 2011.
  * [GKP05] G. Gottlob, C. Koch, and R. Pichler.  Efficient algorithms for processing XPath queries.  ACM Transactions on Database Systems, 30(2):444–491, 2005.
  * [Gol84] R. Goldblatt.  An abstract setting for Henkin proofs.  Topoi, 3(1):37–41, Jun 1984.
  * [HKT00] D. Harel, D. Kozen, and J. Tiuryn.  Dynamic Logic.  MIT Press, Cambridge, MA, 2000.
  * [KRV15] E. Kostylev, J. Reutter, and D. Vrgoč.  XPath for DL ontologies.  In Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, AAAI’15, pages 1525–1531. AAAI Press, 2015.
  * [LMV16] L. Libkin, W. Martens, and D. Vrgoč.  Querying graphs with data.  J. ACM, 63(2):14:1–14:53, 2016.
  * [LV12] L. Libkin and D. Vrgoč.  Regular path queries on graphs with data.  In International Conference on Database Theory, pages 74–85, 2012\.
  * [Mar04] M. Marx.  XPath with conditional axis relations.  In International Conference on Extending Database Technology (EDBT’04), volume 2992 of LNCS, pages 477–494. Springer, 2004.
  * [MdR05] M. Marx and M. de Rijke.  Semantic characterizations of navigational XPath.  ACM SIGMOD Record, 34(2):41–46, 2005.
  * [MN07] W. Martens and F. Neven.  Frontiers of tractability for typechecking simple xml transformations.  Journal of Computer and System Sciences, 73(3):362–390, 2007.
  * [Pra91] V. R. Pratt.  Dynamic algebras: Examples, constructions, applications.  Studia Logica, 50(3-4):571–605, 1991.
  * [Rey01] M. Reynolds.  An axiomatization of full computation tree logic.  The Journal of Symbolic Logic, 66(3):1011–1057, 2001.
  * [RWE13] I. Robinson, J. Webber, and E. Eifrem.  Graph Databases.  O’Reilly Media, Inc., 2013.
  * [SP10] L. Schröder and D. Pattinson.  Named models in coalgebraic hybrid logic.  In J.-Y. Marion and Th. Schwentick, editors, 27th International Symposium on Theoretical Aspects of Computer Science, STACS 2010, March 4-6, 2010, Nancy, France, volume 5 of LIPIcs, pages 645–656. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2010.
  * [SV01] U. Sattler and M. Vardi.  The hybrid mu-calculus.  In R. Goré, A. Leitsch, and T. Nipkow, editors, Proceedings of the International Joint Conference on Automated Reasoning, volume 2083 of LNAI, pages 76–91. Springer Verlag, 2001.
  * [tCLM10] B. ten Cate, T. Litak, and M. Marx.  Complete axiomatizations for XPath fragments.  Journal of Applied Logic, 8(2):153–172, 2010.
  * [tCM09] B. ten Cate and M. Marx.  Axiomatizing the logical core of XPath 2.0.  Theory of Computing Systems, 44(4):561–589, 2009.
  * [Wad00] P. Wadler.  A formal semantics of patterns in XSLT and XPath.  Markup Languages, 2(2):183–202, 2000.
  * [Wor02] World Wide Web Consortium.  XQuery 1.0 and XPath 2.0 formal semantics. W3C working draft.  Technical report, 2002.  http://www.w3c.org/TR/query-algebra.