text:
\section{Backwards propagation}
\label{se:backwards-app}\label{app:backward}

Here we give the exact formulation of the backwards propagation lemma
and prove it.

It is convenient to consider a program $\overline{S}$, which behaves like $S$, except that it does not abort.
$\overline{S}$ uses a fresh variable $abo$ to indicate whether $S$ aborts.
 The command $abo := \mathbf{F}$ is added at the beginning of the code.
 Every command $C$ of the form $var_1 := var_2.f$, $var_2.f := var_1$ or $dispose(var_2)$ is replaced with $\overline{C} = if\,\, var_2\,\, =\,\, \mathrm{null}\,\, then\,\, abo := \mathbf{T}\,\, else\,\, C\,\, fi$.
 For $if$, $assume$ and assignments of the form $var_1.f_1 := var_2.f_2$ commands the case is similar, except that there may be two evaluations
of the form $var_i.f_j$, which need to be reflected in the condition in $\overline{C}$.
By the construction of $\overline{S}$, $\overline{S}$ has the following properties:
\begin{enumerate}
 \item The run of $\mathcal{M}_1$ on $\overline{S}$ does not abort for any $\mathcal{M}_1$.
 \item $abo$ has the value $\mathbf{T}$ at the end of the run of $\overline{S}$ on $\mathcal{M}_1$
if and only if $S$ aborts on $\mathcal{M}_1$.
 \item If $\left\langle S,\mathcal{M}_1\right\rangle\leadsto \mathcal{M}_2$, then $\left\langle \overline{S},\mathcal{M}_1\right\rangle\leadsto \mathcal{M}_2$.
\end{enumerate}

We need a further extension of our structures, which uses a refined $\leadsto$ relation.
The refined $\leadsto$ relation will get rid of some non-determinism in the semantics of the programming language.

Given a finite set $Y$ of labels and a tuple $\bar{d}_Y=(d_y: y\in Y)$ of elements of $M$,
we denote by $\left\langle \mathcal{M}_1, (\bar{R}^{ext})^{\mathcal{M}_1}, \bar{d}_Y \right\rangle$
the structure obtained from $\left\langle \mathcal{M}_1, (\bar{R}^{ext})^{\mathcal{M}_1}\right\rangle$ by adding the constants $d_y$ for each $y\in Y$.
The vocabulary $\tau_{Y}^{ext}$ of $\left\langle \mathcal{M}_1, (\bar{R}^{ext})^{\mathcal{M}_1}, \bar{d}_Y \right\rangle$ extends
$\tau^{ext}$ by constant symbols $\{o_y: y\in Y\}$.

Given a loopless program $S'$, we assign unique labels $y$ to the commands of $S'$.
For any loopless program $S'$, we denote by $Y_{S'}$ the set of labels of commands in $S'$.
The $\leadsto_{{\bar{d}_{Y_S'}}}$ relation is obtained from the $\leadsto$ relation as follows:\\
$\left\langle S',\mathcal{M}_1\right\rangle\leadsto_{\bar{d}_{Y_{S'}}}  \mathcal{M}_2$ iff $\left\langle S',\mathcal{M}_1\right\rangle\leadsto \mathcal{M}_2$, except in the three following cases
for $S'$:
\begin{itemize}
 \item[--] $y: var_1 := var_2.f$: $\left\langle S',\mathcal{M}_1\right\rangle\leadsto_{d_y}  \mathcal{M}_2$ iff
 $\left\langle S',\mathcal{M}_1\right\rangle\leadsto  \mathcal{M}_2$ and  $f^{\mathcal{M}_1}(o_{var_2}^{\mathcal{M}_1})=d_y$.
           Else, $\left\langle S',\mathcal{M}_1\right\rangle\leadsto_{d_y} \mbox{abort}$.
 \item[--] $y: var:=new$: $\left\langle S',\mathcal{M}_1\right\rangle\leadsto_{d_y}  \mathcal{M}_2$ iff
 $\left\langle S',\mathcal{M}_1\right\rangle\leadsto  \mathcal{M}_2$ and  $o_{var}^{\mathcal{M}_2}=d_y$.
           Otherwise, $\left\langle S',\mathcal{M}_1\right\rangle\leadsto_{d_y} \mbox{abort}$.
 \item[--] $S'_1; S'_2$: If $\left\langle S'_1,\mathcal{M}_1\right\rangle\leadsto_{\bar{d}_{Y_{S'_1}}}  \mathcal{M}'$ and
$\left\langle S'_2,\mathcal{M}'\right\rangle\leadsto_{\bar{d}_{Y_{S'_2}}}  \mathcal{M}_2$,
then $\left\langle S'_1;S'_2,\mathcal{M}_1\right\rangle\leadsto_{\bar{d}_{Y_{S'_1}}\cup\bar{d}_{Y_{S'_2}}}  \mathcal{M}_2$.
\end{itemize}
The main observation is:
\begin{lemma}
For any two memory structures $\mathcal{M}_1$ and $\mathcal{M}_2$,
$\left\langle S',\mathcal{M}_1\right\rangle\leadsto \mathcal{M}_2$ iff there exists a tuple $\bar{d}_{Y_S'}$ such that
$\left\langle S',\mathcal{M}_1\right\rangle\leadsto_{\bar{d}_{Y_S'}}  \mathcal{M}_2$ .
\end{lemma}

We are now ready to state Lemma \ref{lem:backwards--} precisely:
\begin{lemma}\label{lem:backwards-app} \label{se:backwards-ghost-app}
Let $S$ be a loopless program, $Y_{\overline{S}}$ be the set of labels of commands in $\overline{S}$,
$\mathcal{M}_1$ and $\mathcal{M}_2$ be  memory structures, $\bar{d}_{Y_{\overline{S}}}$ be a tuple of $M$ elements
labeled with the labels in $Y_{\overline{S}}$, $d_{abo}\in M$, and
 $\varphi$ be an $\mathcal{ALCQIO}_{b,Re}$-formula over $\tau$.
\begin{enumerate}
 \item If $\left\langle S, \mathcal{M}_1\right\rangle \leadsto_{\bar{d}_{Y_{\overline{S}}}} \mathcal{M}_2$,
 then:\\
 $\mathcal{M}_2\models \varphi$ iff
$\left\langle \mathcal{M}_1, (\bar{R}^{ext})^{\mathcal{M}_1}, \bar{d}_{Y_{\overline{S}}}, d_{abo} \right\rangle \models \Theta_{S}(\varphi)$.
\item If $\left\langle S, \mathcal{M}_1\right\rangle\leadsto_{\bar{d}_{Y_{\overline{S}}}}  \mbox{abort}$, then
  for every tuple $\bar{d}_{Y_{\overline{S}}}$ of $M$ elements,
$\left\langle \mathcal{M}_1, (\bar{R}^{ext})^{\mathcal{M}_1},
\bar{d}_{Y_{\overline{S}}},d_{abo} \right\rangle \not\models \Theta_{S}(\varphi)$.
\end{enumerate}
The vocabulary of the structure $\left\langle \mathcal{M}_1, (\bar{R}^{ext})^{\mathcal{M}_1}, \bar{d}_{Y_{\overline{S}}}, d_{abo} \right\rangle$ is
$\tau^{ext}_{Y_{\overline{S}}} \cup\{o_{abo}\}$.

The definition of $\Theta_S$ is:
\begin{definition}$\Theta_{S}(\varphi)=\Phi_{\overline{S}}(\varphi\land (o_{abo} \equiv o_\mathbf{F})))$,
$\Phi$ is obtained from $\Psi$ by
substituting every  symbol $R\in\tau^{rem}$ in $\varphi$ by $R^{ext}$, and
$\Psi$ is defined as:
\[\begin{array}{lll}
\Psi_{skip}(\varphi) &=&\varphi\\
\Psi_{var_{1}:=e}(\varphi)&=&\varphi[{o_{var_{1}} /  o_{e}}],\, e=var_{2}\mbox{ or }e=\mathrm{null}\\
\Psi_{y: var_{1}:=var_{2}.f}(\varphi)&=&\varphi[o_{var_{1}} / o_y] \land (\exists f^{-}.o_{var_{2}}\equiv o_y)\\
\Psi_{var_{1}.f:=e}(\varphi)&=&\varphi[f / f\backslash(o_{var_{1}}\times\top)\cup(o_{var_{1}},o_{e})],\, \\
&&\mbox{where }e=var_{2}\mbox{ or }e=\mathrm{null}\\
\Psi_{if\,\, b\,\, then\,\,  S_{1}\,\, else\,\, S_{2}\,\, fi}
(\varphi)&=&\varepsilon_{b}\land\Psi_{S_{1}}(\varphi)\lor\neg\varepsilon_{b}\land\Psi_{S_{2}}(\varphi)\\
\Psi_{y:var:=new}(\varphi)&=&\varphi[o_{var} /  o_{y}][Alloc / Alloc\sqcup o_{y}] \\
&&\land o_y\sqsubseteq \neg Alloc\\
\Psi_{dispose(var)}(\varphi)&=&\Psi_{S_{disp}}(\varphi[Alloc / Alloc\sqcap\neg o_{var}]),\\
&&\mbox{where }S_{disp}=var.f_{k_1} := \mathrm{null}; \\
 && \cdots;  var.f_{k_w} := \mathrm{null}\\
\Psi_{S_{1};S_{2}}(\varphi)&=&\Psi_{S_{1}}(\Psi_{S_{2}}(\varphi)) \
\end{array}
\]
The notation $\varphi[A / B]$ should be interpreted as
the syntactic replacement of any occurrence of $A$ with $B$.
We write e.g. $y: var:= new$ to indicate that the command $var := new$ is labeled with $y$.
$\varepsilon_{b}$ is defined inductively:
for
$e_{1}=e_{2}$ we set $\varepsilon_{b}=(A_{e_{1}}\equiv A_{e_{2}})$,
with $A_{var}=o_{var}$ and $A_{var.f}=\exists f^{-}.o_{var}$; $\varepsilon$
extends naturally to the Boolean connectives.
In the definition of $\Psi_{dispose(var)}$, $f_{k_1},\ldots,f_{k_w}$ are the members of $\tau_{\mathrm{fields}}$ which
occur in $\varphi$. W.l.o.g. we assume that $S$ does not contain commands of the form $if\,\,b\,\,then\,\,S_1\,\, fi$
or $var_1.f_1 := var_2.f_2$, since they can be expressed using the other commands.
\end{definition}
\end{lemma}

To prove Lemma \ref{lem:backwards-app} we need the following lemma:

\begin{lemma}\label{lem:backwards2-app}
Let $S$ be a loopless program without $assume$ commands, $Y_S$ be the set of labels of commands in $S$,
$Y$ be a set of labels disjoint from $Y_S$,
$\mathcal{M}_1$ and $\mathcal{M}_2$ be memory structures with universe $M$
and $\bar{d}_{Y_S}$ a tuple of $M$ elements
such that
$\left\langle S, \mathcal{M}_1\right\rangle\leadsto_{\bar{d}_{Y_S}} \mathcal{M}_2$.
Let $\bar{d}_Y$ be a tuple of $M$ elements and
 $\varphi$ be an $\mathcal{ALCQIO}_{b,Re}$-formula over $\tau\cup\{o_{y}: y\in Y\}$.
$\left\langle \mathcal{M}_2, \bar{d}_Y \right\rangle\models \varphi$ iff
$\left\langle \mathcal{M}_1, (\bar{R}^{ext})^{\mathcal{M}_1}, \bar{d}_Y, \bar{d}_{Y_S} \right\rangle \models \Phi_S(\varphi)$.
\end{lemma}

\begin{proof}
We prove the lemma by induction.
\begin{itemize}
\item $S=skip$: $Y_S = \emptyset$, and we have $\left\langle \mathcal{M}_2, \bar{d}_Y \right\rangle\models \varphi$
      iff $\left\langle \mathcal{M}_1, \bar{R}^{ext}, \bar{d}_Y \right\rangle\models \Phi_S(\varphi)$, as required.
\item $S = if\,b\,then\,S_1\,else\,S_2\, fi$: depending on whether $\varepsilon_b$ is true or false, $\Phi_{S_1}(\varphi)$ or $\Phi_{S_2}(\varphi)$
      should be used.
\item $var_1 := e$, where $e$ is a variable $var_2$ or $\mathrm{null}$: every reference to $var_1$ in $\varphi$ is replaced
      by a reference to $var_2$ or $\mathrm{null}$, respectively.
\item $var_1 := var_2.f$: every reference to $var_1$ in $\varphi$ is replaced with a reference to $o_y$, whose interpretation is $d_y$,
      in accordance with $\leadsto_{\bar{d}_{Y_S}}$, which requires that $d_y$ be the result of applying $f$ on $var_2$.
\item $var_1.f := e$, where $e$ is a variable $var_2$ or $\mathrm{null}$: the function symbol $f$ is updated by
      removing the current value of $f$ on $var_1$ by subtracting $(o_{var_{1}}\times\top)^{\mathcal{M}_1}$ from $f^{\mathcal{M}_1}$
      and setting the new value explicitly
      by adding the pair $(o_{var_1}^{\mathcal{M}_1},o_{e}^{\mathcal{M}_1})$ to $f^{\mathcal{M}_1}$.
\item $S= var := new$ with label $y$: $Y_S = \{y\}$ and $\bar{d}_{Y_S}=(d_y)$. By the definition of $\leadsto_{\bar{d}_{Y_S}}$
      for $new$ commands, $\{d_y\} = Alloc^{\mathcal{M}_2}\backslash Alloc^{\mathcal{M}_1}$.
      $\Phi_S(\varphi)$ adds $o_y$ to $Alloc$ and replaces
      every reference to $var$ by a reference to $o_y$.

\item $S = dispose(var)$: $\Phi_S(\varphi)$ removes $var$ from $Alloc$, and using an application of $\Phi$
      to the program $var.f_{k_1} := \mathrm{null}; \cdots; var.f_{k_w} := \mathrm{null}$, sets all of the fields
      in $\varphi$ to $\mathrm{null}$.
\item $S=S_1;S_2$: $\Phi_S(\varphi) = \Phi_{S_1}(\Phi_{S_2}(\varphi))$.
      Let $\mathcal{M}_3$ be an memory structure such that
      $\left\langle S_1,  \mathcal{M}_1 \right\rangle\leadsto_{\bar{d}_{Y_{S_1}}} \mathcal{M}_3$
      and $\left\langle S_2,  \mathcal{M}_3 \right\rangle\leadsto_{\bar{d}_{Y_{S_2}}} \mathcal{M}_2$.
      We have ${\bar{d}_{Y_{S}}} ={\bar{d}_{Y_{S_1}}}\cup {\bar{d}_{Y_{S_2}}}$.

      Consider first $\Phi_{S_2}(\varphi)$. By the induction hypothesis,
      $\left\langle \mathcal{M}_2, \bar{d}_Y \right\rangle\models \varphi$ iff
      $\left\langle \mathcal{M}_3,  \bar{R}^{\mathcal{M}_2}, \bar{d}_Y, \bar{d}_{Y_{S_2}} \right\rangle \models \Phi_{S_2}(\varphi)$.

      Let $\mathcal{M}_4$ be obtained from $\mathcal{M}_3$ be replacing every relation $R^{\mathcal{M}_3}$ with $R^{\mathcal{M}_2}$ for $R\in \tau^{rem}$.
      We have
      $\Psi_{S_2}(\varphi) \models \left\langle \mathcal{M}_4,\bar{d}_Y, \bar{d}_{Y_{S_2}} \right\rangle$
      iff $ \Phi_{S_2}(\varphi) \models \left\langle \mathcal{M}_3,  \bar{R}^{\mathcal{M}_2}, \bar{d}_Y, \bar{d}_{Y_{S_2}} \right\rangle$.

      Since we have $\left\langle S_2,  \mathcal{M}_4 \right\rangle\leadsto_{\bar{d}_{Y_{S_2}}} \mathcal{M}_2$,
      we can apply the induction hypothesis once again, this time on $\Psi_{S_2}$.
      We get that
      $\left\langle \mathcal{M}_4, \bar{d}_Y, \bar{d}_{Y_{S_2}} \right\rangle\models \varphi$ iff
      $\left\langle \mathcal{M}_1,  \bar{d}_Y, \bar{d}_{Y_{S_2}}, \bar{d}_{Y_{S_1}} \right\rangle \models \Phi_{S_1}(\Phi_{S_2}(\varphi))$.
      Hence,
      $\left\langle \mathcal{M}_2, \bar{d}_Y \right\rangle\models \varphi$ iff
      $\left\langle \mathcal{M}_1, \bar{R}^{\mathcal{M}_2}, \bar{d}_Y, \bar{d}_{Y_{S}} \right\rangle \models \Phi_{S_1}(\Phi_{S_2}(\varphi))$.

\end{itemize}

\end{proof}

\begin{proof}[Proof of Lemma \ref{lem:backwards-app}]

Using Lemma \ref{lem:backwards2-app} with $Y=\emptyset$,
if $\left\langle S, \mathcal{M}_1\right\rangle\leadsto_{\bar{d}_{Y_S}} \mbox{abort}$, then
for every tuple of relations $\bar{U}$ interpreting $\bar{R}^{ext}$ we have
$\left\langle \mathcal{M}_1, \bar{U}, \bar{d}_{Y_S}, d_{abo} \right\rangle \not\models \Phi_{\overline{S}}(\varphi\land (o_{abo} \equiv o_\mathbf{F}))$,
because $abo$ is set to true during the run of $\overline{S}$.
If $\left\langle S, \mathcal{M}_1\right\rangle\leadsto_{\bar{d}_{Y_S}} \mathcal{M}_2$,
$\mathcal{M}_2 \models \varphi$  iff
$\left\langle \mathcal{M}_1, \bar{d}_{Y_S}, d_{abo} \right\rangle \models \Phi_{\overline{S}}(\varphi\land (o_{abo} \equiv o_\mathbf{F}))$.

Note that $d_{abo}$ is the value of $abo$ at the beginning of the run of $\overline{S}$.
Since the first command of $\overline{S}$ assigns $abo$ a new value, $d_{abo}$ plays no role (it appears because, technically, $abo$ still needs a value at the beginning of the run).

Also note that in Lemma \ref{lem:backwards--}, $\bar{d}_{Y_{\overline{S}}}$ strictly extends $\bar{d}_{Y_S}$, since
$\overline{S}$ extends $S$. However, the semantics of all of the new commands in $\overline{S}$ does not actually
depend on the relevant $d_y$ (since none of them of $new$ commands or assignments of the form $var_1.var_2.f$).
Hence, any extension of  $\bar{d}_{Y_S}$ into $\bar{d}_{Y_{\overline{S}}}$ will do.
\end{proof}

\begin{remark}
Revisiting the example in Section \ref{se:backwards-example} with the detailed version of Lemma \ref{lem:backwards-app} in mind,
we now see that $\Theta$ is actually the backwards propagation of programs of the form $\overline{S}$.
The backward propagation of $\overline{\lambda(\ell_l.\ell_l)}$ is similar to that presented in Section
\ref{se:backwards-example}, with
$\Theta_{\overline{\lambda(\ell_l.\ell_l)}}(\varphi_{p-as-\ell_l}) = \Phi_{\overline{\lambda(l.l)}}(\varphi_{p-as-\ell_l}\land
(o_{abo} \equiv o_\mathbf{F}))$.

\end{remark}

\section{Application to program analysis}

\subsection{Memory Structures \label{subse:structures--1}\label{subse:memory-structures--1}}

We use ordinary first order structures to represent memory in a
precise way. A \emph{structure} (or, \emph{interpretation}) is a tuple
$\mathcal{M}=(M,\tau,\cdot)$, where
(i) $M$ is an infinite set (the \emph{universe}),
(ii) $\tau$ is a set of \emph{constants} and \emph{relation symbols}
  with an associated non-negative arity, and
(iii) $\cdot$ is an \emph{interpretation function}, which assigns to
  each constant $c\in \tau$ an element $c^\mathcal{M}\in M$, and to each
  $n$-ary relation symbol $R\in \tau$ an $n$-ary relation $R^{\mathcal{M}}$
  over $M$. Each relation is either unary or binary
  (i.e. $n\in\{1,2\}$).
  Given $A\subseteq M$, a binary $R^\mathcal{M}$, $R^\mathcal{M}$ and $e\in A^\mathcal{M}$, we may use the notation
  $R^\mathcal{M}(e)$ if $R^\mathcal{M}$ is known to be a function over $A^\mathcal{M}$.

A {\em Memory structure} describes a snapshot of the heap and the
local variables. We assume sets
$\tau_{\mathrm{var}}\subseteq \tau$ of constants $\tau_{\mathrm{fields}}\subseteq \tau$ of
binary relation symbols.  We will later employ these symbols for
variables and fields in programs.  A {\em memory structure} is a structure
$\mathcal{M}=(M,\tau,\cdot)$ that satisfies the following conditions:
\begin{enumerate}[(1)]
\item
  $\tau$ includes the constants $o_{\mathrm{null}}$, $o_\mathbf{T}$, $o_\mathbf{F}$.
\item $\tau$ has the unary relations $Addresses$, $Alloc$, $PossibleTargets$, $MemPool$,
  and $Aux$.
\item $Aux^\mathcal{M}=\{o_\mathrm{null}^\mathcal{M},o_\mathbf{T}^\mathcal{M},o_\mathbf{F}^\mathcal{M}\}$ and $|Aux^\mathcal{M}|=3$.
\item $Addresses^\mathcal{M}\cap Aux^\mathcal{M}= \emptyset$ and $Addresses^\mathcal{M} \cup Aux^\mathcal{M} =
  M$.
\item $Alloc^\mathcal{M}$, $PossibleTargets^\mathcal{M}$ and $MemPool^\mathcal{M}$ form a partition of $Addresses^\mathcal{M}$.
\item $c^\mathcal{M}\in M\backslash MemPool^\mathcal{M}$ for every constant $c$ of $\tau$.
\item For all $f\in  \tau_{\mathrm{fields}}$, $f^\mathcal{M}$ is a function from
  $Addresses^\mathcal{M}$ to $M\backslash MemPool^\mathcal{M}$.
\item If $e\in MemPool^\mathcal{M}$, then $f^\mathcal{M}(e)\in \{o_\mathrm{null}^\mathcal{M},o_\mathbf{F}^\mathcal{M}\}$.
\item $R^{\mathcal{M}}\subseteq (M\backslash MemPool^\mathcal{M})^n$ for every\footnote{Here $n\in \{1,2\}$.}
  $n$-ary $R\in \tau \setminus (\{MemPool \}\cup \tau_{\mathrm{fields}})$.
 \item $Alloc^\mathcal{M}$ and $PossibleTargets^\mathcal{M}$  are finite. $MemPool^\mathcal{M}$ is infinite.

\end{enumerate}

We explain the intuition behind memory structures. Variables in
programs will either have a Boolean value or be pointers. Thus, to
represent $\mathrm{null}$ and the Boolean values $\mathbf{T}$ and $\mathbf{F}$, we
employ the auxiliary relation $Aux^\mathcal{M}$ storing 3 elements
corresponding to the 3 values. $Addresses^{\mathcal{M}}$ represents the memory
cells.
The relation $Alloc^\mathcal{M}$ is the set of allocated
cells, $PossibleTargets^\mathcal{M}$ contains all cells which are not allocated,
but are pointed to by allocated cells (for technical reasons it possibly contains some other unallocated cells).
$MemPool^\mathcal{M}$ contains the cells which are not allocated, do
not have any field values other than $\mathrm{null}$ and $\mathbf{F}$, are not
pointed to by any field, do not participate in any other relation and
do not interpret any constant (see (6-9)). The memory cells in $MemPool$ are
the candidates for allocation during the run of a program.
 Since the allocated memory should by finite at any point of the
execution of a program, we require that
$Alloc^\mathcal{M} $ and $PossibleTargets^\mathcal{M}$
are finite (see (10)), while the available memory $Addresses^\mathcal{M}$ and the memory pool $MemPool^\mathcal{M} $
are infinite. Finally, each
cell is seen as a record with the fields of
$\tau_{\mathrm{fields}}$.

\subsubsection{Ghost symbols}
As discussed in Section \ref{se:EPM-example-DL},
in order to allow invariants of the form
$
\begin{array}{lll}
 \varphi_{lists-updt} &=& ELst_{{gho}} \equiv ELst  \land
  PLst_{{gho}}\sqcup o_{proj}  \equiv  PLst
\end{array}
$\\
we need ghost symbols.
We assume $\tau$ contains, for every symbol e.g. $s \in \tau$, the symbol $s_{{gho}}$.
Therefore, memory structures actually contain {\em two}
snapshots of the memory:
one is the {\em current} snapshot, on which the program operates,
and the other is a {\em ghost} snapshot, which is a snapshot of the memory
 at the beginning of the program, and which the program does not change or interact with.
We denote the two underlying memory structures of $\mathcal{M}$ by
$\mathcal{M}_{cur}$ and $\mathcal{M}_{gho}$.
Since the interpretations of ghost symbols should not change throughout the run of a program,
they will sometime require special treatment.

\subsection{Syntax and Semantics of the Programming Language }

\subsubsection{Loopless Programs}
are generated by the following syntax:
\begin{center}
$
\begin{array}{lll}
e & :: & var.f\mid var\mid\mathrm{null}\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,(f\in\tau_{\mathrm{fields}},\, o_{var}\in\tau_{\mathrm{var}})\\
b & :: &(e_{1}=e_{2})\mid\,\sim b\mid(b_{1}\, and\, b_{2})\mid(b_{1}\, or\, b_{2}) \mid \mathbf{T} \mid \mathbf{F}\\
S & :: & var_{1}:=e_{2}\mid var_{1}.f:=e_{2}\mid skip\mid S_{1};S_{2}
\mid var:=new \mid dispose(var)  \mid \\
 & & if\,\, b\,\, then\,\, S_{1}\,\, fi
  \mid if\,\, b\,\, then\,\, S_{1}\,\, else\,\, S_{2}\,\, fi \mid assume(b)
\end{array}
$
\end{center}

 Let $Exp$
denote the set of expressions $e$ and $Bool$ denote the set of Boolean
expressions $b$.
To define the semantics of pointer and Boolean expressions, we extend  $f^{\mathcal{M}}$
by $f^{\mathcal{M}}(\mbox{err})=\mbox{err}$ for every $f\in \tau_{\mathrm{fields}}$. We define
$\mathcal{E}_e(\mathcal{M}):Exp\,\,\to Addresses^\mathcal{M}\cup\{\mathrm{null},\mbox{err}\}$ and $\mathcal{B}_b(\mathcal{M}):Bool\to\{o_\mathbf{T},o_\mathbf{F},\mbox{err}\}$
(with $\mbox{err}\not\in M$):
\begin{center}
$
\begin{array}{llll}
\mathcal{E}_{var}(\mathcal{M}) & =o_{var}^{\mathcal{M}},  \mbox{ if }o_{var}^{\mathcal{M}}\in Alloc^{\mathcal{M}}\ &
\mathcal{B}_{e_{1}=e_{2}}(\mathcal{M}) & =\mbox{err}  \mbox{ if }\mathcal{E}_{e_{i}}(\mathcal{M})=\mbox{err}, i\in\{1,2\}\\
\mathcal{E}_{var}(\mathcal{M}) & =\mbox{err},  \mbox{ if }o_{var}^{\mathcal{M}}\not\in Alloc^{\mathcal{M}}&
\mathcal{B}_{e_{1}=e_{2}}(\mathcal{M}) & =o_\mathbf{T},  \mbox{ if }\mathcal{E}_{e_{1}}(\mathcal{M})=\mathcal{E}_{e_{2}}(\mathcal{M})\\
\mathcal{E}_{ar.f}(\mathcal{M}) &=f^{\mathcal{M}}(\mathcal{E}_{var}(\mathcal{M}))&
\mathcal{B}_{e_{1}=e_{2}}(\mathcal{M}) & =o_\mathbf{F},  \mbox{ if }\mathcal{E}_{e_{1}}(\mathcal{M})\not=\mathcal{E}_{e_{2}}(\mathcal{M})
\end{array}
$\end{center}
$\mathcal{B}$ extends naturally w.r.t. the Boolean connectives.

The operational semantics of the programming language is:
For any command $S$, if $\mathcal{E}$ or $\mathcal{B}$
give the value $\mbox{err}$, then $\left\langle S,\mathcal{M}\right\rangle \leadsto\mbox{abort}$.
Otherwise, the semantics is as listed below.
First we assume that
in the memory structures involved
all relation symbols either belong to $\tau_{\mathrm{fields}}$, are ghost symbols
or are the required symbols of memory structures ($Alloc$, $Aux$, etc.).
\begin{enumerate}
\item $\left\langle skip,\mathcal{M}\right\rangle \leadsto\mathcal{M}$.
\item
$\left\langle var_{1}:=e_{2},\mathcal{M}\right\rangle \leadsto[\mathcal{M}\mid o_{var_{1}}^{\mathcal{M}}\mbox{ is set to }\mathcal{E}_{e_{2}}(\mathcal{M})]$.
\item $\left\langle var:=new,
\mathcal{M}\right\rangle\leadsto$
$[\mathcal{M}\mid \mbox{For some }t\inMemPool^\mathcal{M},$ \\$ t\mbox{ is moved to }Alloc^{\mathcal{M}}\mbox{ and }o_{var}^{\mathcal{M}}\mbox{ is set to }t],$
\item If $o_{var}^{\mathcal{M}}\not\in Alloc^{\mathcal{M}}$, $\left\langle dispose(var),\mathcal{M}\right\rangle \leadsto\mbox{abort}$;\\
otherwise $\left\langle dispose(var),\mathcal{M}\right\rangle \leadsto[\mathcal{M}\mid o_{var}^{\mathcal{M}}\mbox{ is removed from }Alloc^{\mathcal{M}}]$.
\item $\left\langle S_{1};S_{2},\mathcal{M}\right\rangle \leadsto\left\langle S_{2},\left\langle S_{1},\mathcal{M}\right\rangle \right\rangle$
\item
$\left\langle if\,\, b\,\, then\,\, S_{\mathbf{T}}\,\, else\,\, S_{\mathbf{F}},\mathcal{M}\right\rangle \leadsto\left\langle S_{tv},\mathcal{M}\right\rangle $
where $tv=\mathcal{B}_{b}(\mathcal{M})$.
\item
$\left\langle if\,\, b\,\, then\,\, S\,\, ,\mathcal{M}\right\rangle \leadsto
\left\langle if\,\, b\,\, then\,\, S\,\, else\,\, skip\,\, fi ,\mathcal{M}\right\rangle$.
\item
If $\mathcal{B}_{b}(\mathcal{M})=\mathbf{T}$, then
$\left\langle assume(b), \mathcal{M}\right\rangle \leadsto \mathcal{M}$;\\
otherwise $\left\langle assume(b), \mathcal{M}\right\rangle \leadsto \mbox{abort}$.
\end{enumerate}
If $\mathcal{M}$ is
a memory structure and $\left\langle S,\mathcal{M}\right\rangle \leadsto\mathcal{M}'$,
then $\mathcal{M}'$ is a memory structure.

Now consider a relation symbol e.g. $ELst$.
If $\left\langle S,\mathcal{M}\right\rangle \leadsto\mathcal{M}'$,
then we want to think of $ELst^{\mathcal{M}}$ and $ELst^{\mathcal{M}'}$ as the employee list
before and after the execution of $S$. However, the constraints that
$ELst^{\mathcal{M}}$ and $ELst^{\mathcal{M}'}$ are lists and that
$ELst^{\mathcal{M}'}$ is indeed obtained from from $ELst^{\mathcal{M}}$ by running $S$
will be expressed as formulae.
In the $\leadsto$ relation, we allow any values for $ELst^\mathcal{M}$ and $ELst^{\mathcal{M}'}$.

For any tuple $\bar{R}$ of relation symbols which do not belong to $\tau_{\mathrm{fields}}$,
are not ghost symbols
and are not the required symbols of memory structures ($Alloc$, $Aux$, etc.),
we extend $\leadsto$ as follows: if $\left\langle S,\mathcal{M}\right\rangle \leadsto\mathcal{M}'$,
then $\left\langle S,\left\langle \mathcal{M},\bar{R}^{\mathcal{M}}\right\rangle \right\rangle \leadsto\left\langle\mathcal{M}',\bar{R}^{\mathcal{M}'}\right\rangle$,
for any tuples $\bar{R}^{\mathcal{M}}$ and $\bar{R}^{\mathcal{M}'}$.

\subsubsection{Programs with Loops} are represented as hybrids of the programming language for loopless code
and control flow graphs.
 \begin{definition}[Program]\label{def:program}
 A {\em program} is $G = \left\langle V, E,\ell_{init}, shp, dmn,\lambda\right\rangle$
 such that
 $G=(V,E)$ is a directed graph with no multiple edge but possibly containing self-loops, $\ell_{init} \in V$ has in-degree $0$,
  $shp:V\to \mathrm{\mathbf{SL{\scriptstyle ls}}}$, $dmn:V\to \mathcal{ALCQIO}_{b,Re}(\tau)$ are functions, and $\lambda$ is a function from $E$ to the set of loopless programs.
 \end{definition}

\begin{tabular}{ll}
Here is the code $S$ from the introduction:   &
\multirow{5}{*}{\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \includegraphics[scale=0.80]{ProgramGraph}}\\
\end{tabular}\\
\begin{tabular}{ll}
$V=\{\ell_{b},\ell_l,\ell_{e}\}$ & $E=\{(\ell_{b},\ell_l),(\ell_l,\ell_l),(\ell_l,\ell_{e})\}$ \\
$\lambda(\ell_{b},\ell_l)=S_{b}$ & $\ell_{init}=\ell_{b}$ \\
 $\lambda(\ell_l,\ell_l)=assume(\sim(e\,=\,\mathrm{null}));S_{\ell_l}$\\
$\lambda(\ell_l,\ell_e)=assume(e\,=\,\mathrm{null});S_e$
\end{tabular}
\\ \ \\
$S_{b}$, $S_{\ell_l}$ and $S_{e}$ denote
 the three loopless code blocks which are respectively the code block before the loop, inside the loop and after the loop.
 The annotations $shp$ and $dmn$ are described in Section \ref{se:general-meth-example}.

The semantics of programs derive from the semantics of loopless programs and is given in terms of program paths.
Given a program $G$, a {\em path in $G$} is a finite sequence of directed edges
$e_1,\ldots,e_t$ such that for all $1\leq i\leq t-1$, the tail of $e_i$
is the head of $e_{i+1}$.
A path may contain cycles.
 \begin{definition}[$\leadsto^*$ for paths]
 Given a program $G$, a path $P$ in $G$,
 and memory structures $\mathcal{M}_1$ and $\mathcal{M}_2$
 we define whether
 $\left\langle P, \mathcal{M}_1\right\rangle\leadsto^* \mathcal{M}_2$
 holds inductively.
 \begin{itemize}
 \item If $P$ is empty, then $\left\langle P, \mathcal{M}_1\right\rangle\leadsto^* \mathcal{M}_2$ iff $\mathcal{M}_1=\mathcal{M}_2$.
 \item If $e_t$ is the last edge of $P$, then $\left\langle P, \mathcal{M}_1\right\rangle\leadsto^* \mathcal{M}_2$ iff
 there is $\mathcal{M}_3$ such that
 $\left\langle P\backslash\{e_t\}, \mathcal{M}_1 \right\rangle\leadsto^* \mathcal{M}_3$
 and $\left\langle \lambda(e_t), \mathcal{M}_1 \right\rangle\leadsto^* \mathcal{M}_3$.
  $P\backslash\{e_t\}$ denotes the path obtained from $P$ by removing the last edge $e_t$.
 \end{itemize}
 \end{definition}

\subsection{Hoare-style Proof System}

Now we are ready to state our two-step verification methodology that we formulated in Section \ref{se:intro} precisely.
Our methodology assumes a program $P$ as in Definition~\ref{def:program} as input (ignoring the $shp$ and $dmn$ functions for the moment).

\textbf{I. Shape Analysis.}
The user annotates the program locations with SL formulae from $\mathrm{\mathbf{SL{\scriptstyle ls}}}$ (stored in the $shp$ function of $P$).
Then the user proves the validity of the $\mathrm{\mathbf{SL{\scriptstyle ls}}}$ annotations, for example, by using techniques from~\cite{pr:BCO05}.

\textbf{II. Content Analysis.}
The user annotates the program locations with $\mathcal{ALCQIO}_{b,Re}$-formulae that she wants to verify (stored in the $dmn$ function of $P$).
We point out that an annotation $dmn(\ell)$ can use the concepts occurring in $\alpha(shp(\ell))$ (recall that $\alpha: \mathrm{\mathbf{SL{\scriptstyle ls}}} \rightarrow \mathcal{ALCQIO}_{b,Re}$ maps SL formulae to $\mathcal{ALCQIO}_{b,Re}$-formulae).

In the rest of the paper we discuss how to verify the $dmn$ annotations.
In Section~\ref{se:methodology} we describe how to derive a verification condition for every program edge.
The verification conditions rely on the backwards propagation function $\Theta$ for $\mathcal{ALCQIO}_{b,Re}$-formulae which we introduce in Section~\ref{se:backwards-example}.
The key point of our methodology is that the validity of the verification conditions can be discharged automatically by a satisfiability solver for $CT^{2}$-formulae.
We show that all the verification conditions are valid if and only if $dmn$ is inductive.
Intuitively, $dmn$ being inductive ensures that the annotations $dmn$ can be used in an inductive proof to show that all reachable memory structures indeed satisfy the annotations $dmn(\ell)$ at every program location $\ell$ (see Definition~\ref{def:inductive-annotation} below).

\subsection{Content Verification}\label{se:methodology}

 We want to prove that, for every initial memory structure $\mathcal{M}_1$
 from which the computation satisfies $shp$ and which satisfies the domain~pre-condition $dmn(\ell_{init})$,
 the computation satisfies $dmn$. Here are the corresponding verification conditions, which annotate the vertices of $G$:

\begin{definition}[Verification conditions]
 Given a program $G$, $VC$ is the function from $E$ to $\mathcal{ALCQIO}_{b,Re}$
 given for $e=(\ell_0,\ell)$ by
 \begin{eqnarray*}
    VC(e) &=& \neg \big[ \beta(shp(\ell_0))\land tr(dmn(\ell_0))  \land tr\left( \Theta_{\lambda(e)}\big(\alpha(shp(\ell)) \land \neg  dmn(\ell)\big)\right)\big]
 \end{eqnarray*}
 $VC(e)$ {\em holds} if $VC(e)$ is a tautology over memory structures ($\top \models_m VC(e)$).

 \end{definition}
 $\Theta$ is discussed in Section \ref{se:backwards--}. As we will see, $VC(\ell_0,\ell)$ expresses that
 when running the loopless program $\lambda(e)$ when the memory satisfies the the annotations of $\ell_0$,
 and when the shape annotation of $\ell$ is at least partly true (i.e., when $\alpha(shp(\ell))$),
 the content annotation of $\ell$ holds.

 Let $J$ be a set of  memory structures.
 For a formula in $CT^{2}$ or $\mathcal{ALCQIO}_{b,Re}$, we write $J\models\varphi$
 if, for every $\mathcal{M}\in J$, $\mathcal{M}\models \varphi$.
 Let $Init$ be a set of memory structures.
 \begin{definition}[Inductive program annotation]
 \label{def:inductive-annotation}
 Let $f:V\to CT^{2}$.
 We say $f$ is {\em inductive} for $Init$ if (i) $Init\models f(\ell_{init})$, and (ii)
 for every edge $e=(\ell_1,\ell_2)\in E$ and memory structures
 $\mathcal{M}_1$ and $\mathcal{M}_2$ such that $\mathcal{M}_1\models f(\ell_1)$ and $\left\langle \lambda(e),\mathcal{M}_1\right\rangle \leadsto \mathcal{M}_2$,
 we have $\mathcal{M}_2\models f(\ell_2)$.

 We say $shp$ is inductive for $Init$ if the composition $shp\circ\beta:V\toCT^{2}$ is inductive for $Init$.

 We say {\em $dmn$ is inductive for $Init$ relative to $shp$}
 if $shp$ is inductive for $Init$ and
 $g:V\toCT^{2}$ is inductive for $Init$,
 where $g(\ell)=tr(dmn(\ell))\land \beta(shp(\ell))$.
 \end{definition}

 \vspace{4pt}
 \begin{theorem}[Soundness and Completeness of the Verification Conditions] \label{th:soundness-completeness}
 Let $G$ be a program such that $shp$ is inductive for $Init$ and $Init\models cnt(\ell_{init})$.
The following statements are equivalent:\\
 (i)  For all $e\in E$, $VC(e)$ holds.\ \ \ \ \ (ii)  $dmn$ is inductive for $Init$ relative to $shp$.
 \end{theorem}

 We make the notion of a computation satisfying the verification conditions precise using the following definition:
 \begin{definition}[$Reach(\ell)$]
 Given a program $G$, a node $\ell\in V$, and a set $Init$ of memory structures,
 $Reach(\ell)$ is the set of  memory structures $\mathcal{M}$ for which there is
 $\mathcal{M}_{init} \in Init$ and a path $P$ in $G$ starting at $\ell_{init}$
 such that $\left\langle P,\mathcal{M}_{init}\right\rangle\leadsto^* \mathcal{M}$.
 \end{definition}
 In particular, $Reach(\ell_{init})=Init$.
 The proof of Theorem \ref{th:soundness-completeness} and its consequence Theorem \ref{th:soundness-2} below
 are in Appendix \ref{app:soundness-completeness}.
 \begin{theorem}[Soundness of the Verification Methodology] \label{th:soundness-2}
 Let $G$ be a program such that $shp$ is inductive for $Init$ and $Init\models cnt(\ell_{init})$.
 If for all $e\in E$,
 $VC(e)$ holds, then for $\ell\in V$, $Reach(\ell)\models dmn(\ell)$.
 \end{theorem}

\subsection{Backwards Propagation and the Running Example}\label{se:backwards--}\label{se:backwards-example}
Here we shortly discuss the backwards propagation of a formula along a loopless program $S$.
Let $\left\langle S, \mathcal{M}_1\right\rangle\leadsto \mathcal{M}_2$ where $\mathcal{M}_1$ and $\mathcal{M}_2$
are memory structures over the same vocabulary $\tau$.
E.g., in our running example, for $i=1,2$, $\mathcal{M}_i$ is
\[
\begin{array}{l}
\left\langle M, ELst^{\mathcal{M}_i}, next^{\mathcal{M}_i}, mngBy^{\mathcal{M}_i}, \cdots,\right.
\left. ELst_{{gho}}^{\mathcal{M}_i}, next_{{gho}}^{\mathcal{M}_i},  \cdots, Alloc^{\mathcal{M}_i}, Aux^{\mathcal{M}_i} \cdots  \right\rangle
\end{array}
\]

We will show how to translate a formula for $\mathcal{M}_2$ to a formula for an extended $\mathcal{M}_1$.
Fields and variables in $\mathcal{M}_2$ will be translated by the backwards propagation
 into expressions
involving elements of $\mathcal{M}_1$. For ghost symbols $s_{{gho}}$, $s_{{gho}}^{\mathcal{M}_1}$ will be used instead of $s_{{gho}}^{\mathcal{M}_2}$
since they do not change during the run of the program. Let $\tau^{rem}\subseteq \tau$ be the set of the remaining symbols,
i.e.  the symbols of $\tau \setminus (\{PossibleTargets,MemPool \}\cup \tau_{\mathrm{fields}})$ which are not ghost symbols,
for example $ELst$, but not $ELst_{{gho}}$, $next$ or $mngBy$.
We need the result of the backwards propagation to refer to the interpretations of symbols in $\tau^{rem}$
from $\mathcal{M}_2$ rather than $\mathcal{M}_1$.
Therefore,
these interpretations are copied as they are from $\mathcal{M}_2$ and added to $\mathcal{M}_1$ as follows.
For every $R\in \tau^{rem}$, we add a symbol $R^{ext}$ for the copied relation.
We denote by $(\bar{R}^{ext})^{\mathcal{M}_1}$ the tuple
$
 \big((R^{ext})^{\mathcal{M}_1} : (R^{ext})^{\mathcal{M}_1}=R^{\mathcal{M}_2}\mbox{ and }R\in\tau^{rem}\big)
$
Let $\tau^{ext}$ extend $\tau$ with $R^{ext}$ for each $R\in\tau^{rem}$.
The backwards propagation updates the fields and variables according to the loopless code.
Afterwards, we substitute the symbols $R\in\tau^{rem}$ in $\varphi$ with the corresponding $R^{ext}$.

We present here a somewhat simplified version of the backwards propagation lemma. The precise version is similar in spirit
and is given in Appendix \ref{app:backward}.
\begin{lemma}[Simplified]\label{lem:backwards--} \label{se:backwards-ghost--}
Let $S$ be a loopless program, let
$\mathcal{M}_1$ and $\mathcal{M}_2$ be  memory structures, and
 $\varphi$ be an $\mathcal{ALCQIO}_{b,Re}$-formula over $\tau$.
\begin{enumerate}
 \item If $\left\langle S, \mathcal{M}_1\right\rangle \leadsto \mathcal{M}_2$,
 then:
 $\mathcal{M}_2\models \varphi$ iff
$\left\langle \mathcal{M}_1, (\bar{R}^{ext})^{\mathcal{M}_1}\right\rangle \models \Theta_{S}(\varphi)$.
\item If $\left\langle S, \mathcal{M}_1\right\rangle\leadsto \mbox{abort}$, then
$\left\langle \mathcal{M}_1, (\bar{R}^{ext})^{\mathcal{M}_1},\right\rangle \not\models \Theta_{S}(\varphi)$.
\end{enumerate}
\end{lemma}

As an example of the backwards propagation process,
we consider a formula from Section \ref{se:general-meth-example},
which is part of the domain~annotation of $\ell_l$
and perform the backwards propagation on the loopless program inside the loop:
\[
\begin{array}{lll}
\varphi_{p-as-\ell_l} &=&
P_1 \sqcap\exists wrkFor_{{gho}}.o_{\mathrm{null}} \equiv
P_1 \sqcap\exists wrkFor.o_{proj}
\end{array}
\]

Since $next$ does not occur in $\varphi_{p-as-\ell_l}$, backwards propagation of $\varphi_{p-as-\ell_l}$
over $e := e.next$ does not change the formula (however $\alpha(shp(\ell_l))$
by this command). The backwards propagation of the $if$ command gives
\[
\begin{array}{ll}
 \Psi_{S_{\ell_l}}(\varphi_{p-as-\ell_l}) = &
 \big(\neg(\exists wrkFor^-.o_e \equiv o_\mathrm{null})  \land
 \varphi_{p-as-\ell_l} \big) \lor \\
 &\exists wrkFor^-.o_e \equiv o_\mathrm{null}\hphantom{)}\land
 \Psi_{e.wrkFor := proj}(\varphi_{p-as-\ell_l})\big)\\
\Psi_{e.wrkFor := proj}(\varphi_{p-as-\ell_l}) =&
 P_1 \sqcap\exists wrkFor_{gho}.o_{\mathrm{null}} \equiv  \\
 & P_1\sqcap\exists {((wrkFor\backslash (o_{e} \times \top)) \cup (o_e,o_{proj}))}.o_{proj}
\end{array}
\]
$\Psi_{e.wrkFor := proj}(\varphi_{p-as-\ell_l})$ is obtained from $\varphi_{p-as-\ell_l}$ by substituting the $wrkFor$
role with the correction  $((wrkFor\backslash (o_{e} \times \top)) \cup (o_e,o_{proj}))$
which updates the value of $o_e$ in $wrkFor$ to $proj$.
$\Phi_{S_{\ell_l}}(\varphi_{p-as-\ell_l})$ is obtained from $\Psi_{S_{\ell_l}}(\varphi_{p-as-\ell_l})$
by subtituting ${P_1}$ with ${P_1}^{ext}$.
$\Theta$ is differs from $\Phi$ from technical reasons related to
aborting computations (see Appendix \ref{app:backward}).

 \input{appendix-backwards}

\section{\label{se:main-section} Decision procedures for $\mathcal{ALCQIO}_{b,Re}$}

Let $\Phi=\varphi\land\bigwedge RE\land\bigwedge DI$ be an $\mathcal{ALCQIO}_{b,Re}$-formula.
Let $\tau=\mathsf{N_{C}}\cup\mathsf{N_{R}}\cup\mathsf{N_{n}}$ be the vocabulary of $\varphi$.
We denote $RE=\{\Reacha{B_{1}}{S_{1}}{A_{1}},\ldots,\Reacha{B_{h}}{S_{h}}{A_{h}}\}$.

In this section we prove the existence a decision procedure of finite satisfiability and implication for $\mathcal{ALCQIO}_{b,Re}$:

\begin{thm-th:exp}
Let $\Phi_{i}=\varphi_{i}\land\bigwedge RE_{i}\land\bigwedge DI_{i}\in\mathcal{ALCQIO}_{b,Re}$, for $i=1,2$.
There are $\mathcal{\LoiqNObTEXT}$ formulas $\mu$ and $\kappa$ over an extended vocabulary such that\\
(1) $\Phi_{1}$ is finitely satisfiable iff $\mu$ is finitely satisfiable.\\
(2) $\Phi_{1}$ implies $\Phi_{2}$ iff $\kappa$ is not finitely satisfiable.
\end{thm-th:exp}

\paragraph{Outline of proof. }

$\formula{\Phi}$ already belongs to $\LoiqNOb_{b}$.
The reachability requirements are missing in order to capture $\Phi$.
The models of $\formula{\Phi}$ can be partitioned into \emph{standard }and \emph{non-standard models}, depending on whether they satisfy $\bigwedge RE$.
In general, we cannot augment $\formula{\Phi}$ in $\LoiqNOb_{b}$ to eliminate the non-standard models, since reachability is not expressible
in $\LoiqNOb_{b}$.
However, we can augment it so that it is guaranteed that whenever a non-standard model exists, so does a standard model.
To do so, we define \emph{semi-connectedness}, which is a weaker requirement than satisfying $\bigwedge RE$.
A model is semi-connected if every element of its universe which should be reachable according to some $\Reacha{B_{i}}{S_{i}}{A_{i}}$ and is not, is reachable from a cycle in $A_{i}$.
We show that semi-connectedness is expressible in $\LoiqNOb_{b}$.

Under certain conditions, it is possible to repeatedly apply an operation $\rhd$, which turns non-standard but semi-connected models into standard models, by eliminating the said cycles.
The existence of a non-standard semi-connected model then implies the existence of a standard model.
A sufficient condition under which semi-connected models can be turned to standard models using $\rhd$ is that the elements in $A_{i}$ admit so-called \emph{useful labelings}.
Useful labelings mimic an order relation on the types of the elements in $A_{i}$ and guarantee that applying the operation $\rhd$ makes progress towards a standard model.
We show that having useful labelings is expressible in $\LoiqNOb_{b}$.

As a consequence we get a decision procedure for satisfiability of
$\Phi$, which amounts to adding to $\formula{\Phi}$ the requirements that models are semi-connected and have useful labelings.
The resulting $\mathcal{\LoiqNObTEXT}$-formula is satisfiable iff $\Phi$ is.
A decision procedure for implication is obtained as consequence.
Decision procedures which are tight in terms of complexity are given in Section \ref{se:poly}.
In Section \ref{se:reduce-to-formula} we give simpler but complexity-wise suboptimal decision procedures.
The decision procedures in Section \ref{se:poly} follow the same plan, and differ only in the construction and sizes of the formulae expressing the existence of useful labelings.

\subsection{Types and the operation $\rhd$}

We write $C\in\varphi$ if there exists a concept $D$ and an inclusion
$C\sqsubseteq D$ or $D\sqsubseteq C$ which occurs in $\varphi$.
$C$ and $D$ need not be atomic.
\begin{definition}
[$\rhd$] Let $\mathcal{M}$ be a $\tau$-structure.
Let $a_{0},a_{1}\in M$ and $r\in\mathsf{N_{F}}$ and $\mathfrak{t} = (a_{0},a_{1},r)$.
Let $\op{\mathcal{M}}{\mathfrak{t}}$ be the structure such that $\mathcal{M}$ and $\op{\mathcal{M}}{\mathfrak{t}}$ have the same universe $M$ and the same interpretations of every atomic concept, nominal and atomic role except for $r$, and $r^{\op{\mathcal{M}}{\mathfrak{t}}} = r^{\mathcal{M}} \setminus \{(a_{i},b) \mid (a_{i},b) \in r \text{ and } i \in \{0,1\}\} \cup$ $\{(a_{1-i},b) \mid (a_{i},b) \in r \text{ and } i \in \{0,1\}\}$.
\end{definition}

For the main property of $\rhd$ we need the notion
of types:
\begin{definition}
[Types]
We define $\mathrm{TYPES}_{\varphi} = \textbf{2}^{ \{C \mid C \in \varphi\} }$ as the powerset over the set of concepts appearing in $\varphi$.
Let $\mathcal{M}$ be a $\tau$-structure $\mathcal{M}$ and $u \in M$.
We denote by $\overline{tp}_{\mathcal{M}}^{\varphi}(u) \in \mathrm{TYPES}_{\varphi}$ the set of concepts $C \in \varphi$ such that $u \in C^{\mathcal{M}}$.
We call $\overline{tp}_{\mathcal{M}}^{\varphi}(u)$ the \emph{type} of $u$.
We sometimes omit the subscript $\mathcal{M}$ when it is clear from the context.
\end{definition}
We note that the size of $\mathrm{TYPES}_{\varphi}$ is at most $2^{|\varphi|}$.

\begin{lemma}
\label{lem:types}
\label{lem:1-type-to-2-type-a-}
\label{lem:1-type-to-2-type-b-}
Let $\mathcal{M}_{1}$ and $\mathcal{M}_{2}$ be two $\tau$-structures with the same universe $M$.
If for all $u\in M$ we have $\overline{tp}_{\mathcal{M}_{1}}^{\varphi}(u)=\overline{tp}_{\mathcal{M}_{2}}^{\varphi}(u)$,
then $\mathcal{M}_{1}$ and $\mathcal{M}_{2}$ agree on $\varphi$.
\end{lemma}

\begin{proof}
$\varphi$ is a Boolean combination of inclusion assertions.
Therefore, it is enough to show $\mathcal{M}_{1}\models C\sqsubseteq D$ iff $\mathcal{M}_{2}\models C\sqsubseteq D$ for all of the inclusion assertions $C\sqsubseteq D$ which occur
in $\varphi$.
Let $C\sqsubseteq D$ be such an inclusion assertion.
For $u\in M$, $u\in C^{\mathcal{M}_{1}}$ iff $u\in C^{\mathcal{M}_{2}}$, and $u\in D^{\mathcal{M}_{1}}$
iff $u\in D^{\mathcal{M}_{2}}$.
Hence, $C^{\mathcal{M}_{1}}=C^{\mathcal{M}_{2}}$ and $D^{\mathcal{M}_{1}}=D^{\mathcal{M}_{2}}$,
implying $\mathcal{M}_{1}\models C\sqsubseteq D$ iff $\mathcal{M}_{2}\models C\sqsubseteq D$.
\end{proof}

The crucial property of $\rhd$ is that $\mathcal{M}$ and $\op{\mathcal{M}}{\mathfrak{t}}$ agree on $\varphi$ if $a_{0}$ and $a_{1}$ have the same type:

\begin{lemma}
\label{lem:op-on-concepts} \label{lem:mm-op--}
Let $\mathcal{M}$ be a $\tau$-structure, let $a_{0}, a_{1} \in M$ such that $\overline{tp}_{\mathcal{M}}^{\varphi}(a_{0}) = \overline{tp}_{\mathcal{M}}^{\varphi}(a_{1})$,
let $r \in \mathsf{N_{F}}$, and let $\mathfrak{t}=(a_{0},a_{1},r)$.
\begin{enumerate}[(1)]
 \item $C^{\mathcal{M}}=C^{\op{\mathcal{M}}{\mathfrak{t}}}$ for all $C\in\varphi$.
\end{enumerate}
Consequently:
\begin{itemize}
 \item[(2)]  For every $u\in M$, $\overline{tp}_{\mathcal{M}}^{\varphi}(u) = \overline{tp}_{\op{\mathcal{M}}{\mathfrak{t}}}^{\varphi}(u)$.
 \item[(3)] $\mathcal{M}\models \varphi$ iff $\op{\mathcal{M}}{\mathfrak{t}}\models \varphi$.
 \end{itemize}
\end{lemma}

Statement (1) of Lemma \ref{lem:op-on-concepts} is proven by induction on the construction of concepts in $\varphi$.
(2) follows directly from (1).
(3) follows using Lemma \ref{lem:types}.
See Appendix \ref{app:proofs-lem:op-on-concepts} for a detailed proof.

\section{\label{app:LoiqFO} \texorpdfstring{$\LoiqNOb_{b}$}{\LoiqNObTEXT b} and first order logic}

$\LoiqNOb_{b}$ has a fairly standard reduction to the two-variable fragment
of first order logic with counting $C^{2}$ (see e.g. \cite{DBLP:journals/ai/Borgida96})
\begin{definition}
Let $tr:\LoiqNOb_{b}\toC^{2}$ be given as follows:
\end{definition}
\[
\begin{array}{lll}
tr_{z}(C) & = & C(z)\qquad\qquad~C~\mbox{ is an atomic concept}\\
tr_{z,\bar{z}}(r) & = & r(z,\bar{z})\qquad\qquad r~\mbox{ is an atomic role}\\
tr_{z}(C\sqcap D) & = & tr_{z}(C)\land tr_{z}(D)\\
tr_{z}(C\sqcap D) & = & tr_{z}(C)\lor tr_{z}(D)\\
tr_{z}(\neg C) & = & \neg tr_{z}(C)\\
tr_{z,\bar{z}}(r^{-}) & = & tr_{\bar{z},z}(r)\\
tr_{z}(\exists r.C) & = & \exists y.tr_{z,\bar{z}}(r)\land tr_{\bar{z}}(C)\\
tr_{z}(\exists^{\leq n}r.C) & = & \exists^{\leq n}y.tr_{z,\bar{z}}(r)\land tr_{\bar{z}}(C)\\
tr_{z}(\exists^{\geq n}r.C) & = & \exists^{\geq n}y.tr_{z,\bar{z}}(r)\land tr_{\bar{z}}(C)\\
\\
tr(C\sqsubseteq D) & = & \forall x.tr_{x}(C)\rightarrow tr_{x}(D)\\
tr(\varphi\land\psi) & = & tr(\varphi)\land tr(\psi)\\
tr(\neg\varphi) & = & \neg tr(\varphi)
\end{array}
\]

\begin{lemma}
For every $\varphi\in\LoiqNOb_{b}$, $\varphi$ and $tr(\varphi)$ agree
on the truth value of all $\tau$-structures.
\end{lemma}

\section{\label{app:Loiq_LoiqNOb} From \texorpdfstring{$\LoiqNOb_{b}$}{\LoiqNObTEXT b}
to \texorpdfstring{$\mathcal{\LoiqNObTEXT}$}{ALCQIO}}

Here we show the reduction from satisfiability in $\LoiqNOb_{b}$ to satisfiability
in $\mathcal{\LoiqNObTEXT}$.
\begin{lemma}
Let $\tau$ be a vocabulary and $\varphi\in\LoiqNOb_{b}(\tau)$. There exist
a vocabulary $\sigma\supseteq\tau$ and $\psi\in\mathcal{\LoiqNObTEXT}(\sigma)$
such that $\varphi$ is satisfiable iff $\psi$ is satisfiable, and
the size of $\psi$ is linear in the size of $\varphi$. More precisely:
\begin{enumerate}
\item If $\mathcal{M}$ is a $\tau$-structure satisfying $\varphi$, then there
exists an extension $\mathcal{N}$ of $\mathcal{M}$ such that $\mathcal{N}\models\psi$.
$\mathcal{N}$ has the same universe as $\mathcal{M}$ and agrees with $\mathcal{M}$ on the
interpretation of the symbols in $\tau$.
\item If $\mathcal{N}$ is a $\sigma$-structure satisfying $\psi$, then the substructure
of $\mathcal{N}$ which corresponds to $\tau$ satisfies $\varphi$.
\end{enumerate}
\end{lemma}
\begin{proof}
We prove the claim by induction on the construction of formulae in
$\LoiqNOb_{b}$. The claim we prove is slightly augmented as follows:
\begin{itemize}
\item We assume without loss of generality that $\varphi$ is given in negation
normal form (NNF).
\item $\psi$ will not contain any negations.
\end{itemize}

We may assume without loss of generality that if $\varphi$ is satisfiable,
then it is satisfiable by a structure of size strictly larger than
$1$.

\end{proof}
\begin{description}
\item [{Base}] If $\varphi=C\sqsubseteq D$, then $C\sqsubseteq D\in\mathcal{\LoiqNObTEXT}$
and $\sigma=\tau$.
\item [{Closure}] Let $\varphi_{1},\varphi_{2}\in\LoiqNOb_{b}(\tau)$ in NNF,
$\sigma_{1},\sigma_{2}\supseteq\tau$ be vocabularies, $\psi_{1}\in\mathcal{\mathcal{\LoiqNObTEXT}}(\sigma_{1})$
and $\psi_{2}\in\mathcal{\mathcal{\LoiqNObTEXT}}(\sigma_{2})$ as guaranteed. Without
loss of generality, $(\sigma_{1}\backslash\tau)\cap(\sigma_{2}\backslash\tau)=\emptyset$.

\begin{enumerate}
\item $\varphi=\varphi_{1}\land\varphi_{2}$: Let $\psi=\psi_{1}\land\psi_{2}$
and $\sigma=\sigma_{1}\cup\sigma_{2}$.
\item $\varphi=\neg\varphi_{1}$: By the assumption that that $\varphi$
is in NNF, $\varphi_{1}$ is of the form $(C\sqsubseteq D)$. Let
$o$ be a fresh nominal which does not occur in $\sigma_{1}$. Let
$\sigma=\sigma_{1}\cup\{o\}$. Let $\psi=(o\sqsubseteq C)\land(D\sqsubseteq\neg o)$.
\item $\varphi=\varphi_{1}\lor\varphi_{2}$. Let $r$ be a fresh role and
$o_{1},o_{2},o_{X},o_{Y}$ be fresh nominals.
\begin{eqnarray*}
\psi_{prep} & = & (o_{X}\sqsubseteq\neg o_{Y})\land(o_{1}\sqsubseteq\neg o_{2})\land(o_{X}\sqcup o_{Y}\equiv o_{1}\sqcup o_{2})\land\\
 &  & (\exists r.o_{X}\equiv\top)\land(\exists r.o_{Y}\equiv\bot)
\end{eqnarray*}
For a structure $\mathcal{M}$ with universe $M$, $\mathcal{M}\models\psi_{prep}$
iff

\begin{enumerate}
\item $o_{X}^{\mathcal{M}}\not=o_{Y}^{\mathcal{M}}$
\item $o_{1}^{\mathcal{M}}\not=o_{2}^{\mathcal{M}}$
\item $o_{1}^{\mathcal{M}}=o_{X}^{\mathcal{M}}$ and $o_{2}^{\mathcal{M}}=o_{Y}^{\mathcal{M}}$, or $o_{1}^{\mathcal{M}}=o_{Y}^{\mathcal{M}}$
and $o_{2}^{\mathcal{M}}=o_{X}^{\mathcal{M}}$.
\item $(\exists r.o_{1})^{\mathcal{M}}=M$ and $(\exists r.o_{2})^{\mathcal{M}}=\bot$,
or

$(\exists r.o_{1})^{\mathcal{M}}=\bot$ and $(\exists r.o_{2})^{\mathcal{M}}=M$.

\end{enumerate}

For $i\in\{1,2\}$, let $\theta_{i}$ be the formula obtained from
$\varphi_{i}$ by replacing every atomic formula $C\sqsubseteq D$
with $C\sqcap\exists r.o_{i}\sqsubseteq D\sqcap\exists r.o_{i}$.
Let $\sigma=\sigma_{1}\cup\sigma_{2}\cup\{r,o_{1},o_{2},o_{X},o_{Y})$.
Let $\psi=\psi_{prep}\land\theta_{1}\land\theta_{2}$. The desired
property follows directly from the claim:
\begin{claim}
Let $\mathcal{N}$ be a $\sigma$-structure such that $\mathcal{N}\models\psi_{prep}$,
and let $\mathcal{M}_{\mathcal{N}}$ be the substructure of $\mathcal{N}$ which corresponds
to $\tau$.
\begin{enumerate}
\item If $(\exists r.o_{1})^\mathcal{N}=M$, then $\mathcal{N}\models\psi$ iff $\mathcal{M}_{\mathcal{N}}\models\varphi_{1}$.
\item If $(\exists r.o_{1})^\mathcal{N}=\emptyset$, then $\mathcal{N}\models\psi$ iff
$\mathcal{M}_{\mathcal{N}}\models\varphi_{2}$. \end{enumerate}
\begin{proof}
~\end{proof}
\begin{enumerate}
\item Let $\mathcal{N}$ be a $\sigma$-structure such that $(\exists r.o_{1})^\mathcal{N}=M$.
For every atomic formula $C\sqsubseteq D$ in $\varphi_{1}$, $(C\sqcap\exists r.o_{1})^\mathcal{N}=C^\mathcal{N}\cap M=C^\mathcal{N}$
and $(D\sqcap\exists r.o_{1})^\mathcal{N}=D^\mathcal{N}\cap M=D^\mathcal{N}$. Hence,
$\mathcal{M}_{\mathcal{N}}\models C\sqsubseteq D$ iff $\mathcal{N}\models C\sqcap\exists r.o_{1}\sqsubseteq D\sqcap\exists r.o_{1}$.
By construction of $\theta_{1}$, $\mathcal{M}\models\varphi_{1}$ iff $\mathcal{N}\models\theta_{1}$.

For every atomic formula $C\sqsubseteq D$ in $\varphi_{2}$, $(C\sqcap\exists r.o_{2})^\mathcal{N}=C^\mathcal{N}\cap\emptyset=\emptyset$
and $(D\sqcap\exists r.o_{2})^\mathcal{N}=D^\mathcal{N}\cap\emptyset=\emptyset$.
Hence, $\mathcal{N}\models C\sqcap\exists r.o_{2}\sqsubseteq D\sqcap\exists r.o_{2}$.
Since $\theta_{2}$ is a negation free Boolean combination of atomic
formulae, $\mathcal{N}\models\theta_{2}$.

\item This case is symmetric to the previous case. Let $\mathcal{N}$ be a $\sigma$-structure
such that $(\exists r.o_{1})^\mathcal{N}=\emptyset$. Then $(\exists r.o_{2})^\mathcal{N}=M$.
For every atomic formula $C\sqsubseteq D$ in $\varphi_{2}$, $(C\sqcap\exists r.o_{2})^\mathcal{N}=C^\mathcal{N}\cap M=C^\mathcal{N}$
and $(D\sqcap\exists r.o_{2})^\mathcal{N}=D^\mathcal{N}\cap M=D^\mathcal{N}$. Hence,
$\mathcal{M}\models C\sqsubseteq D$ iff $\mathcal{N}\models C\sqcap\exists r.o_{2}\sqsubseteq D\sqcap\exists r.o_{2}$.
By construction of $\theta_{2}$, $\mathcal{M}_{\mathcal{N}}\models\varphi_{2}$ iff
$\mathcal{N}\models\theta_{2}$.

For every atomic formula $C\sqsubseteq D$ in $\varphi_{1}$, $(C\sqcap\exists r.o_{1})^\mathcal{N}=C^\mathcal{N}\cap\emptyset=\emptyset$
and $(D\sqcap\exists r.o_{1})^\mathcal{N}=D^\mathcal{N}\cap\emptyset=\emptyset$.
Hence, $\mathcal{N}\models C\sqcap\exists r.o_{1}\sqsubseteq D\sqcap\exists r.o_{1}$.
Since $\theta_{1}$ is a negation free Boolean combination of atomic
formulae, $\mathcal{N}\models\theta_{1}$.

\end{enumerate}
\end{claim}
\end{enumerate}
\end{description}

\subsection{NEXPTIME decision procedures \label{se:poly}}

The algorithm in Theorem~\ref{th:exp} produces, for a formula $\varphi$, a formula whose size is exponential in the size of $\varphi$.
Most of the constructions along the proof introduce only a polynomial growth, except for the nominals in Definition~\ref{def:ORD} and the formulae that use them.
We discuss here how to effectively compute an $\mathcal{\LoiqNObTEXT}$-formula of polynomial size in $\varphi$, which introduces the required linear ordering of exponential length without use of the nominals.
Since satisfiability in $\mathcal{\LoiqNObTEXT}$ is NEXPTIME-complete \cite{thesis:Tobias01}, so is satisfiability and implication in $\mathcal{ALCQIO}_{b,Re}$.
We sketch the idea first.

In Section~\ref{se:reduce-to-formula} a structure $\mathcal{N} \in \mathrm{ORD}(\varphi)$ with universe $N$ represents a model $\mathcal{M}$ of $\varphi$ with universe $M$ and at the same time also contains useful labelings for $\mathcal{M}$.
Here, we define structures $\mathcal{N}$ which extend $\mathcal{M}$ in a different though similar way.
Let $k = |\{C \mid C \in \varphi \}|$.
We introduce new concepts $P_1,\ldots,P_k$ and use them to require that $O := N \backslash M$ is of size $2^k$ and  that $\ensuremath{\mathit{succ}}$ is interpreted as a successor relation on $O$.
We think of the reflexive-transitive closure of $\ensuremath{\mathit{succ}}^\mathcal{N}$ as $\ensuremath{\mathit{ord}}^\mathcal{N}$ from Definition~ \ref{def:ORD}, but we will not compute $\ensuremath{\mathit{ord}}^\mathcal{N}$ explicitly.
For every binary word $b_1 \ldots b_k$, there will be exactly one element of $O$ in $\bigcap_{i:b_i=1}P_i^\mathcal{N} \cap \bigcap_{i:b_i=0} \neg P_i^\mathcal{N}$.
I.e., $P_i^{\mathcal{M}}$ represents elements whose corresponding binary word has $b_i=1$.
$\ensuremath{\mathit{succ}}^\mathcal{N}$ will be induced by the usual successor relation on binary words of length $k$:
an element $u \in O$ is the successor of $v \in O$ in $\ensuremath{\mathit{succ}}^\mathcal{N}$ iff
there is $\ell$ such that (1) $u$ and $v$ agree on $P_i^\mathcal{N}$, $i > \ell$,
(2) $u \in P_\ell^\mathcal{N}$ and $v \notin P_\ell^\mathcal{N}$ and
(3) $v \in P_i^\mathcal{N}$ and $u \notin P_i^\mathcal{N}$, $i<\ell$.
Similarly as in Definition~ \ref{def:ORD}, the functions $f_{h'}^\mathcal{N}$ need to be useful labelings, using $O$ for the numbers $[1,2^k]$ and $(\ensuremath{\mathit{succ}}^\mathcal{N})^{*}$ for the linear order on natural numbers in Definition~\ref{def:useful-labeling}.
Importantly, we do not define the transitive closure $\left(\ensuremath{\mathit{succ}}^\mathcal{N}\right)^{*}$ explicitly.
Instead, we exploit the fact that $b_{y}\ldots b_{1}$ is less than $d_{y}\ldots d_{1}$ iff there exists an index $i$ such that $b_{y}\ldots b_{i+1}=d_{y}\ldots d_{i+1}$, $b_{i}=0$ and $d_{i}=1$.

\begin{definition}
\label{def:ORD-exp}
Let $\varphi$ be a $\LoiqNOb_{b}$ formula over vocabulary $\tau$.
Let $k = |\{C \mid C \in \varphi \}|$.
We define an extended vocabulary $\ensuremath{\mathit{ext}}(\tau)$ that extends $\tau$ with new atomic concepts $M, P_1,\ldots,P_k$, a new nominal $o_\ensuremath{\mathit{start}}$, and new atomic functional roles $\ensuremath{\mathit{succ}}, f_1,\ldots, f_h$.

Let $\mathcal{N}$ be a $\ensuremath{\mathit{ext}}(\tau)$-structure with universe $N$.
We denote the substructure of $\mathcal{N}$ with universe $M^\mathcal{N}$ by $\mathcal{M}$.
We denote the set $N \setminus M^\mathcal{N}$ by $\ensuremath{O}^\mathcal{N}$.
We denote by $\ensuremath{\mathit{eval}}: \ensuremath{O}^\mathcal{N} \rightarrow [1,2^k]$ the function that maps an element $u \in \ensuremath{O}^\mathcal{N}$ to $\ensuremath{\mathit{eval}}(u) = 1 + \sum_{i:u \in P_i^\mathcal{N}} 2^{i-1}$.
We denote by $\left(\ensuremath{\mathit{succ}}^\mathcal{N}\right)^{*}$ the reflexive-transitive closure of $\ensuremath{\mathit{succ}}^\mathcal{N}$.
The structure $\mathcal{N}$ belongs to $\ensuremath{\mathit{ORD}}(\varphi)$ if the following conditions hold:
\begin{enumerate}
\item \label{prop:Mtilde-exp} $\mathcal{M}$ satisfies $\varphi$.
\item \label{prop:partition-exp} We have $\ensuremath{O}^\mathcal{N} = \{o_\ensuremath{\mathit{start}}^\mathcal{N}\} \cup \bigcup_{1 \le i \le k} P_i^\mathcal{N}$.
\item \label{prop:linear-exp}
    $\ensuremath{\mathit{eval}}$ is a bijective function, $\ensuremath{\mathit{eval}}(o_\ensuremath{\mathit{start}}^\mathcal{N}) = 1$, and
    $\ensuremath{\mathit{succ}}(u) = v$ iff $\ensuremath{\mathit{eval}}(u) + 1 = \ensuremath{\mathit{eval}}(v)$ for all $u,v \in \ensuremath{O}^\mathcal{N}$.
\item \label{prop:ftypes-exp} $f_{h'}^\mathcal{N}$ is a function from $A_\ell^\mathcal{M}$ to $\ensuremath{O}^\mathcal{N}$, for every $1 \le {h'} \le h$.
\item \label{prop:ford-exp} $f_{h'}^\mathcal{N}$ is a $h'$-useful labeling for $\mathcal{M}$, using $ \ensuremath{O}^\mathcal{N}$ for the natural numbers $[1,2^k]$ and $\left(\ensuremath{\mathit{succ}}^\mathcal{N}\right)^{*}$ for the order on the natural numbers in Definition~\ref{def:useful-labeling}, for every $1 \le h' \le h$.
\end{enumerate}
\end{definition}

\begin{lemma}
\label{lem:extension-useful-exp}
$\ensuremath{\mathit{ORD}}(\varphi)$ is non-empty iff there is a model $\mathcal{M}$ of $\varphi$ with $h'$-useful labelings for $\mathcal{M}$ for every $1\leq h'\leq h$.
\end{lemma}

\begin{lemma}
\label{lem:definingORD-exp}
For every formula $\varphi \in \LoiqNOb_{b}$ there exists a formula $\ensuremath{\mathit{ext}}(\varphi)$, of size polynomial in $k$, such that $\ensuremath{\mathit{ext}}(\varphi)$ defines $\ensuremath{\mathit{ORD}}(\varphi)$.
\end{lemma}

\begin{proof}
We set $\ensuremath{\mathit{ext}}(\varphi) = \theta^{1} \land \theta^{2} \land \theta^{3} \land \theta^{4} \land \theta^{5a} \land \theta^{5b}$.
$\theta^{X}$ defines the property $X$ in Definition \ref{def:ORD-exp}.
The formulae $\theta^{1}$, $\theta^{4}$ and $\theta^{5a}$ are the same as in the proof of Lemma~\ref{lem:definingORD}.
\begin{itemize}
\item
Let $\theta^{2} = \neg M \equiv o_\ensuremath{\mathit{start}} \sqcup \displaystyle{\bigsqcup_{1 \le i \le k}} P_i$.
$\theta^{2}$ says that $\ensuremath{O}^\mathcal{N} = N \setminus M^\mathcal{N} = \{o_\ensuremath{\mathit{start}}^\mathcal{N}\}  \cup \bigcup_{1 \le i \le k} P_i^\mathcal{N}$.
\item
Let $\theta^{3} = \zeta_{consec} \land \zeta_{first} \land \zeta_{last}$.
$\zeta_{consec}$ expresses that the successor relation mimics the binary words:
two words $b_{k}\ldots b_{1}$ and $d_{k}\ldots d_{1}$ are consecutive in $\ensuremath{\mathit{succ}}$ iff there exists an index $i$ such that $b_{i}\ldots b_{1} = 01^{i-1}$, $d_{i}\ldots d_{1} = 10^{i-1}$, and $b_{k}\ldots b_{i+1}=d_{k}\ldots d_{i+1}$.
We introduce concepts $C_i$, for every $1\leq i\leq k$ (the concepts $C_i$ can be either added as fresh concepts or used as abbreviations; the resulting formula $\zeta_{consec}$ will be of polynomial size in both cases):
\[
\begin{array}{lll}
C_{i} & = & \neg P_{i}\sqcap\exists \ensuremath{\mathit{succ}}.P_{i}\\
C_{<i} & = & {\displaystyle \mybigsqcapDisp_{j<i}\left(P_{j}\sqcap\exists \ensuremath{\mathit{succ}}.\neg P_{j}\right)}\\
C_{>i} & = & {\displaystyle \mybigsqcapDisp_{i<j\leq y}\left(P_{j}\sqcap\exists \ensuremath{\mathit{succ}}.P_{j}\sqcup\neg P_{j}\sqcap\exists \ensuremath{\mathit{succ}}.\neg P_{j}\right)}\\
\zeta_{consec} & = & {\displaystyle (\neg M \sqcap \neg \left( P_{1} \sqcap \cdots \sqcap P_{k} \right) \sqsubseteq}\\
& & \quad \quad \quad \displaystyle{\bigsqcup_{1\leq i\leq k}} C_{<i}\sqcap C_{i}\sqcap C_{>i})
\end{array}
\]
The formulae
\[
    \begin{array}{lll}
    \zeta_{first} & = & o_\ensuremath{\mathit{start}} \equiv \left(\neg P_{1} \sqcap \cdots \sqcap \neg P_{k} \right) \land\\
    & & \quad \quad \quad \exists \ensuremath{\mathit{succ}}^{-}\equiv\neg M \sqcap o_\ensuremath{\mathit{start}}\\
    \zeta_{last} & = & \exists \ensuremath{\mathit{succ}}\equiv\neg M \sqcap \neg \left( P_{1} \sqcap \cdots \sqcap P_{k} \right)
    \end{array}
\]
specify that all elements in $\ensuremath{O}^\mathcal{N}$ except for $(P_{1} \sqcap \cdots \sqcap P_{k})^\mathcal{N}$ have a successor, that all elements except for $o_\ensuremath{\mathit{start}}^\mathcal{N}$ have a predecessor and that $\left(\neg P_{1}\sqcap\cdots\sqcap\neg P_{y}\right)^\mathcal{N}$ contains exactly the single element $o_\ensuremath{\mathit{start}}^\mathcal{N}$.
The above stated facts imply that for every vector $(b_1,\ldots,b_k) \in \{0,1\}^k$ there is exactly one element of $\ensuremath{O}^\mathcal{N}$ in
\[
(\mybigsqcapDisp_{i:b_{i}=1} P_{i} \sqcap \mybigsqcapDisp_{i:b_{i}=0} \neg P_{i})^\mathcal{N}.
\]
\item
We do not define the transitive closure $\left(\ensuremath{\mathit{succ}}^\mathcal{N}\right)^{*}$ explicitly.
Instead, we exploit the fact that $b_{y}\ldots b_{1}$ is less than $d_{y}\ldots d_{1}$ iff there exists an index $i$ such
that $b_{y}\ldots b_{i+1}=d_{y}\ldots d_{i+1}$, $b_{i}=0$ and $d_{i}=1$.
We introduce concepts $E_{h',s,i}^\mathcal{N}$, for every $1 \le h' \le h, s\in S_{h'}$ and $ \in [1,k]$, which will contain all of the elements $u \in M$ such that the types of $u$ and $s^\mathcal{N}(u)$ agree on membership in $P_{i+1}^\mathcal{N},\ldots,P_{y}^\mathcal{N}$, $u\notin P_{i}^\mathcal{N}$ and $s^\mathcal{N}(u)\in P_{i}^\mathcal{N}$ (the concepts $E_{h',s,i}^\mathcal{N}$ can be either added as fresh concepts or used as abbreviations; the resulting formula $\theta^{5b}$ will be of polynomial size in both cases).
\begin{eqnarray*}
E_{h',s,i} & \equiv & \exists f_{h'}.\neg P_{i} \sqcap\exists s.\exists f_{h'}.P_{i} \sqcap \\
& &\mybigsqcapDisp_{i+1\leq j\leq y} \Big( \exists f_{h'}.P_{j}\sqcap\exists s.\exists f_{h'}.P_{j} \sqcup\\
& & \quad \quad \exists f_{h'}.\neg P_{j}\sqcap\exists s.\exists f_{h'}.\neg P_{j}\Big)
\end{eqnarray*}
The formula $\theta^{5b}$ states that for every element $u\in A_{h'}^\mathcal{M}$ with $u \not\in B_{h'}^{\mathcal{M}}$ there is an element $v$ with the same value (i.e., $v$ points to the same element as $u$ via $f_{h'}$) such that $v$ is again in $A_{h'}^{\mathcal{M}}$ and $v$ has a previous element which is smaller than $v$.
$\theta^{5b}$ is the conjunction of
\[
\begin{array}{ll}
\exists f_{h'}^{-}. \neg B_{h'} \sqsubseteq \exists f_{h'}^{-}. \left(\displaystyle{\bigsqcup_{s\in S_{h'}, i \in [1,k]}} \exists s^{-}.E_{h',s,i}\right)
\end{array}
\]
for every $1\leq h'\leq h$.
\end{itemize}
\end{proof}

\begin{theorem}
\label{th:poly} Let $\Phi_{i}=\varphi_{i}\land\bigwedge RE_{i}\land\bigwedge DI_{i}\in\mathcal{ALCQIO}_{b,Re}$
for $i=1,2$.
There are polynomial-time computable $\mathcal{\LoiqNObTEXT}$ formulas
$\eta$ and $\rho$ over an extended vocabulary such that
\begin{enumerate}
\item $\Phi_{1}$ is satisfiable iff $\eta$ is satisfiable.
\item $\Phi_{1}$ implies $\Phi_{2}$ iff $\rho$ is not satisfiable.
\item Satisfiability and implication in $\mathcal{ALCQIO}_{b,Re}$ is NEXPTIME-complete.
\end{enumerate}

\end{theorem}

(1) follows from Lemmas \ref{lem:conn-equiv-semi-conn-plus-useful-ord--},
\ref{lem:semi-def}, \ref{lem:extension-useful-exp} and \ref{lem:definingORD-exp} by setting $\eta = \ensuremath{\mathit{ext}}(\semi{\Phi})$.

(2) follows from (1) similarly to Theorem \ref{th:exp}.

(3): We use here the reduction from $\LoiqNOb_{b}$ to $\mathcal{\LoiqNObTEXT}$ in  Appendix~\ref{app:Loiq_LoiqNOb}.
Satisfiability in $\mathcal{\LoiqNObTEXT}$ is NEXPTIME-complete \cite{thesis:Tobias01}.
Since $\mathcal{ALCQIO}_{b,Re}$ contains $\mathcal{\LoiqNObTEXT}$, and at the same time, satisfiability
and implication of $\mathcal{ALCQIO}_{b,Re}$-formulae are polynomial-time reducible to
$\mathcal{\LoiqNObTEXT}$ satisfiability, (3) holds.

\section{Introduction}
\emph{Description Logics} (\emph{DLs}) are a well established family of logics for Knowledge Representation and Reasoning \cite{bk:Baader2003}.
They model the domain of interest in terms of \emph{concepts} (classes of objects) and \emph{roles} (binary relations between objects).
These features make DLs very useful to formally describe and reason about graph-structured information.
The usefulness of DLs is witnessed e.g.\,by the W3C choosing DLs to provide the logical
foundations to the standard Web Ontology Language (OWL)~\cite{owl2-overview}.
Another application of DLs is formalization and static analysis of UML class diagrams and ER diagrams, which are basic modeling artifacts in object-oriented software development and database design, respectively~\cite{BeCD05,ACKRZ07b}.
In these settings, standard reasoning services provided by DLs can be used to verify e.g.\, the consistency of a diagram.

In complex software projects, the source code is usually accompanied by design documents which provide extensive documentation and models of data structure content (e.g., using UML and ER diagrams).
This documentation is both an opportunity and a challenge for program verification.
However, the verification community has focused mostly on a bottom-up approach to the analysis of programs with dynamic data structures, which examines pointers and the shapes induced by them.
It is therefore a compelling question, if DLs can be used to model and verify richer properties of dynamic data structures.

A promising framework for shape analysis based on description logics was developed in \cite{georgieva2005description}.
\cite{georgieva2005description} is based mostly on
an extension of $\mathcal{\LoiqNObTEXT}$ with fixed points.
$\mathcal{\LoiqNObTEXT}$ is itself the extension of $\mathcal{ALC}$ with nominals, number restrictions and inverses, see e.g. \cite{DBLP:conf/aaai/BaaderLMSW05}.
$\mathcal{ALC}$ is a syntactic variant of the multimodal logic $K_m$~\cite{DBLP:journals/ai/Schmidt-SchaussS91,Schild91acorrespondence}.
$\mathcal{\LoiqNObTEXT}$ already fulfills most of the requirements for describing the memory of programs with dynamic data structures:
(i) nominals allow to represent the program's variables;
(ii) number restrictions allow to model the program's pointers by functions;
(iii) inverses allow to define the incoming pointers for data structure elements, e.g., in a tree every tree element must have at most one parent.
Additionally, it needs to be ensured that data structures only contain elements \emph{reachable} from program variables via program pointers (iv).
Reachability is expressible in $\mu \mathcal{\LoiqNObTEXT}$, the extension of $\mathcal{\LoiqNObTEXT}$ with fixed points, but not in $\mathcal{\LoiqNObTEXT}$.

The main disadvantage of \cite{georgieva2005description} is that finite satisfiability and implication of $\mu \mathcal{\LoiqNObTEXT}$ formulas
is undecidable \cite{ar:BonattiPeron2004}.
No extensions of $\mathcal{\LoiqNObTEXT}$ with reachability or transitive closure
were known to be decidable on finite structures.

{\em Our contribution: }
We introduce
and develop decision procedures over finite structures
for the logic $\mathcal{ALCQIO}_{b,Re}$, which extends the closure ($\LoiqNOb_{b}$) of $\mathcal{\LoiqNObTEXT}$
under Boolean operations with reachability assertions.
The reachability assertions guarantee that elements of the universe of a model are reachable in the graph-theoretic sense from initial sets of elements using prescribed sets of binary relation symbols.
Alternatively, we can think of $\mathcal{ALCQIO}_{b,Re}$ as $\LoiqNOb_{b}$ interpreted over structures containing an unbounded number of binary trees.

The main results of this paper are algorithms which decide the finite satisfiability and finite implication problems of $\mathcal{ALCQIO}_{b,Re}$.
The algorithms are reductions to finite satisfiability in $\mathcal{\LoiqNObTEXT}$, which suggests relatively simple implementation using existing $\mathcal{\LoiqNObTEXT}$ reasoners.
The algorithms run in NEXPTIME, which is optimal since $\mathcal{\LoiqNObTEXT}$ is already NEXPTIME-hard.

{\em A description logic for shape analysis.}
The logic $\mathcal{ALCQIO}_{b,Re}$ we introduce is especially well-suited to shape analysis, since $\mathcal{ALCQIO}_{b,Re}$ contains
nominals, number restrictions, inverses and reachability.
$\mathcal{ALCQIO}_{b,Re}$ is a flexible and powerful formalism for describing complex data structures with sharing.
This, together with the existence of a decision procedure for implication and not just satisfiability, makes $\mathcal{ALCQIO}_{b,Re}$ a promising candidate for software verification applications.

We discuss in Section \ref{se:examples} that $\mathcal{ALCQIO}_{b,Re}$ is strong enough to describe e.g. lists, trees and lists of trees, etc.
$\mathcal{ALCQIO}_{b,Re}$ supports programs with sharing, in which memory cells (which in model-theoretic terms are elements of the universe of the model) may participate in multiple data structures.
In particular, we show that $\mathcal{ALCQIO}_{b,Re}$ supports modular reasoning:
Our results support composition of data structures with disjoint domains, as well as composition of data structures whose domains are not disjoint, but have disjoint pointers.

The closure of the underlying logic $\LoiqNOb_{b}$ under Boolean operations allows to describe conditional statements in programs.
The decision procedure for implication for $\mathcal{ALCQIO}_{b,Re}$ is essential for verification applications, since it allows to show that specifications relating pre- and post-conditions are correct.
We demonstrate the usefulness of $\mathcal{ALCQIO}_{b,Re}$ by giving a Hoare-style correctness proof for an example pointer-manipulating program in Section~\ref{se:verification}.
We leave the development of a full Hoare-style verification framework for future work.

\paragraph{Related Work.}
We discuss further related work in the following.

\emph{Separation Logic.}
In the last decade, the leading approach for shape analysis has been separation logic~\cite{pr:Reynolds02}.
While separation logic has a strong proof-theoretic tradition - in origin and in proof techniques used, model-theoretic approaches have been less prominent.
We believe that recent advances in finite model theory have created an opportunity for the development of new model-theoretic approaches to shape analysis.
In this paper, we explore this model-theoretic line of research building on previous results on description logics.

\emph{Description logics and reachability. }
Description logics extended with various forms of reachability have been studied in the literature, though the focus is mostly on arbitrary
rather than finite structures.
The important work of Schild~\cite{Schild91acorrespondence} exposed a correspondence between variants of propositional dynamic logic (PDL), a logic for reasoning about program behavior, and variants of DLs extended with further role constructors, e.g.\,the transitive closure of a role.
Close correspondences between DLs extended with fixpoints and variants of the $\mu$-calculus have also been identified~\cite{DBLP:conf/kr/Schild94,DBLP:conf/ecai/GiacomoL94}.
Recently, extensions of DLs with regular expressions over roles have been proposed~\cite{calv-etal-09}.
DLs with transitive roles and counting quantifiers were studied in  \cite{KSZ07,schroder2008many}.
\cite{pr:DLC13} proved decidability over arbitrary structures for a DL with transitive closure and counting quantifiers.

{\em The two-variable fragment.}
Our results bear similarity with a recent deep result~\cite{pr:CharatonikWitkowski13} based on \cite{ar:PrattHartmann2005}.
There, the complexity of finite satisfiability of the two-variable fragment of first order logic extended with counting quantifiers ($C^{2}$) and additionally with two forests ($CT^{2}$) is studied.

The results in our paper and in \cite{pr:CharatonikWitkowski13} are incomparable due to differences in several orthogonal aspects.
(i) $C^{2}$ strictly contains $\LoiqNOb_{b}$.
(ii) $CT^{2}$ is restricted to at most two forests, whereas $\mathcal{ALCQIO}_{b,Re}$ allows an unbounded number of reachability conditions.
The decidability of the extension of $C^{2}$ with three successor relations is not known, while extending $\LoiqNOb_{b}$ with three successor relations is covered by our results.
(iii) we have a decision procedure for implication in $\mathcal{ALCQIO}_{b,Re}$, while no such decision procedure is given for $CT^{2}$ in \cite{pr:CharatonikWitkowski13}.
(iv) to our knowledge, no reasoners for $C^{2}$ exist; the sophisticated construction in \cite{pr:CharatonikWitkowski13} makes the worthy task of implementing a reasoner for $CT^{2}$ a considerable challenge.
In contrast, our result reduces reasoning in $\mathcal{ALCQIO}_{b,Re}$ to satisfiability in $\mathcal{\LoiqNObTEXT}$, which is contained in the description logic $\mathcal{SROIQ}$ for which several reasoners have been implemented, e.g., \cite{pellet,fact,hermit}.

Due to the intricate nature of the proof in \cite{pr:CharatonikWitkowski13}, the exact relationship between our result and that of \cite{pr:CharatonikWitkowski13} is difficult to ascertain.
It would be beneficial in future work to understand whether these results can be united within a natural logic containing both $CT^{2}$ and $\mathcal{ALCQIO}_{b,Re}$.

\begin{comment}
Both $\mathcal{ALCQIO}_{b,Re}$ and $CT^{2}$ allow an unbounded number of binary relations.
\end{comment}

\emph{Shape Analysis and Content Verification.}
In a recent paper~\cite{arXiv:CKSVZ13} the use of a DL to reason and verify correctness of entity-relations-type content of data structures on top of an existing shape analysis is discussed.
Technically, \cite{arXiv:CKSVZ13} is based on a reduction of a DL to satisfiability in $CT^{2}$.
The DL in \cite{arXiv:CKSVZ13} cannot express reachability and the approach there depends on a combination of DL with an existing shape analysis.
We believe the method of \cite{arXiv:CKSVZ13} can be modified to be based on $\mathcal{ALCQIO}_{b,Re}$ alone.
Exploration of this question is part of future work.

\section{The Formalism and Examples}

From the point of view of finite model theory, $\LoiqNOb_{b}$ and $\mathcal{ALCQIO}_{b,Re}$
are syntactic variants of fragments of first or second order logic.
In description logics terminology, binary relation symbols are called
{\em atomic roles}, unary relation symbols are called {\em atomic concepts},
and constant symbols are called {\em nominals}. Let $\mathsf{N_{R}}$, $\mathsf{N_{C}}$
and $\mathsf{N_{n}}$ denote the sets of atomic roles, atomic concepts and nominals.
A vocabulary $\tau$ is then the union of $\mathsf{N_{R}}$, $\mathsf{N_{C}}$ and $\mathsf{N_{n}}$.
Let $\mathsf{N_{F}}\subseteq\mathsf{N_{R}}$ be a set of atomic roles. The roles in $\mathsf{N_{F}}$
are called {\em functional}.

Formulae are built from the symbols in $\tau$. The various constructors
available to build formulae determine the particular DL,
giving rise to a wide family of logics with varying expressivity,
and decidability and complexity of reasoning. The semantics to formulae
is given in terms of structures, where atomic concepts and atomic
roles are interpreted as unary and binary relations in a structure,
respectively, and constants are interpreted as elements in the structure's
universe.
We now define $\LoiqNOb_{b}$ and $\mathcal{ALCQIO}_{b,Re}$.
See Section \ref{se:examples} for examples.
\begin{definition}
[Syntax of $\LoiqNOb_{b}$] The set of \emph{roles},\emph{ concepts} and\emph{
formulae} of $\LoiqNOb_{b}$ are defined inductively:
\begin{itemize}
\item Atomic concepts and nominals are concepts; Atomic roles are roles;
\item If $r$ is a role, $C,D$ are concepts and $n$ is a positive integer,
then $C\sqcap D$, $C\sqcup D$, $\neg C$, $\exists r.C$ and $\exists^{\leq n}\, r.C$
are concepts, and $r^{-}$ is a role;
\item $C\sqsubseteq D$ (\emph{concept inclusion}) and $C\equiv D$ (\emph{concept equality}) where $C,D$ are concepts,
are formulae;
\item If $\varphi$ and $\psi$ are formulae, then $\varphi\land\psi$,
$\varphi\lor\psi$, and $\neg\psi$ are formulae.
\end{itemize}
\end{definition}
The sub-logic $\mathcal{\LoiqNObTEXT}\subseteq \LoiqNOb_{b}$ does not allow negations and disjunctions.

A \emph{structure} (or \emph{interpretation}) is a tuple $\mathcal{M}=(M,\tau,\cdot)$,
where $M$ is a finite set (the \emph{universe}), $\tau$ is a set
of \emph{constants} and unary and binary \emph{relation symbols} (\emph{the
vocabulary}), and $\cdot$ is an \emph{interpretation function}, which
assigns to each constant $c\in\tau$ an element $c^{\mathcal{M}}\in M$, and
to each $n$-ary relation symbol $R\in\tau$ an $n$-ary relation
$R^{\mathcal{M}}$ over $M$. In this paper, each relation is either unary
or binary (i.e. $n\in\{1,2\}$). In this paper, all structures are
finite. Satisfiability and implication always refer to finite structures
only.
\begin{definition}
[Semantics of $\LoiqNOb_{b}$ ]
The semantics of an $\LoiqNOb_{b}(\tau)$-formula $\varphi$ is given in terms of $\tau$-structures such that every $f\in\mathsf{N_{F}}$, $f^{\mathcal{M}}$ is a partial function.
\begin{comment}
\footnote{If $f\in\mathsf{N_{F}}$ then, whenever $\{(e,e_{1}),(e,e_{2})\}\subseteq f^{\mathcal{M}}$
we have $e_{1}=e_{2}$.}
\end{comment}
The function $\cdot^{\mathcal{M}}$ is extended to the remaining concepts and roles inductively below.
The satisfaction relation $\models$ is also given below.
If $\mathcal{M}\models\varphi$, then $\mathcal{M}$ is a \emph{model} of $\varphi$.
We write $\psi\models\varphi$ and say that $\psi$ implies $\varphi$ if every model of $\psi$ is also a model of $\varphi$.
\[
\begin{array}{llllll}
(C\sqcap D)^{\mathcal{M}} & = & C^{\mathcal{M}}\cap D^{\mathcal{M}} \\
(C\sqcup D)^{\mathcal{M}} & = & C^{\mathcal{M}}\cup D^{\mathcal{M}} \\
(\neg C)^{\mathcal{M}} & = & M\setminus C^{\mathcal{M}} \\

(r^{-})^{\mathcal{M}} & = & \{(e,e')\mid (e',e)\in r^{\mathcal{M}})\}\\
(\exists r.C)^{\mathcal{M}} & = & \{e\mid\exists e':(e,e')\in r^{\mathcal{M}},\,e'\in C^\mathcal{M}\}\\
(\exists^{\leq n}r.C)^{\mathcal{M}} & = & \{e\mid\exists^{\leq n}e':(e,e')\in r^{\mathcal{M}},\,e'\in C^\mathcal{M}\}\\

\mathcal{M}\models C\sqsubseteq D & \mathrm{if} & C^{\mathcal{M}}\subseteq D^{\mathcal{M}} \\
\mathcal{M}\models\varphi\land\psi & \mathrm{if} & \mathcal{M}\models\varphi~\mathrm{and}~\mathcal{M}\models\psi\\
\mathcal{M}\models\neg\varphi & \mathrm{if} & \mathcal{M}\not\models\varphi\\
\mathcal{M}\models\varphi\lor\psi & \mathrm{if} & \mathcal{M}\models\varphi~\mathrm{or}~\mathcal{M}\models\psi
\end{array}
\]

\end{definition}
We will use the following abbreviations.
$\top=C\sqcup \neg C$, where $C$ is an arbitrary atomic concept and $\bot=\neg \top$;
$\alpha \equiv \beta$ for the formula $\alpha\sqsubseteq \beta\land \beta\sqsubseteq \alpha$;
$\exists r$ for the concept $\exists r.\top$;
$\exists^{= n}r.C$ for the concept $\exists^{\leq n}r.C \sqcap \neg \exists^{\leq n-1}r. C$;
Note that $\top^\mathcal{M}=M$ and $\bot^\mathcal{M}=\emptyset$ for any structure $\mathcal{M}$ with universe $M$.
For a formula $\varphi$, we denote by $|\varphi|$ the length of $\varphi$ as a string.

For $\mathcal{ALCQIO}_{b,Re}$, we define two new types of assertions.
\begin{description}
\item [{Reachability~Assertion}] $\Reacha{B}{S}{A}$ where $A,B\in\mathsf{N_{C}}$
and $S\subseteq\mathsf{N_{F}}$.
Intuitively, it says that $B$ is contained in $A$ and that $A$ is a set of elements reachable from $B$, without leaving $A$, through the roles of $S$.
\item [{Disjointness~Assertion}] $Disj(A_{1},A_{2})=(A_{1}\sqcap A_{2}\equiv\bot)$
for $A_{1},A_{2}\in\mathsf{N_{C}}$\textit{.}
\end{description}
Let $RE$ and $DI$ be sets of reachability respectively disjointness
assertions.
\begin{description}
\item [{Compatibility}] $RE$ and $DI$ \emph{compatible }if for every
$\Reacha{B_{1}}{S_{1}}{A_{1}}$ and $\Reacha{B_{2}}{S_{2}}{A_{2}}$
in $RE$ such that $S_{1}\cap S_{2}\not=\emptyset$, $Disj(A_{1},A_{2})$
is in $DI$.
\end{description}

\begin{definition}
[Syntax of $\mathcal{ALCQIO}_{b,Re}$]  $\Phi=\phi\land\bigwedge RE\land\bigwedge DI$ is an $\mathcal{ALCQIO}_{b,Re}$-formula if

 \begin{enumerate}[(A)]
\item $\phi \in \LoiqNOb_{b}$
\item $RE$ is a set of reachability assertions
\item $DI$ is a set of disjointness assertions
\item $RE$ and $DI$ are compatible
\end{enumerate}
The set of {\em containment assertions}
\[CO(RE)=\left\{ B\sqsubseteq A\mid \Reacha{B}{S}{A}\in RE\right\}\,.\]
\end{definition}

\begin{definition}
[Semantics of $\mathcal{ALCQIO}_{b,Re}$]
Let $\Phi=\phi\land\bigwedge RE\land\bigwedge DI\in\mathcal{ALCQIO}_{b,Re}$.
Let $\formula{\Phi} = \phi \land \bigwedge CO(RE) \land  DI$ be the $\LoiqNOb_{b}$ formula associated to $\Phi$.

For every $\beta=\Reacha{B}{S}{A}\in RE$ and $\tau$-structure $\mathcal{M}$,
let $D_{\beta}^{\mathcal{M}}$ be the directed subgraph $\left\langle M,\bigcup_{s\in S}s^{\mathcal{M}}\right\rangle$ induced by $A^{\mathcal{M}}$; we call $D_{\beta}^{\mathcal{M}}$ \emph{connected}, if every vertex of $D_{\beta}^{\mathcal{M}}$ is reachable from a vertex of $B^{\mathcal{M}}$.

For every $\tau$-structure $\mathcal{M}$, $\mathcal{M}\models\Phi$ if $\mathcal{M} \models \formula{\Phi}$ (in $\LoiqNOb_{b}$ semantics) and $D_{\beta}^{\mathcal{M}}$ is connected for every $\beta = \Reacha{B}{S}{A}\in RE$.
\end{definition}

\paragraph{Comment 1:}
For illustration purposes, we state an equivalent definition of the semantics of $\mathcal{ALCQIO}_{b,Re}$ in the following:
Let $*$ denote the reflexive-transitive closure, $\circ$ denote role composition,
$R^\mathcal{M} = (\bigcup_{s\in S}s^{\mathcal{M}}\cap A^{\mathcal{M}}\times A^{\mathcal{M}})^*$ and
$R^\mathcal{M}(B^\mathcal{M}) = \{ v \mid \exists (u,v)\in R^\mathcal{M}.\, u\in B^\mathcal{M}\}$.
We have $\mathcal{M}\models\Phi$ iff $\mathcal{M} \models \formula{\Phi}$ and $R^\mathcal{M}(B^\mathcal{M}) = A^M$ for every $\beta = \Reacha{B}{S}{A}\in RE$.

\paragraph{Comment 2:}
The motivation for $CO(RE)$ is to guarantee that data structures over the same roles
have disjoint domains (see {\em Compositionality 1} in the examples).

\subsection{Examples} \label{se:examples}

\paragraph{List-segments and successor relations.}
Given a concept $L$, a nominal $\mathit{head}$ and a functional role $\mathit{next}$,
$L^{\mathcal{M}}$ is a singly-linked list-segment from $\mathit{head}^{\mathcal{M}}$ via $\mathit{next}^{\mathcal{M}}$,
if the directed subgraph of $\left\langle M,\mathit{next}^{\mathcal{M}}\right\rangle$ induced by $L^{\mathcal{M}}$ is a (potentially cyclic) successor relation.
This can be expressed by the $\mathcal{ALCQIO}_{b,Re}$ formula $\Phi^{\mathit{head},\mathit{next},L}_{List}$ obtained as the conjunction of
$\top\sqsubseteq \top$,
$RE_{l}=\{\Reacha{head}{next}{L}\}$ and $DI_{l}=\emptyset$.
$RE_l$ expresses that $\mathit{head}^\mathcal{M} \in L^\mathcal{M}$ and all elements of $L^{\mathcal{M}}$
are reachable from $\mathit{head}^{\mathcal{M}}$ via $\mathit{next}^{\mathcal{M}}$; $DI_l$ is empty
since we have described no other data structure which could be disjoint
from this list.
$\Phi^{\mathit{head},\mathit{next},L}_{List}$ does not determine where the $\mathit{next}$ role of the last
element of the list points. Acyclic and cyclic list-segments are defined as follows:
$\Phi^{\mathit{head},\mathit{next},L}_{aList} = \Phi^{\mathit{head},\mathit{next},L}_{List} \land \neg(L\sqsubseteq \exists next)$
and
$\Phi^{\mathit{head},\mathit{next},L}_{cList} = \Phi^{\mathit{head},\mathit{next},L}_{List} \land
(\mathit{head}\sqsubseteq \exists \mathit{next}^-.L)$.

\paragraph{$d$-ary trees.}
Given a concept $T$, a nominal $\mathit{root}$ and functional roles $\mathit{left}$
and $\mathit{right}$, $T^{\mathcal{M}}$ is a binary tree rooted at $root^{\mathcal{M}}$
via $\mathit{left}^{\mathcal{M}}$ and $\mathit{right}^{\mathcal{M}}$ if the directed subgraph of
$\left\langle M,\mathit{left}^{\mathcal{M}}\cup \mathit{right}^{\mathcal{M}}\right\rangle $
induced by $T^{\mathcal{M}}$ is a directed tree rooted at $\mathit{root}^{\mathcal{M}}$ in
the graph-theoretic sense. This can be expressed by the $\mathcal{ALCQIO}_{b,Re}$ formula
$\varPhi_{T}$ obtained as the conjunction of
(a) $\mathit{root} \sqsubseteq \neg\exists \mathit{left}^-.T \sqcap \neg\exists \mathit{right}^-.T$,
(b) $T \sqcap \neg \mathit{root} \sqsubseteq \exists^{= 1}\mathit{left}^{-}.T \sqcap \neg\exists \mathit{right}^{-}.T \sqcup \exists^{= 1}\mathit{right}^{-}.T \sqcap \neg\exists \mathit{left}^{-}.T$,
(c) $RE_{t}=\{\Reacha{root}{\{\mathit{left},right\}}{T}\}$ and (d) $DI_{t}=\emptyset$.
(a) expresses that $\mathit{root}^{\mathcal{M}}$ belongs to $T^{\mathcal{M}}$ and is not
pointed to from $T^{\mathcal{M}}$; (b) expresses that every element of $T^{\mathcal{M}}$
besides the root has exactly one incoming pointer from a $T^{\mathcal{M}}$
element. (c) expresses that $\mathit{root}^{\mathcal{M}}$ belongs to $T^{\mathcal{M}}$ and that all elements of $T^{\mathcal{M}}$ are reachable from $\mathit{root}^{\mathcal{M}}$ via $\mathit{left}^{\mathcal{M}}$ and $\mathit{right}^{\mathcal{M}}$.
The case of $d$-ary trees, $d>2$, is similar, using
$d$ functional roles $child_1,\ldots,child_d$.
We remark that $1$-ary trees correspond to acyclic list-segments.

\paragraph{Compositionality 1.}
$\mathcal{ALCQIO}_{b,Re}$ is closed under taking memory disjoint union of data structures.
E.g. $\mathcal{ALCQIO}_{b,Re}$-formulae $\Phi_i=\varphi_i\land \{\Reacha{B_i}{S_i}{A_i}\}$, $i=1,2$,
the following formula expresses that the domains of its models consist of
two disjoint parts, corresponding to the $\Phi_i$:
$\Phi = \varphi_1\land\varphi_2\land \bigwedge RE\land \bigwedge	 DI$,
where $RE = \{\Reacha{B_i}{S_i}{A_i}\mid i=1,2\}$ and
$DI = \{Disj(A_{1},A_{2})\}$.
There is no disjointness requirement on the roles in $S_1$ and $S_2$.

\paragraph{Compositionality 2.}
$\mathcal{ALCQIO}_{b,Re}$ allows to define multiple data structures which may overlap in memory,
as long as they do not share the same pointers.
E.g. given $\mathcal{ALCQIO}_{b,Re}$-formulae $\Phi_i=\varphi_i\land \{\Reacha{B_i}{S_i}{A_i}\}$, $i=1,2,3$,
such that $S_1$, $S_2$ and $S_3$ are pairwise disjoint,
the following formula expresses that the three data structures are defined simultaneously
with possibly overlapping domain:
$\Phi = \varphi_1\land\varphi_2\land \phi_3\land \bigwedge RE$,
where $RE = \{\Reacha{B_i}{S_i}{A_i} \mid i=1,2,3\}$.
We note that this compositionality property allows us to define three successor relations.

\paragraph{Compositional Data Structures.}
$\mathcal{ALCQIO}_{b,Re}$ allows us to define compositional data structures such as list of lists, list of trees, tree of lists of lists, etc.
For example, let us define an acyclic list of acyclic lists:
Given a concept $L$, a nominal $head$, and functional roles $next_1$
and $next_{2}$, $L^{\mathcal{M}}$ is a acyclic list of acyclic lists from $head^{\mathcal{M}}$
via $next_1^{\mathcal{M}}$ and $next_{2}^{\mathcal{M}}$ if there exists $L_1^\mathcal{M} \subseteq L^{\mathcal{M}}$
such that $L_{1}^{\mathcal{M}}$ is an acyclic list from $var_{1}^{\mathcal{M}}$ via $next_1^{\mathcal{M}}$,
and $L^{\mathcal{M}}$
is a disjoint union of acyclic lists via $next_{2}^{\mathcal{M}}$ whose heads belong to $L_{1}^{\mathcal{M}}$.
This can be expressed by the acyclic list-segment formulae $\Phi^{\mathit{head},\mathit{next_1},L_1}_{aList}$ and $\Phi^{L_1,\mathit{next_2},L}_{aList}$, which can be composed because of disjoint roles in the reachability assertions (see Compositionality 2).

\input{verification.tex}
\input{content.tex}

\input{body-auto.tex}
\input{semi.tex}
\input{nexp.tex}
\input{rhd-proof.tex}

\bibliographystyle{plain}

\section{\label{app:proofs-lem:op-on-concepts} Proof of Lemma \ref{lem:op-on-concepts}}

The proof of (1) proceeds by induction on the construction of the concepts, showing that $C^{\mathcal{M}} = C^{\op{\mathcal{M}}{\mathfrak{t}}}$ for all $C\in\varphi$.
For ease of notation we write $\mathcal{M}_{1}=\mathcal{M}$ and $\mathcal{M}_{2} = \op{\mathcal{M}}{\mathfrak{t}}$.
\begin{enumerate}
\item If $A\in\mathsf{N_{C}}$, then $A^{\mathcal{M}_{1}} = A^{\mathcal{M}_{2}}$ since none of the atomic concepts change between $\mathcal{M}_{1}$ and $\mathcal{M}_{2}$.
\item If $o\in\mathsf{N_{n}}$, then similarly, there is no change.
\item If $C_{1}$ and $C_{2}$ are concepts satisfying the induction hypothesis, then $C_{1} \sqcap C_{2}$, $C_{1} \sqcup C_{2}$ and $\neg C_{1}$ also satisfy the claim, e.g.,
    $(C_{1} \sqcap C_{2})^{\mathcal{M}_{1}} = C_{1}^{\mathcal{M}_{1}} \cap C_{2}^{\mathcal{M}_{1}} =
     C_{1}^{\mathcal{M}_{2}} \cap C_{2}^{\mathcal{M}_{2}} = (C_{1} \sqcap C_{2})^{\mathcal{M}_{2}}$.
\item For a role $s$, a concept $C$ and a non-negative integer $n$, we consider the concepts $\exists s.C$, $\exists^{\leq n} s.C$, $\exists s^{-}.C$ and $\exists^{\leq n} s^{-}.C$:

    \begin{enumerate}
    \item If $s\not=r$, then $\left(\exists s.C^{\mathcal{M}_{1}}\right) = \left(\exists s.C\right)^{\mathcal{M}_{2}}$ since $s^{\mathcal{M}_{1}}=s^{\mathcal{M}_{2}}$ and by induction $C^{\mathcal{M}_{1}} = C^{\mathcal{M}_{2}}$.
        Similarly, this holds for $\exists^{\leq n} s.C$, $\exists s^{-}.C$ and $\exists^{\leq n} s^{-}.C$.
    \item If $s=r$:
    \begin{itemize}
    \item $\exists r.C$ and $\exists^{\leq n} s.C$:
        We fix some $i \in \{0,1\}$.
        We have $a_i \in \left(\exists r.C\right)^{\mathcal{M}_{1}}$ iff
        $a_{i-1} \in \left(\exists r.C\right)^{\mathcal{M}_{1}}$
        (by $\overline{tp}_{\mathcal{M}_{1}}^{\varphi}(a_{0}) = \overline{tp}_{\mathcal{M}_{1}}^{\varphi}(a_{1})$)
        iff there is a $b$ such that $(a_{i-1},b) \in r^{\mathcal{M}_{1}}$ and $b \in C^{\mathcal{M}_{1}}$
        iff there is a $b$ such that $(a_{i-1},b) \in r^{\mathcal{M}_{1}}$ and $b \in C^{\mathcal{M}_{2}}$ (by induction assumption) iff
        iff there is a $b$ such that $(a_i,b) \in r^{\mathcal{M}_{2}}$ and $b \in C^{\mathcal{M}_{2}}$ (by the definition of the operation $\rhd$) iff
        $a_i \in \left(\exists r.C\right)^{\mathcal{M}_{2}}$.
        Since the only difference between $\mathcal{M}_{1}$ and $\mathcal{M}_{2}$ are the values of $r^{\mathcal{M}_{i}}$ on $a_{0}$ and $a_{1}$, we have $\left(\exists r.C\right)^{\mathcal{M}_{1}} = \left(\exists r.C\right)^{\mathcal{M}_{2}}$
        and $\left(\exists^{\leq n} r.C\right)^{\mathcal{M}_{1}} = \left(\exists^{\leq n} r.C\right)^{\mathcal{M}_{2}}$.
    \item $\exists r^{-}.C$ and $\exists^{\leq n} r^{-}.C$:
        For every $u\in M$, $i=1,2$, we define
        \[
            S_{i}(u)=\left\{ v\mid(u,v)\in\left(r^{-}\right)^{\mathcal{M}_{i}}\mbox{ and }v\in C^{\mathcal{M}_{i}}\right\}
        \]
        We fix some $u\in M$.
        We have $v\in S_{1}(u)$ iff $v\in S_{2}(u)$ for every $v \notin \{a_{0},a_{1}\}$, using that $(u,v) \in  \left(r^{-}\right)^{\mathcal{M}_{1}}$
        iff $(u,v) \in \left(r^{-}\right)^{\mathcal{M}_{2}}$ and that by induction $C^{\mathcal{M}_{1}}=C^{\mathcal{M}_{2}}$.
        %
        We now consider $v \in \{a_{0},a_{1}\}$:
        We have $a_{i} \in S_{1}(u)$
        iff $(a_{i},u) \in r^{\mathcal{M}_{1}}$ and $a_{i}\in C^{\mathcal{M}_{1}}$
        iff $(a_{i},u) \in r^{\mathcal{M}_{1}}$ and $a_{i-1}\in C^{\mathcal{M}_{1}}$ (because $\overline{tp}_{\mathcal{M}_1}^{\varphi}(a_{0}) = \overline{tp}_{\mathcal{M}_1}^{\varphi}(a_{1})$)
        iff $(a_{i-1},u) \in r^{\mathcal{M}_{2}}$ and $a_{i-1}\in C^{\mathcal{M}_{1}}$ (by the definition of the operation $\rhd$)
        iff $(a_{i-1},u)\in r^{\mathcal{M}_{2}}$ and $a_{i-1}\in C^{\mathcal{M}_{2}}$ (by induction assumption)
        iff $a_{i-1}\in S_{2}(u)$.
        So, $|S_{1}(u)| = |S_{2}(u)|$.
        Therefore, $u \in (\exists r^{-}.C)^{\mathcal{M}_{1}}$ iff $u \in (\exists r^{-}.C)^{\mathcal{M}_{2}}$ and $u \in (\exists^{\leq n} r^{-}.C)^{\mathcal{M}_{1}}$ iff $u \in (\exists^{\leq n} r^{-}.C)^{\mathcal{M}_{2}}$, $i=1,2$.
    \end{itemize}
\end{enumerate}
\end{enumerate}
We turn to the two conclusions:
\begin{enumerate} [(2)]
    \item We get directly that for every $u\in M$, $\overline{tp}_{\mathcal{M}}^{\varphi}(u) = \overline{tp}_{\op{\mathcal{M}}{\mathfrak{t}}}^{\varphi}(u)$.
\end{enumerate}
\begin{enumerate} [(3)]
    \item Follows using Lemma~\ref{lem:types}.
\end{enumerate}

\subsection{\label{app:useful-proof} \label{app:proofs} Applying $\rhd$ leads to Standard Models}

In the proof of Lemma \ref{lem:connected-implies-useful-order--} we have shown how to turn non-standard models
into standard models by repeated aplications of $\rhd$ and based on Lemma \ref{lem:rhd-connectedness--}, which we prove here.

\begin{proof}[Proof of Lemma~\ref{lem:rhd-connectedness--}]
We assume $\mathit{val}(D_{h'}^{\mathcal{M}}) > 0$.
Let $X$ be a base for $D_{h'}^{\mathcal{M}}$ such that $\mathit{val}(X) = \mathit{val}(D_{h'}^{\mathcal{M}})$.
Because of $\mathit{val}(D_{h'}^{\mathcal{M}}) > 0$, there is a base element $a_{1} \in X$ with $a_{1} \not\in B_{h'}^\mathcal{M}$.
By the $h'$-usefulness of $f_{h'}$, there are
$a_0,w\in A_{h'}^{\mathcal{M}}$ such that $f_{h'}(a_{0}) = f_{h'}(a_1)$, $f_{h'}(w) < f_{h'}(a_0)$ and the graph $D_{h'}^{\mathcal{M}}$ has an edge $(w,a_0)$.

By Lemma~\ref{lem:basis-circle} $a_{1}$ belongs to some cycle $C$ in $D_{h'}^{\mathcal{M}}$.
We denote the successor of $a_1$ in $C$ by $b_{1}$.
Let $r \in \mathsf{N_{F}}$ be the functional role with $(a_1,b_1) \in r^\mathcal{M}$ and $r \in S_{h'}$ (recall that the set $S_{h'}$ belongs to the reachability-assertion $\Reacha{B_{h'}}{S_{h'}}{A_{h'}}$).
We denote the remaining path from $b_1$ to $a_1$ in $C$ by $\pi_{b_1,a_1}$.
We note that $\pi_{b_1,a_1}$ does not contain $a_0$;
otherwise $X' = X \setminus \{a_1\} \cup \{w\}$ would be a basis for $D_{h'}^{\mathcal{M}}$ with $\mathit{val}(D_{h'}^{\mathcal{M}}) = \mathit{val}(X) > \mathit{val}(X')$, contradiction.
We denote by $b_0$ the $r^\mathcal{M}$-successor of $a_0$, if it exists (i.e., if there is an edge $(a_0,b_0) \in r^\mathcal{M}$).

We set $\mathfrak{t}=(a_{0},a_{1},r)$.
For all $1\leq\ell\leq h$ we define the shorthand $D_{\ell}^{\rhd}=D_{\ell}^{\op{\mathcal{M}}{\mathfrak{t}}},\,\, A_{\ell}^{\rhd}=A_{\ell}^{\op{\mathcal{M}}{\mathfrak{t}}},\,\, B_{\ell}^{\rhd}=B_{\ell}^{\op{\mathcal{M}}{\mathfrak{t}}}$.

\begin{enumerate}
\item By the compatibility of $RE$ and $DI$, $D_\ell^{\mathcal{M}}=D_\ell^{\rhd}$ for all $\ell \not= h'$.
\item By Lemma \ref{lem:op-on-concepts}, $\overline{tp}_\mathcal{M}(u)=\overline{tp}_{\op{\mathcal{M}}{\mathfrak{t}}}^{\varphi}(u)$ for all $u\in M$.
    Since the outgoing edges of every vertex $u \notin \{a_0,a_1\}$ do not change by applying $\rhd$,
    $\overline{tp}_\mathcal{M}(u)=\overline{tp}_{\op{\mathcal{M}}{\mathfrak{t}}}^{\varphi}(u)$.
    For $a_0,a_1$, the only change is in $s$, but $a_0$ and $a_1$ have outgoing edges corresponding to $r$ both in $\mathcal{M}$ and in $\op{\mathcal{M}}{\mathfrak{t}}$.
    So, $\overline{tp}_\mathcal{M}(u)=\overline{tp}_{\op{\mathcal{M}}{\mathfrak{t}}}^{\varphi}(u)$ for $u\in\{a_0,a_1\}$.

\item By Lemma \ref{lem:op-on-concepts}, $\mathcal{M}$ and $\op{\mathcal{M}}{\mathfrak{t}}$ agree on $\varphi$.
\item We show that $X' = X \setminus \{a_1\} \cup \{w\}$ is a base for $D_{h'}^{\rhd}$.
    We have $\mathit{val}(X) > \mathit{val}(X')$ by $f_{h'}(a_{0}) = f_{h'}(a_{1})$ and $f_{h'}(w) < f_{h'}(a_{0})$.
    This is sufficient to establish $\mathit{val}(D_{h'}^{\mathcal{M}}) = \mathit{val}(X) > \mathit{val}(X') \ge  \mathit{val}(D_{h'}^{\rhd})$.

    We consider some node $v \in D_{h'}^{\mathcal{M}}$.
    Because $X$ is a basis, $v$ is reachable from some $u \in X$ by some path $\pi$.
    We introduce $Z = \{a_{0},b_{0},a_{1},b_1\}$ as a shorthand.
    We proceed by a case distinction.

    Case 1:
        $\pi$ does not contain any node from $Z$ (in particular $u \neq a_1$).
        Then, $\pi$ also witnesses that $v$ is reachable from $u \in X'$ by $\pi$ in $D_{h'}^{\rhd}$.

    Case 2:
        $\pi$ contains a node from $Z$.
        Then there is a decomposition of $\pi$ into two paths $\pi_1$ and $\pi_2$, i.e.,
        $\pi = \pi_1\pi_2$, such that $\pi_2$ starts with a node $z \in Z$ but otherwise does not visit $Z$.
        We construct a path $\pi_0$ from $w$ to $z$ using a suitable combination of the edges $(w,a_0),(a_0,b_1),(a_1,b_0)$ and the path $\pi_{b_1,a_1}$.
        Then the composition $\pi' = \pi_0\pi_2$ witnesses that $v$ is reachable from $w \in X'$ by $\pi'$ in $D_{h'}^{\rhd}$.

    For use in 6), we point out that the special case of $v = w$ establishes that $w$ is
    either reachable from a node in $X \setminus \{a_1\}$ (case 1)
    or belongs to a cycle in $D_{h'}^{\rhd}$ (case 2).

\item Follows directly from 1 and 2.

\item Follows directly from 1 for every $1\leq \ell \leq h$ with $h'\not=\ell$.
In 4), we have established that $X' = X \setminus \{a_1\} \cup \{w\}$ is a basis for $D_{h'}^{\rhd}$ and that $w$ is either reachable from a node in $X \setminus \{a_1\}$ or belongs to a cycle.
It remains to show that every $u \in X \setminus \{a_1\}$ either belongs to $B_{h'}^\rhd$ or to a cycle of $D_{h'}^{\rhd}$.
We fix some $u \in X \setminus \{a_1\}$.
By Lemma~\ref{lem:basis-circle} $u$ either belongs to $B_{h'}^\mathcal{M}$ or to a cycle of $D_{h'}^{\mathcal{M}}$.
If $u \in B_{h'}^\mathcal{M}$, then $u \in B_{h'}^\rhd$ by 2).
Otherwise, $u$ belongs to a cycle $C$ in $D_{h'}^{\mathcal{M}}$.
$C$ cannot contain $a_1$; otherwise $X \setminus \{a_1\}$ would be a base with $\mathit{val}(X \setminus \{a_1\}) < \mathit{val}(X) = \mathit{val}(D_{h'}^{\mathcal{M}})$.
We obtain the cycle $C'$ in $D_{h'}^{\rhd}$ by replacing every edge $(a_0,b_0)$ in $C$ with the path $(a_0,b_1),\pi_{b_1,a_1},(a_1,b_0)$.

\item Follows directly from 1 and 2 for every $1\leq \ell \leq h$ with $h'\not=\ell$.
Because $f_{h'}$ is a $h'$-useful labeling for $D_{h'}^{\mathcal{M}}$ we have that (1) $f_{h'}(u) = f_{h'}(v)$ implies $\overline{tp}_{\mathcal{M}}^{\varphi}(u) = \overline{tp}_{\mathcal{M}}^{\varphi}(v)$ for all $u,v \in A_{h'}^{\mathcal{M}}$ and (2) for every element $u\in A_{h'}^{\mathcal{M}}$, either $u \in B_{h'}^{\mathcal{M}}$, or there exist elements $v,w\in A_{h'}^{\mathcal{M}}$ such that $f_{h'}(u) = f_{h'}(v)$, $f_{h'}(w) < f_{h'}(v)$ and the graph $D_{h'}^{\mathcal{M}}$ has an edge $(w,v)$.
We have that $\overline{tp}_\mathcal{M}(u) = \overline{tp}_{\op{\mathcal{M}}{\mathfrak{t}}}^{\varphi}(u)$ for all $u \in M$ by 2).
Thus, $A_{h'}^{\mathcal{M}} = A_{h'}^{\rhd}$.
Further, $f_{h'}$ has the same values on $A_{h'}^{\mathcal{M}}$ and $A_{h'}^{\rhd}$.
Because the operation $\rhd$ changed only the edges $(a_0,b_0)$ and $(a_1,b_1)$ these facts almost show that
$f_{h'}$ is a $h'$-useful labeling for $D_{h'}^{\rhd}$.
It remains to argue that for every element $u$ with $f_{h'}(u) = f_{h'}(a_0)$ ($= f_{h'}(a_1))$  there exist elements $v,w \in A_{h'}^{\rhd}$ such that $f_{h'}(u) = f_{h'}(v)$, $f_{h'}(w) < f_{h'}(v)$ and the graph $D_{h'}^{\rhd}$ has an edge $(w,v)$.
This fact is witnessed by the edge $(w,a_1)$.
\end{enumerate}
\end{proof}

\subsection{Semi-connectedness and useful labelings}

Here we define semi-connectedness and useful labelings exactly and prove that they capture reachability (Lemma~\ref{lem:connected-implies-useful-order--}).

\begin{definition}
[Semi-connected Structure]
\label{def:Po-conn}
For every reachability assertion $\beta_{h'} = \Reacha{B_{h'}}{S_{h'}}{A_{h'}}$, we write $D_{h'}^{\mathcal{M}}$ for \emph{the directed graph $D_{\beta_{h'}}^{\mathcal{M}}$}.
Let $\mathcal{M}$ be a $\tau$-structure.
$\mathcal{M}$ is $\Phi$-semi-connected, if
(I) $\mathcal{M} \models \formula{\Phi}$ and
(II) for every $\Reacha{B_{h'}}{S_{h'}}{A_{h'}}\in RE$ and $u\in A_{h'}^{\mathcal{M}}$, either $u$ is reachable in $D_{h'}^{\mathcal{M}}$ from $B_{h'}^{\mathcal{M}}$ or $u$ is reachable from a cycle.
\end{definition}

Observe that if $\mathcal{M}$ is $\Phi$-semi-connected, then $\mathcal{M}\models\bigwedge RE\land\bigwedge DI$
iff $\mathcal{M}$ satisfies the following strengthening of {\it (II)}:
{\it for every $\Reacha{B_{h'}}{S_{h'}}{A_{h'}}\in RE$ and $u\in A_{h'}^{\mathcal{M}}$, $u$ is reachable from $B_{h'}^{\mathcal{M}}$}.
The $h'$-useful labelings we define next mimic linear orderings on the types of the elements in $A_{h'}^{\mathcal{M}}$ that can be obtained from a Depth-First Search (DFS) run on $D_{h'}^{\mathcal{M}}$ starting from elements in $B_{h'}^{\mathcal{M}}$.
\begin{definition}[Useful Labeling]
\label{def:useful-labeling}
Let $\mathcal{M}$ be a $\tau$-structure.
Let $1\leq h'\leq h$.
A function $f_{h'}: A_{h'}^{\mathcal{M}} \rightarrow [1,|\mathrm{TYPES}_{\varphi}|]$ is a \emph{$h'$-useful labeling for $\mathcal{M}$}, if (1) $f_{h'}(u) = f_{h'}(v)$ implies $\overline{tp}_{\mathcal{M}}^{\varphi}(u) = \overline{tp}_{\mathcal{M}}^{\varphi}(v)$ for all $u,v \in A_{h'}^{\mathcal{M}}$ and if (2) for every element $u\in A_{h'}^{\mathcal{M}}$, either $u \in B_{h'}^{\mathcal{M}}$,
or there exist elements $v,w\in A_{h'}^{\mathcal{M}}$ such that $f_{h'}(u) = f_{h'}(v)$, $f_{h'}(w) < f_{h'}(v)$ and the graph $D_{h'}^{\mathcal{M}}$ has an edge $(w,v)$.
\end{definition}

\begin{lemma}
\label{lem:use-ord}
Let $\mathcal{M}$ be a $\tau$-structure.
If $\mathcal{M} \models \Phi$, then there are $h'$-useful labelings $f_{h'}$ for $\mathcal{M}$, for every $1\leq h'\leq h$.
\end{lemma}
\begin{proof}
We assume $\mathcal{M}$ satisfies $\Phi = \varphi \land \bigwedge RE \land \bigwedge DI$.
We fix some $1\leq h'\leq h$.
We have that $\Reacha{B_{h'}}{S_{h'}}{A_{h'}}$ holds for $\mathcal{M}$.
We explain how to build a $h'$-useful labeling for $\mathcal{M}$ by executing a Depth-First Search (DFS) from the elements in $B_{h'}^{\mathcal{M}}$.
If an element $u$ is visited during the DFS, $u$ is assigned a number according to its type $\overline{tp}_{\mathcal{M}}^{\varphi}(u)$.
If the type $\overline{tp}_{\mathcal{M}}^{\varphi}(u)$ has not appeared during the DFS yet, $u$ is assigned the smallest number in $[1,|\mathrm{TYPES}_{\varphi}|]$ that has not been used so far;
if the type has already appeared, $u$ is assigned the number associated with this type.
Let $f_{h'}$ be the labeling resulting from this process.
We show that $f_{h'}$ is a $h'$-useful labeling for $\mathcal{M}$.

By construction $f_{h'}$ is a function from $A_{h'}^{\mathcal{M}}$ to $[1,|\mathrm{TYPES}_{\varphi}|]$.
Moreover, for all $u,v \in A_{h'}^{\mathcal{M}}$ is holds that $f_{h'}(u) = f_{h'}(v)$ iff $\overline{tp}_{\mathcal{M}}^{\varphi}(u) = \overline{tp}_{\mathcal{M}}^{\varphi}(v)$ (*).
It remains to show that for every element $u\in A_{h'}^{\mathcal{M}}$, either $u \in B_{h'}^{\mathcal{M}}$,
or there exist elements $v,w\in A_{h'}^{\mathcal{M}}$ such that $f_{h'}(u) = f_{h'}(v)$, $f_{h'}(w) < f_{h'}(v)$ and the graph $D_{h'}^{\mathcal{M}}$ has an edge $(w,v)$:
Let $u \in A_{h'}^{\mathcal{M}} \setminus B_{h'}^{\mathcal{M}}$.
We proceed by a case distinction:
(1) The type $\overline{tp}_{\mathcal{M}}^{\varphi}(u)$ of $u$ has not been seen during the DFS before $u$ is visited.
Because of $u \not\in B_{h'}^{\mathcal{M}}$ there is a predecessor $w \in A_{h'}^{\mathcal{M}}$ of $u$ in $D_{h'}^{\mathcal{M}}$ through which $u$ has been reached during the DFS.
Because $w$ has been reached before $u$ and because $u$ is assigned the smallest number in $[1,|\mathrm{TYPES}_{\varphi}|]$ that has not been used so far, we have $f_{h'}(w) < f_{h'}(u)$.
(2) The type $\overline{tp}_{\mathcal{M}}^{\varphi}(u)$ of $u$ has already been seen during the DFS before $u$ is visited.
Let $v \in A_{h'}^{\mathcal{M}}$ be the first node with type $\overline{tp}_{\mathcal{M}}^{\varphi}(v) = \overline{tp}_{\mathcal{M}}^{\varphi}(u)$ to be visited during the DFS.
By case (1) there is a predecessor $w$ of $v$ in $D_{h'}^{\mathcal{M}}$ with
$f_{h'}(w) < f_{h'}(v)$.
By (*) we have $f_{h'}(u) = f_{h'}(v)$.
Thus, the claim follows.
\end{proof}

This gives direction $\Rightarrow$ of the following lemma:
\begin{lemma}
\label{lem:connected-implies-useful-order--} \label{lem:conn-equiv-semi-conn-plus-useful-ord--}
$\Phi=\varphi\land\bigwedge RE\land\bigwedge DI$ is satisfiable iff
there is a $\Phi$-semi-connected structure with $h'$-useful labelings for every $1\leq h'\leq h$.
\end{lemma}

Next, we introduce definitions that will be needed for the proof of direction $\Leftarrow$.

Let $G=(V,E)$ be a directed graph.
$\reach{G}{X} = Y$ denotes the set of  elements $Y \subseteq V$ that are \emph{reachable} from $X \subseteq V$ in $G$.

\begin{definition}
[Base and Values]
Let $f$ be a $h'$-useful labeling for $\mathcal{M}$.
We call a set $X \subseteq A_{h'}^\mathcal{M}$ a \emph{base} for $D_{h'}^{\mathcal{M}}$, if
$\reach{D_{h'}^{\mathcal{M}}}{X} = A_{h'}^\mathcal{M}$.
We call a member $x$ of a base $X$ a \emph{base element}.
We define the \emph{value} $\mathit{val}_f(X) = \sum_{x \in X \setminus B_{h'}^\mathcal{M}} f(x)$ \emph{of a base} $X$ to be the sum over the label values of the base elements of $X$ that are not in $B_{h'}^\mathcal{M}$.
We define the \emph{value} $\mathit{val}_f(D_{h'}^{\mathcal{M}}) = \min \{\mathit{val}_f(X) \mid X \text{ is a base for } D_{h'}^{\mathcal{M}} \}$ \emph{of the graph} $D_{h'}^{\mathcal{M}}$ to be the minimum of the values of its bases.
We omit the subscript $f$ in $\mathit{val}(X)$ and $\mathit{val}(D_{h'}^{\mathcal{M}})$ when $f$ is clear from the context.
\end{definition}

Intuitively, values $\mathit{val}_f(D_{h'}^{\mathcal{M}})$ capture how close the graph $D_{h'}^{\mathcal{M}}$ is to being connected:

\begin{lemma}
\label{lem:value-zero}
Let $f$ be a $h'$-useful labeling for $\mathcal{M}$.
$\mathit{val}_f(D_{h'}^{\mathcal{M}}) = 0$ iff $D_{h'}^{\mathcal{M}}$ is connected.
\end{lemma}
\begin{proof}
Assume $D_{h'}^{\mathcal{M}}$ is connected.
Then $B_{h'}^\mathcal{M}$ is a base for $D_{h'}^{\mathcal{M}}$.
Thus $\mathit{val}(B_{h'}^\mathcal{M}) = 0$, which implies $\mathit{val}(D_{h'}^{\mathcal{M}}) = 0$.

Assume $\mathit{val}(D_{h'}^{\mathcal{M}}) = 0$.
Then there is a base $X$ for $D_{h'}^{\mathcal{M}}$ with $\mathit{val}(X) = 0$.
Because $f$ maps all nodes to positive values, we must have $X \subseteq B_{h'}^\mathcal{M}$.
Thus, every node in $D_{h'}^{\mathcal{M}}$ is reachable from $B_{h'}^\mathcal{M}$.
\end{proof}

The following lemma states a property of bases in semi-connected structures:

\begin{lemma}
\label{lem:basis-circle}
Let $\mathcal{M}$ be a structure that is $\Phi$-semi-connected.
Let $f$ be a $h'$-useful labeling for $\mathcal{M}$.
Let $X$ be a base for $D_{h'}^{\mathcal{M}}$ with $\mathit{val}_f(X) = \mathit{val}_f(D_{h'}^{\mathcal{M}})$.
Then every base element $x \in X$ either belongs to $B_{h'}^\mathcal{M}$ or to a cycle of $D_{h'}^{\mathcal{M}}$.
\end{lemma}
\begin{proof}
We fix some base element $x \in X$.
Let us assume $x$ does not belong to $B_{h'}^\mathcal{M}$ or to a cycle of $D_{h'}^{\mathcal{M}}$.
By definition we have $\mathit{val}(X) = \mathit{val}(D_{h'}^{\mathcal{M}}) = \min \{\mathit{val}(X) \mid X \text{ is a base for } D_{h'}^{\mathcal{M}} \}$.
By the semi-connectedness of $\mathcal{M}$, $x$ is either reachable from $B_{h'}^\mathcal{M}$ (1) or from a cycle in $D_{h'}^{\mathcal{M}}$ (2).
Case (1): $x$ is reachable from some $z \in B_{h'}^\mathcal{M}$.
However, $X' = X \setminus \{x\} \cup \{z\}$ is a base for $D_{h'}^{\mathcal{M}}$ with $\mathit{val}(X') < \mathit{val}(X)$.
Contradiction.
Case (2): $x$ is reachable from some cycle $C$ in $D_{h'}^{\mathcal{M}}$.
We fix an element $y$ on $C$.
Because $X$ is a base, there is a base element $z \in X$ such that $y$ can be reached from $z$.
We have $z \neq x$, because otherwise $x$ would belong to a cycle of $D_{h'}^{\mathcal{M}}$.
However, $X' = X \setminus \{x\}$ is a base for $D_{h'}^{\mathcal{M}}$ with $\mathit{val}(X') < \mathit{val}(X)$.
Contradiction.
\end{proof}

The next lemma, Lemma \ref{lem:rhd-connectedness--}, shows that $\rhd$ can be applied to $D_{h'}^{\mathcal{M}}$ such that $\mathit{val}(D_{h'}^{\mathcal{M}})$ decreases for some $1 \le h' \le h$.
The compatibility of $RE$ and $DI$ ensures that $\rhd$ does not modify the graphs $D_\ell^{\mathcal{M}}$ with $\ell \neq h'$.

\begin{lemma}
\label{lem:rhd-connectedness--}
Let $1\leq h' \leq h$ and let $\mathcal{M}$ be a structure such that $\mathcal{M} \models \formula{\Phi}$, $\mathcal{M}$ is $\Phi$-semi-connected and has $\ell$-useful labelings $f_\ell$ for all $1 \leq \ell \leq h$.
If $\mathit{val}_{f_{h'}}(D_{h'}^{\mathcal{M}}) > 0$,
then there is a tuple\textup{ $\mathfrak{t}=(a_{0},a_{1},r)$
}such that
\begin{enumerate}
\item For all $\ell \not= h'$, $D_\ell^{\mathcal{M}} = D_\ell^{\op{\mathcal{M}}{\mathfrak{t}}}$.
\item For all $u\in M$, $\overline{tp}_{\mathcal{M}}^{\varphi}(u)=\overline{tp}_{\op{\mathcal{M}}{\mathfrak{t}}}^{\varphi}(u)$.
\item $\op{\mathcal{M}}{\mathfrak{t}}\models \formula{\Phi}$.
\item $\mathit{val}_{f_{h'}}(D_{h'}^{\mathcal{M}}) > \mathit{val}_{f_{h'}}(D_{h'}^{\op{\mathcal{M}}{\mathfrak{t}}})$.
\item $\mathit{val}_{f_{\ell}}(D_\ell^{\mathcal{M}}) = \mathit{val}_{f_{\ell}}(D_\ell^{\op{\mathcal{M}}{\mathfrak{t}}})$
for all $\ell \not= h'$.
\item $\op{\mathcal{M}}{\mathfrak{t}}$ is $\Phi$-semi-connected.
\item $f_\ell$ is a $\ell$-useful labeling for $\op{\mathcal{M}}{\mathfrak{t}}$
for all $1\leq \ell \leq h$.
\end{enumerate}
\end{lemma}
\begin{proof}[Proof Sketch]
In the following, we will give an intuition on the proof of Lemma~\ref{lem:rhd-connectedness--}. We delay the full proof to
Section \ref{app:useful-proof}.
We fix some base $X$ for $D_{h'}^{\mathcal{M}}$ with $\mathit{val}(X) = \mathit{val}(D_{h'}^{\mathcal{M}}) > 0$.
We choose a base element $a_1 \in X \setminus B_{h'}^\mathcal{M}$.
Because $f_{h'}$ is a $h'$-useful labeling for $\mathcal{M}$ there are $a_0,w\in A_{h'}^{\mathcal{M}}$ such that $f_{h'}(a_0) = f_{h'}(a_1)$, $f_{h'}(w) < f_{h'}(a_0)$ and the graph $D_{h'}^{\mathcal{M}}$ has an edge $(w,a_0)$.
$a_0$ and $a_1$ cannot belong to the same cycle in $D_{h'}^{\mathcal{M}}$ by the minimality of $X$.
By Lemma~\ref{lem:basis-circle}, $a_1$ belongs to a cycle in $D_{h'}^{\mathcal{M}}$.
$b_1$ denotes the successor of $a_1$ by some edge $r$ in this cycle.
\piccaption[]{\label{fig:1}}\parpic[r]{\includegraphics[scale=0.85]{diag}}
Figure \ref{fig:1} shows the result (II) of applying $\rhd$ on (I) (we depict here the case, where $a_0$ has an $r$-successor $b_0$).
The black vertex belongs to the base $X$, dotted arrows denote paths inside $A_{h'}^{\mathcal{M}}$ whose edges belong to $S_{h'}$, and solid arrows belong to $S_{h'}$.
Applying $\rhd$ increases the reachability of the structure: all
vertices in (II) are now reachable from the black vertex.
However, in the special case where the black vertex and $a_1$ coincide, a new cycle in created.
In both cases we have that $X' = X \setminus \{a_1\} \cup \{w\}$ is a base for $D_{h'}^{\op{\mathcal{M}}{\mathfrak{t}}}$ with $\mathit{val}(X') < \mathit{val}(X)$ and that  $D_{h'}^{\op{\mathcal{M}}{\mathfrak{t}}}$ remains semi-connected.
\end{proof}

Finally, we show that the repeated application of $\rhd$ on a semi-connected structure with useful labelings leads eventually to a structure satisfying $\Phi$:

\begin{proof}[Proof of Lemma~\ref{lem:connected-implies-useful-order--}]
By Lemma~\ref{lem:use-ord} if $\Phi$ is satisfied by a structure $\mathcal{M}$, then $\mathcal{M}$ has $h'$-useful labelings for every $h'$ and is semi-connected.

For the other direction, there is a $\Phi$-semi-connected structure $\mathcal{M}$ with $h'$-useful labelings for every $1\leq h'\leq h$.
There is a sequence $\mathcal{M} = \mathcal{M}_{1},\ldots,\mathcal{M}_{p} = \mathcal{M}'$ of structures such
that each $\mathcal{M}_{j+1}$ is obtained from $\mathcal{M}_{j}$ by one application
of $\rhd$ and $\mathit{val}(D_{h'}^\mathcal{M})=0$ for all $h'$.
There is guaranteed to be such a sequence because
\begin{enumerate}
\item the premise of Lemma \ref{lem:rhd-connectedness--} holds for $\mathcal{M}$,
\item for all $j$, if the premise of Lemma \ref{lem:rhd-connectedness--}
holds for $\mathcal{M}_{j}$ and $\phi$, then the premise of Lemma \ref{lem:rhd-connectedness--}
holds for $\mathcal{M}_{j+1}$, and
\item The tuple $(\mathit{val}(D_1^\mathcal{M}) ,\cdots,\mathit{val}(D_h^\mathcal{M}))$ is decreasing with regard to the component-wise ordering of $h$-tuples over $\mathbb{N}$, so eventually $(0,\ldots,0)$ must be reached.
\end{enumerate}
By Lemma~\ref{lem:value-zero}, $D_{h'}^{\mathcal{M}'}$ is connected for all $h'$.
\end{proof}

\subsection{Reducing connected satisfiability to (plain finite) satisfiability
\label{se:reduce-to-formula}}

Here we show how to express semi-connectedness and existence of useful labelings in $\LoiqNOb_{b}$.
For semi-connectedness, this is easy:
\begin{lemma}
\label{lem:semi-def}
There exists a formula $\semi{\Phi} \in \LoiqNOb_{b}$ such that $\mathcal{M} \models \semi{\Phi}$ iff $\mathcal{M}$ is $\Phi$-semi-connected.
\end{lemma}
\begin{proof}
Let $\semi{\Phi} = \formula{\Phi} \land \bigwedge_{1\leq h'\leq h} \delta_\ensuremath{\mathit{reach-cyc}}^{h'}$
and $\delta_\ensuremath{\mathit{reach-cyc}}^{h'} = A_{h'}\sqcap\neg B_{h'} \sqsubseteq \bigsqcup_{s\in S_{h'}} \exists s^{-}.A_{h'}$.
Assume $\mathcal{M}$ is $\Phi$-semi-connected.
We fix some $1 \le h' \le h$.
Every $u\in A_{h'}^{\mathcal{M}}$ is reachable from $B_{h'}^{\mathcal{M}}$ or is reachable from a cycle, and therefore $u$ has a predecessor in $A_{h'}^{\mathcal{M}}$ with respect to $\bigcup_{s\in S_{h'}}s^{\mathcal{M}}$, unless $u\in B_{h'}$, so $\mathcal{M} \models \delta_\ensuremath{\mathit{reach-cyc}}^{h'}.$

Conversely, we consider a structure $\mathcal{M}$ with $\mathcal{M} \models \formula{\Phi}$, but which is not $\Phi$-semi-connected.
There exists a vertex $u$ and a $1 \le h' \le h$ such that $u$ is not reachable from $B_{h'}^{\mathcal{M}}$ nor from a cycle.
There must exist a vertex $v$ in $A_{h'}^{\mathcal{M}}$ which is a predecessor of $u$ (possibly $u$ itself) and which does not have a predecessor in $A_{h'}^{\mathcal{M}}$, otherwise $u$ lies on a cycle (using the finiteness of the universe).
Since $u$ is reachable from $v$, we must have that, like $u$, $v$ not reachable from $B_{h'}^{\mathcal{M}}$.
Therefore, $v$ is not in $B_{h'}^{\mathcal{M}}$ but belongs to $A_{h'}^{\mathcal{M}}$
and does not have a predecessor, so $\mathcal{M} \not \models \delta_\ensuremath{\mathit{reach-cyc}}^{RE,DI}$.
\end{proof}

Next we define a set of structures $\mathrm{ORD}(\varphi)$ that represent models of $\varphi$ and at the same time also contain useful labelings.
After this definition we will show that $\mathrm{ORD}(\varphi)$ can be defined inside the logic $\LoiqNOb_{b}$.

\begin{definition}
\label{def:ORD}
Let $\varphi$ be a $\LoiqNOb_{b}$ formula over vocabulary $\tau$.
Let $k = |\mathrm{TYPES}_{\varphi}|$.
We define an extended vocabulary $\ensuremath{\mathit{ext}}(\tau)$ that extends $\tau$ with a new atomic concept $M$, new nominals $o_1,\ldots,o_k$,
a new atomic role $\ensuremath{\mathit{ord}}$ and new functional atomic roles $f_1,\ldots, f_h$.

Let $\mathcal{N}$ be a $\ensuremath{\mathit{ext}}(\tau)$-structure with universe $N$.
We denote the substructure of $\mathcal{N}$ with universe $M^\mathcal{N}$ by $\mathcal{M}$.
We denote the set $N \setminus M^\mathcal{N}$ by $\ensuremath{O}^\mathcal{N}$.
The structure $\mathcal{N}$ belongs to $\mathrm{ORD}(\varphi)$ if the following conditions hold:
\begin{enumerate}
\item \label{prop:Mtilde} $\mathcal{M}$ satisfies $\varphi$.
\item \label{prop:partition} $N$ is partitioned into $M^\mathcal{N}$ and $\ensuremath{O}^\mathcal{N} = \{o_1^\mathcal{N},\ldots,o_k^\mathcal{N}\}$.
\item \label{prop:linear} We have that $(o_i^\mathcal{N},o_j^\mathcal{N}) \in \ensuremath{\mathit{ord}}^\mathcal{N}$ iff $i < j$.
\item \label{prop:ftypes} $f_{h'}^\mathcal{N}$ is a function from $A_\ell^\mathcal{M}$ to $\ensuremath{O}^\mathcal{N}$, for every $1 \le {h'} \le h$.
\item \label{prop:ford} $f_{h'}^\mathcal{N}$ is a $h'$-useful labeling for $\mathcal{M}$, using $ \ensuremath{O}^\mathcal{N}$ for the natural numbers $[1,k]$ and $\ensuremath{\mathit{ord}}$ for the order on the natural numbers in Definition~\ref{def:useful-labeling}, for every $1 \le h' \le h$.
\end{enumerate}
\end{definition}

\begin{lemma}
\label{lem:extension-useful}
$\mathrm{ORD}(\varphi)$ is non-empty iff there is a model $\mathcal{M}$ of $\varphi$ with $h'$-useful labelings for $\mathcal{M}$ for every $1\leq h'\leq h$.
\end{lemma}
\begin{proof}
Let $\mathcal{M}$ be a model of $\varphi$ with $h'$-useful labelings $f'_{h'}$ for every $1 \leq h'\leq h$.
Let $M'$ be the universe of $\mathcal{M}$.
We define a model $\mathcal{N}$ with universe $N := M' \cup [1,k]$ by
\begin{itemize}
\item $M^\mathcal{N} = M'$,
\item $o_i^\mathcal{N} := i$,
\item $\ensuremath{\mathit{ord}}^\mathcal{N} = \{(i,j) \mid 1 \le i < j \le k\}$,
\item $f_i^\mathcal{N} := f'_i$, and
\item $C^\mathcal{N} = C^\mathcal{M}$ for all $C \in \varphi$.
\end{itemize}
Clearly, $\mathcal{N}$ satisfies properties~\ref{prop:Mtilde},\ref{prop:partition}, \ref{prop:linear}, \ref{prop:ftypes} and \ref{prop:ford} of Definition~\ref{def:ORD}.

Let $\mathcal{N} \in \mathrm{ORD}(\varphi)$.
Let $\mathcal{M}$ be the substructure of $\mathcal{N}$ with universe $M^\mathcal{N}$.
By property~\ref{prop:Mtilde}, $\mathcal{M}$ satisfies $\varphi$.
By property~\ref{prop:partition}, $\ensuremath{O}^\mathcal{N} = \{o_1^\mathcal{N},\ldots,o_k^\mathcal{N}\}$.
By property~\ref{prop:linear}, $(o_i^\mathcal{N},o_j^\mathcal{N}) \in \ensuremath{\mathit{ord}}^\mathcal{N}$ iff $i < j$.
Thus $(\ensuremath{O}^\mathcal{N},\ensuremath{\mathit{ord}}^\mathcal{N})$ is isomorphic to $([1,k],\leq)$.
By property~\ref{prop:ftypes}, $f_{h'}^\mathcal{N}$ is a function from $A_{h'}^\mathcal{M}$ to $\ensuremath{O}^\mathcal{N}$, for every $1 \le h' \le h$.
By property~\ref{prop:ford}, $f_{h'}^\mathcal{N}$ is a $h'$-useful labeling for $\mathcal{M}$, using $ \ensuremath{O}^\mathcal{N}$
for the natural numbers $[1,k]$ and $\ensuremath{\mathit{ord}}^\mathcal{N}$ for the order on the natural numbers
in Definition~\ref{def:useful-labeling}, for every $1 \le h' \le h$.
Because $(\ensuremath{O}^\mathcal{N},\ensuremath{\mathit{ord}}^\mathcal{N})$ is isomorphic to $([1,k],\leq)$, the last property implies that $f_{h'}^\mathcal{N}$ is a useful labeling, for every $1 \le h' \le h$.
\end{proof}

\begin{lemma}
\label{lem:definingORD}
For every formula $\varphi \in \LoiqNOb_{b}$ there exists a formula $\ensuremath{\mathit{ext}}(\varphi)$ such that $\ensuremath{\mathit{ext}}(\varphi)$ defines $\mathrm{ORD}(\varphi)$.
\end{lemma}
\begin{proof}
We set $\ensuremath{\mathit{ext}}(\varphi) = \theta^{1} \land \theta^{2} \land \theta^{3} \land \theta^{4} \land \theta^{5a} \land \theta^{5b}$.
$\theta^{X}$ defines the property $X$ in Definition \ref{def:ORD}.
\begin{itemize}
\item
For every atomic concept $A$, let $g(A) = A \sqcap M$.
For every concept $C$, $g(C)$ is obtained by replacing its sub-concepts with their $g$ image and intersecting with $M$ (e.g., $g(C_{1}\sqcup C_{2}) = (g(C_{1})\sqcup g(C_{2})) \sqcap M$).
Let $g(\varphi)$ be obtained from $\varphi$ by replacing every inclusion $C \sqsubseteq D$ in $\varphi$ by $g(C) \sqsubseteq g(D)$.
Let $\mathcal{M}$ be the substructure of $\mathcal{N}$ with universe $M^\mathcal{N}$ by $\mathcal{M}$.
We have $\mathcal{M} \models \varphi$ iff $\mathcal{N} \models g(\varphi)$ (this holds because we have $C^\mathcal{M} = g(C)^\mathcal{N}$ for all $C \in \varphi$).

\item
Let $\theta^{2} = \neg M \equiv (o_1 \sqcup \cdots \sqcup o_k)$.
$\theta^{2}$ says that the universe of $N \setminus M^\mathcal{N} = \ensuremath{O}^\mathcal{N}  = \{o_1^\mathcal{N},\ldots,o_k^\mathcal{N}\}$.
\item
Let $\theta^{3}$ be the conjunction of
$o_i \sqsubseteq \left(\neg
\bigsqcup_{1 \leq  j \leq i} \exists \ensuremath{\mathit{ord}}. o_j\right)$
and
$o_i \sqsubseteq
\mybigsqcapDisp_{i <  j \leq k} \exists \ensuremath{\mathit{ord}}.o_j$  for $1\leq i \leq k$.
$\theta^{3}$ says that $o_i^\mathcal{N} \in \bigcap_{i < j \leq k} \{ u \mid (u,o_j^\mathcal{N}) \in \ensuremath{\mathit{ord}}^\mathcal{N}\}$ and $o_i^\mathcal{N} \not\in \bigcup_{1 \le j \leq i} \{ u \mid (u,o_j^\mathcal{N}) \in \ensuremath{\mathit{ord}}^\mathcal{N}\}$, i.e., $(o_i^\mathcal{N},o_j^\mathcal{N}) \in \ensuremath{\mathit{ord}}^\mathcal{N}$ iff $i < j$.
\item
Let $\theta^{4}$ be the conjunction of the formulas $\left(\exists f_{h'} \equiv A_{h'} \sqcap M \right)$ and $\left(\exists f_{h'}^{-}\sqsubseteq\neg M\right)$ for $1\leq h'\leq h$.
$\theta^{4}$ says that $f_{h'}^\mathcal{N}$ is a function from $A^\mathcal{N} \cap M^\mathcal{N} = A_{h'}^\mathcal{M}$ to $N \setminus M^\mathcal{N} = \ensuremath{O}^\mathcal{N}$.
\item
Let $\theta^{5a}$ be the conjunction of
$\left(\exists f_{h'}^{-}.C\right) \sqcap \left(\exists f_{h'}^{-}. \neg C\right) \equiv \bot$ for all $1\leq h'\leq h$ and $C \in \varphi$.
$\theta^{5a}$ says that if $u,v\in A_{h'}^\mathcal{M}$ point to
the same nominal (i.e., $f_{h'}^\mathcal{N}(u) = f_{h'}^\mathcal{N}(v)$), then they must agree on every concept $C \in \varphi$ (i.e., $u \in C^\mathcal{N}$ iff $v \in C^\mathcal{N}$), thus $\overline{tp}_{\mathcal{M}}^{\varphi}(u) = \overline{tp}_{\mathcal{M}}^{\varphi}(v)$.
\item
Let $\theta^{5b}$ be the conjunction, for all $1 \leq \ell \leq k$ and
\[
\begin{array}{l}
1\leq h'\leq h$, of $(\exists f_{h'}. o_\ell  \sqcap \neg B_{h'} \not\equiv \bot)
\rightarrow \\
\big(\bot \not\equiv \big(\bigsqcup_{s\in S_{h'}} \exists s. \exists f_{h'}. o_{\ell}\big) \sqcap \exists f_{h'}. \exists \ensuremath{\mathit{ord}}. o_{\ell} \big)
\end{array}
\]
$\theta^{5b}$ says that if $u \in A_{h'}^{\mathcal{M}} \setminus B_{h'}^{\mathcal{M}}$ is pointing to some nominal $o_\ell^\mathcal{N}$ with $f_{h'}^\mathcal{N}$, then there is a $v \in A_{h'}^{\mathcal{M}}$ that has a successor pointing to the same nominal $o_\ell^\mathcal{N}$ with $f_{h'}^\mathcal{N}$ and that is pointing to a smaller nominal with $f_{h'}^\mathcal{N}$ (i.e., pointing to some nominal in $(\exists \ensuremath{\mathit{ord}}. o_{\ell})^\mathcal{N}$).
\end{itemize}
\end{proof}

\begin{theorem}
\label{th:exp}
Let $\Phi_{i}=\varphi_{i}\land\bigwedge RE_{i}\land\bigwedge DI_{i}\in\mathcal{ALCQIO}_{b,Re}$, for $i=1,2$.
There are $\mathcal{\LoiqNObTEXT}$ formulas $\mu$ and $\kappa$ over an extended vocabulary such that\\
(1) $\Phi_{1}$ is satisfiable iff $\mu$ is satisfiable.\\
(2) $\Phi_{1}$ implies $\Phi_{2}$ iff $\kappa$ is not satisfiable.
\end{theorem}

\begin{proof}
(1) follows from Lemmas \ref{lem:connected-implies-useful-order--},
\ref{lem:semi-def}, \ref{lem:extension-useful}, and \ref{lem:definingORD} by setting $\mu = \ensuremath{\mathit{ext}}(\semi{\Phi})$.

(2): For every $h'$, let $X_{h'}$ be a fresh atomic concept and let
$\alpha_{h'}$ be the conjunction of $(B_{h'}\sqsubseteq X_{h'}) \land (A_{h'}\sqcap\neg X_{h'}\not\equiv\bot)$ and
$\bigwedge_{s\in S_{h'}}(\exists s.\neg X_{h'}\sqsubseteq\neg X_{h'})$.
For every $\mathcal{M}$, $\mathcal{M}\models\neg\Reacha{B_{h'}}{S_{h'}}{A_{h'}}$
iff there is $X_{h'}^{\mathcal{M}}$ such that $\left\langle \mathcal{M},X_{h'}^{\mathcal{M}}\right\rangle \models\alpha_{h'}$.
Hence, $\mathcal{M}\models\neg\Phi_{2}$ iff there are $X_{h'}^{\mathcal{M}}\subseteq M$, $1\leq h'\leq h$, such that $\left\langle \mathcal{M},X_{h'}^{\mathcal{M}}:1\leq h'\leq h\right\rangle \models\neg\varphi_{2}\lor\neg\bigwedge DI_{2}\lor\bigvee_{1\leq h'\leq h}\alpha_{h'}$.
Hence, $\kappa_{\varphi} = \Phi_{1}\land \big(\neg\varphi_{2} \lor \neg \bigwedge DI_{2}\lor\bigvee_{1\leq h'\leq h}\alpha_{h'}\big)$
is satisfiable iff $\Phi_{1}\to\Phi_{2}$ is not a tautology and we
get (2).
In both (1) and (2) we use that satisfiability in $\LoiqNOb_{b}$ is reducible to that in $\mathcal{\LoiqNObTEXT}$, see Appendix \ref{app:Loiq_LoiqNOb}.
\end{proof}

\subsection{Verification of Pointer-manipulating Programs using $\mathcal{ALCQIO}_{b,Re}$ }
\label{se:verification}

The focus of this paper is the development of a logic and decision procedures which can be used for shape analysis in future work.
However, we believe that it is important to relate the logic we develop in this paper to its intended application.
We illustrate in this section how to use $\mathcal{ALCQIO}_{b,Re}$ for the verification of pointer-manipulating programs.
We will discuss on the example program given in Fig. \ref{fig:prog} how to formulate verification conditions for a Hoare-style correctness proof.
We leave the non-trivial task of developming a full verification framework based on $\mathcal{ALCQIO}_{b,Re}$ for future work.
Section \ref{se:main-section} can be read independently of this section.

The program in Fig. \ref{fig:prog} receives as input a list pointed to by $head$ in which some elements may be marked but $head$ is not marked.
The program removes from the list all marked elements.

\begin{figure}
\begin{lstlisting}
start: b := head;
loop:  while (b != null)
          if (b.next != null && b.next.marked)
             b.next := b.next.next;
          else
             b := b.next;
end:   ;
\end{lstlisting}

\caption{\label{fig:prog}}
\end{figure}

We annotate the labels $\mathsf{start}$, $\mathsf{end}$ and $\mathsf{loop}$ with the pre-condition, the post condition and the loop invariant respectively:
\begin{description}
\item [{[Pre-condition]}] $head$ points to the first element of an acyclic list.
    $head$ is not marked.
\item [{[Post-condition]}]~
    \begin{enumerate}
        \item After the program is executed, $head$ points to the first element of an acyclic list containing only unmarked elements.
        \item Moreover, the elements removed from the input list are exactly the marked elements.
    \end{enumerate}
\end{description}
The following loop invariant suffices to prove the correctness of the program with respect to the pre- and post-conditions:
\begin{description}
\item [{[{Loop invariant}]}]~
    \begin{enumerate}
        \item The pre-condition holds.
        \item $b$ points to an element of the list.
        \item the set of unmarked elements in the list is exactly the same set as at the beginning of the program.
        \item all elements in the list before $b$ are unmarked.
    \end{enumerate}
\end{description}
The correctness of the program is achieved by proving that the annotations are correct.
More precisely, $S_{2}$ is the piece of loopless code inside the while loop, i.e., the sequence of $\mathsf{assume(b  \ {!}{=} \ null)}$ and the code in the if-then-else statement, $S_{1}$ is the assignment $\mathsf{b := head}$ and $S_{3}$ is the statement $\mathsf{assume(b \ {=}{=} \  null)}$.
To prove the correctness of the program we need to prove that:
\begin{description}
\item [{[$\mathsf{VC}_1$]}] If the pre-condition holds, then after executing $S_{1}$ the loop invariant will hold.
\item [{[$\mathsf{VC}_2$]}] If the loop invariant holds, then after executing on iteration of the loop, i.e., executing $S_{2}$ once, the loop invariant will hold again.
\item [{[$\mathsf{VC}_3$]}] If the loop-invariant holds, then after executing $S_{3}$ the post-condition will hold.
\end{description}

\paragraph{Annotations in $\mathcal{ALCQIO}_{b,Re}$: }

Next we write the annotations in $\mathcal{ALCQIO}_{b,Re}$. The memory is represented
as $\rho$-structures and $\tau$-structures with $\rho\subseteq\tau$.
$\rho$ contains the nominals $head$, $b$ and $Null$, the role
$next$ and the concept $\ensuremath{\mathit{Marked}}$. We think of each element of the
memory as a fixed size block of memory containing the $\mathsf{next}$
pointer field and the $\mathsf{marked}$ field, except for the special
element which interprets $Null$ and represent the value $\mathsf{null}$.
$head$ and $b$ are the elements which $\mathsf{head}$ and $\mathsf{b}$
point to. $next$ is a function on the elements of the memory defined
by the pointer $\mathsf{next}$. $\ensuremath{\mathit{Marked}}$ contains the set of elements
whose $\mathsf{marked}$ field is set to true.

Our presentation here is a simplification of the memory model in \cite{arXiv:CKSVZ13},
which further supports dynamic allocation and deallocation memory.

$\tau$ extend $\rho$ with the concepts $L$
and $L_{b}$.
$L$ will contain the elements of the list.
$L_{b}$ will contain
the elements of the list segment starting at $head$ up to $b$ (not
including $b$).

The annotations $\Phi_{pre}$, $\Phi_{l-inv}$ and $\Phi_{post}$ refer to the memory at the labels $\mathsf{start}$, $\mathsf{loop}$ and $\mathsf{post}$ respectively.
The pre-condition $\Phi_{pre}$ is
\[
\Phi_{pre} = \Phi_{aList}^{head,next,L} \land head \sqsubseteq \neg \ensuremath{\mathit{Marked}}
\]

$\Phi_{aList}^{head,next,L} = \Reacha{head}{next}L\land\neg(L\sqsubseteq\exists next)$ is the formula defining an acyclic list from Section \ref{se:examples}.
The post-condition is given by $\Phi_{post}=\Phi_{post1}\land\Phi_{post2}$, where
\begin{eqnarray*}
\Phi_{post1} & = & \Phi_{aList}^{head,next,L}\land L\sqsubseteq\neg \ensuremath{\mathit{Marked}}\\
\Phi_{post2} & = & L\equiv L_{ghost}\sqcap\neg \ensuremath{\mathit{Marked}}_{ghost}
\end{eqnarray*}
$L_{ghost}$ and $\ensuremath{\mathit{Marked}}_{ghost}$ represent the values of $L$ and $\ensuremath{\mathit{Marked}}$ at the start of the program.
\[
\Phi_{l-inv}=\Phi_{l-inv1}\land\Phi_{l-inv2}\land\Phi_{l-inv3}\land\Phi_{l-inv4}
\]
where
\begin{eqnarray*}
\Phi_{l-inv1} & = &  \Phi_{pre}\\
\Phi_{l-inv2} & = & b\sqsubseteq L\\
\Phi_{l-inv3} & = & L \sqcap \neg \ensuremath{\mathit{Marked}} \equiv L_{ghost} \sqcap \neg \ensuremath{\mathit{Marked}}_{ghost}\\
\Phi_{l-inv4} & = & (L_{b}\sqsubseteq L) \land (head\sqsubseteq L_{b}\sqcup b)\land(b\sqsubseteq\neg L_{b})\\
 &  & \land(L_{b}\sqsubseteq\forall next.L_{b}\sqcup b)\land(\neg L_{b}\sqsubseteq\forall next.\neg L_{b})\\
 &  & \land(L_{b}\sqsubseteq\neg \ensuremath{\mathit{Marked}})
\end{eqnarray*}

$\Phi_{l-inv4}$ expresses that $L_{b}$ is exactly the set of elements
in $L$ from $head$ to $b$, not including $b$.

\paragraph{Verification conditions in $\mathcal{ALCQIO}_{b,Re}$: }

Expressing the verification conditions exactly requires us first to
relate the loopless pieces of code $S\in\{S_{1},S_{2},S_{3}\}$ with
the annotations $\Phi_{pre}$, $\Phi_{post}$ and $\Phi_{l-inv}$.
Each $S_{i}$ is associated with two annotations $\Phi_{start}^{i},\mbox{\ensuremath{\Phi}}_{end}^{i}\in\{\Phi_{pre},\Phi_{post},\Phi_{l-inv}\}$
(e.g., for $S_{1}$ we have $\Phi_{start}^{1}=\Phi_{pre}$ and $\Phi_{end}^{1}=\Phi_{l-inv}$).

We need three formulas $\Psi_{1},\Psi_{2},\Psi_{3}\in\mathcal{ALCQIO}_{b,Re}(\tau)$ such
that $\psi_{i}$ is satisfiable iff $\mathsf{VC}_{i}$ does not hold.
The verification conditions $\mathsf{VC}_{1}$, $\mathsf{VC}_{2}$,
and $\mathsf{VC}_{3}$ refer to the memory both at the start and at
the end of $S_{i}$. In contrast, the truth-values of $\Psi_{1}$,
$\Psi_{2}$ and $\Psi_{3}$ will be evaluated on $\tau$-structures
corresponding to the memory at the start of $S_{i}$ only.

The main observation which is required to write $\Psi_{i}$ is that
the symbols of $\tau$ in $\Phi_{end}^{i}$ referring to the memory
at the end of $S_{i}$ can be written in terms of the same sybmols
when they refer to the memory at the start of $S_{i}$.

Let $\underline{\rho}$ and $\underline{\tau}$ be disjoint copies
of $\rho$ and $\tau$ with symbols $\underline{sym}$ corresponding
to $sym$. Let $\mathcal{M}$ be a $\rho$-structure. Let $\mathcal{M}_{S_{i}}$ be
the unique $\underline{\rho}$-structure obtained by executing $S_{i}$
on $\mathcal{M}$ and renaming all symbols $sym$ to $\underline{sym}$. Similarly,
we write $\mathcal{N}_{S_{i}}$ for the unique $(\tau\backslash\rho)\cup\underline{\rho}$-structure
obtained by replacing the sub-structure $\mathcal{M}$ with vocabulary $\rho$
of $\mathcal{N}$ with $\mathcal{M}_{S_{i}}$.
Let $\underline{\Phi_{end}^{i}}$ be
obtained from $\Phi_{end}^{i}$ be replacing each $\tau$-symbol $sym$
with the $\underline{\tau}$-symbol $\underline{sym}$.

We will define $\Psi_{i}$ by expressing all symbols of $\underline{\tau}$
referring to the memory at the end of $S_{i}$ by $\tau$-symbols
referring to the memory at the start of $S_{i}$.

Consider $\mathsf{VC}_{i}$. The following are equivalent:
\begin{itemize}
\item [(A)] $\mathsf{VC}_{i}$ does not hold
\item [(B)] There exist a $\tau$-structure $\mathcal{N}$ such that $\mathcal{N}\models\Phi_{start}^{i}$
and for every extension $\mathcal{P}'$ of the $\tau\cup\underline{\rho}$-structure
$\mathcal{P}=\left\langle \mathcal{N},\mathcal{N}_{S_{i}}\right\rangle $ to a $\tau\cup\underline{\tau}$-structure
we have $\mathcal{P}'\not\models\underline{\Phi_{end}^{i}}$.
\end{itemize}
Let $\phi_i = \formula{\Phi_{end}^{i}}$.
 (A) and (B) are equivalent
to (C):
\begin{itemize}
\item [(C)] There exists a $\tau$-structure $\mathcal{N}$ such that $\mathcal{N}\models\Phi_{start}^{i}$
and for every extension $\mathcal{P}'$ of the $\tau\cup\underline{\rho}$-structure
$\mathcal{P}=\left\langle \mathcal{N},\mathcal{N}_{S_{i}}\right\rangle $ to a $\tau\cup\underline{\tau}$-structure
such that $\mathcal{P}'\models\bigwedge RE\land\bigwedge DI$, we have $\mathcal{P}'\models\neg\phi_i$.
\end{itemize}
The next step is to show that the set of possible extensions of $\mathcal{P}$
to $\mathcal{P}'$ with $\mathcal{P}'\models\bigwedge RE\land\bigwedge DI$ is definable.
Let $W_{i}$ be a concept which contains all possible memory cells
accessed during the run of $S_{i}$. E.g. for $S_2$ (see Fig. \ref{fig:list-example}),
\begin{eqnarray*}
W_{2} & \equiv & Z_{I}\sqcup Z_{II}\sqcup Z_{III}\\
Z_{I} & \equiv & b\\
Z_{II} & \equiv & \exists next^{-}.b\\
Z_{III} & \equiv & \exists next^{-}.\exists next^{-}.b
\end{eqnarray*}
$W_{2}$ can be extracted naively from $S_{2}$. The remaining elements
of the memory at the start of $S_{2}$ are two lists segments
\begin{eqnarray*}
Z_{IV} & \equiv & L_{b}\sqcap\neg W_{2}\\
Z_{V} & \equiv & L\sqcap\neg L_{b}\sqcap\neg W_{2}
\end{eqnarray*}
which are guaranteed not to be accessed during the run of $S_{2}$.

\begin{figure}
\begin{center}
\includegraphics[scale=0.7]{list1-diag}
\end{center}
\caption{\label{fig:list-example} The figure depicts the input of one iteration
of the loopless code $S_{2}$ inside the loop, namely a list starting
at $head$ with $b$ pointing to an element in the list. $S_{2}$
only accesses $b$, $b.next$ and $b.next.next$. Therefore, after
the execution of $S_{2}$, $Z_{IV}$ and $Z_{V}$ appear in any list
segment as entirely or not at all. }
\end{figure}

Since the elements of $Z_{IV}$ are not accessed and their pointers remain unchanged, they agree on which
list segments they belong to in $\mathcal{M}_{S_{i}}$, and similarly for
$Z_{V}$. In other words, every list segment in $\mathcal{M}_{S_{i}}$ consists
of a concatenation of a subset of the elements and list segments $\{Z_{I},\ldots,Z_{V}\}$.
I.e. every list segment in $\mathcal{M}_{S_{i}}$ can be characterized entirely
by whether, and in what order, $Z_{I},\ldots,Z_{V}$ occur in it.

Let $\sigma=\{C_{y}\mid y\subseteq\{Z_{I},\ldots,Z_{V}\}\}$ be a
vocabulary consisting of fresh concepts. For $y\subseteq\{Z_{I},\ldots,Z_{V}\}$,
let $\alpha_{y}=\bigsqcup_{Z_{s}\in y}Z_{s}\equiv C_{y}$. The formula
\[
\alpha=\bigwedge_{y\subseteq\{Z_{I},\ldots,Z_{V}\}}\alpha_{y}
\]
 defines the $C_{y}$ to be all possible candidates for list segments
in $\mathcal{M}_{S_{i}}$.

A concept $C_{y}$ is a list segment if there is a linear ordering
witnessing the concatenation of the elements and list segments in
$y$ in $\mathcal{M}_{S_{i}}$. Let $\beta_{y}^{o}$ be the disjunction over
all linear orderings $\leq$ of $y$ with minimal element $min_{\leq}$
of $\beta_{\leq}^{o}$, where
\begin{eqnarray*}
\beta_{\leq}^{o} & = & min_{\leq}\equiv o\land\bigwedge_{Z_{s}\leq Z_{t}\in y}\bot\not\equiv(\exists\underline{next}^{-}.Z_{s})\sqcap Z_{t}
\end{eqnarray*}
$\beta_{\leq}^{o}$ expresses that the elements and list segments
in $y$ are concatenated according to $\leq$ starting from $o$,
and $\beta_{y}^{o}$ expresses that such an ordering exists. E.g.,
$\alpha_{y}\land\beta_{y}^{\underline{head}}$ holds iff $C_{y}$
consists exactly of $\bigsqcup_{Z_{s}\in y}Z_{s}$ and is a list segment
starting at $\underline{head}$. Let $Y$ be the set of pairs $(y_{1},y_{2})$
of disjoint subsets of $\{Z_{I},\ldots,Z_{V}\}$. (C) is equivalent
to:
\begin{itemize}
\item [(D)] There exist a $\tau$-structure $\mathcal{N}$ such that $\mathcal{N}\models\Phi_{start}^{2}$
and we have
\[
\left\langle \mathcal{N},\mathcal{N}_{S_{2}}\right\rangle \models \gamma
\]
where $\gamma$ is
\[
\alpha\land\bigwedge_{(y_{1},y_{2})\in Y}\left(\left(\beta_{y_{1}}^{\underline{head}}\land\beta_{y_{2}}^{\underline{b}}\right)\to\neg\phi_i[\underline{L_{b}}\backslash C_{y_{1}},\underline{L}\backslash C_{y_{1}}\sqcup C_{y_{2}}]\right)
\]
The notation $\phi_i[A\backslash B]$ denotes the syntactical substitution
of $A$ with $B$ in $\phi_i$.
\end{itemize}
$\gamma$ expresses that for every two list segments starting in $\underline{head}$
and $\underline{b}$ respectively, $\phi_i$ does not hold.

Now we can turn to the symbols of $\underline{\rho}$. We can apply
backwards propagation to $head$, $b$, $\ensuremath{\mathit{Marked}}$ and $next$, i.e.
we can compute the weakest precondition predicate transformer for
each of these with respect to $S_{i}$. For $next$ we apply the transformer
directly on concepts $\exists next.C$ and $\exists next^{-}.C$ for
any $C$ which use $next$.

In \cite{arXiv:CKSVZ13} the following is proven\footnote{The description logic used in \cite{arXiv:CKSVZ13} is slightly more powerful, allowing also role inclusion. However, this is easy to overcome, see footnote \ref{foot-sub}. }:
\begin{theorem}
\label{th:back} For every disjoint vocabularies $\xi$ and $\tau$,
every $\LoiqNOb_{b}(\tau\cup\underline{\tau}\cup\xi)$-formula $\phi_i$,
and loopless code $S$, it is possible to compute
a $\LoiqNOb_{b}(\rho\cup(\underline{\tau}\backslash\underline{\rho})\cup\xi)$-formula
$\theta_{S,\phi_i}$  such that $\mathcal{P}\models\theta_{S,\phi}$
iff $\mathcal{P}'=\left\langle \mathcal{P},\mathcal{P}_{S}\right\rangle \models\phi_i$.
\end{theorem}

We apply the backwards propagation to $\gamma$.

For $S = S_{2}$,
let $\phi_{false}$ be obtained from $\gamma$
by syntactically substituting $b$ to $\exists next^{-}.b$.
Let $\phi_{true}$ be obtained from $\gamma$ by
syntactically substituting\footnote{\label{foot-sub} In \cite{arXiv:CKSVZ13} $next$ would have been subtituted syntactically for an expression such as $next \setminus (b \times \top)  \cup (\exists next^-.b \times \exists next^-.\exists next^-.b)$. Since we do not allow role inclusions and $\times$ in out logic, we make the substitutions on the concepts which use $next$ instead.  }
$\exists next.D$ to
\[\stackrel{(\bullet)}{\overbrace{(b\sqcap\exists next.\exists next.D)}}\sqcup\stackrel{(\bullet \bullet)}{\overbrace{(\neg b\sqcap\exists next.D)}}\]
and $\exists next^-.D$ to
\[
 \stackrel{(\bullet)}{\overbrace{\left(\exists next^-.\exists next^-.(b\sqcap D)\right)}} \sqcup \stackrel{(\bullet \bullet)}{\overbrace{\left( \exists next^-.(D \sqcap \neg b)\right)}}
\]
for every concept $D$.
$(\bullet)$ expresses the new value of $next$ on $b$. $(\bullet \bullet)$ expresses the unchanged values of $next$.
Then
\begin{eqnarray*}
\theta_{S_{2},\gamma} & = & (\phi_{cond}\land\phi_{true})\lor(\neg\phi_{cond}\land\phi_{false})\\
\phi_{cond} & = & \exists next^{-}.b\sqsubseteq\neg null\sqcap \ensuremath{\mathit{Marked}}
\end{eqnarray*}

As a consequence we get that (D) is equivalent to (E):
\begin{itemize}
\item [(E)] There exist a $\tau$-structure $\mathcal{N}$ such that $\mathcal{N}\models\Phi_{start}^{2}\land\theta_{S_{2},\gamma}$.
\end{itemize}
Whether (E) holds reduces to the finite satisfiablity problem of $\mathcal{ALCQIO}_{b,Re}$.

In \cite{arXiv:CKSVZ13} a functional program analysis based on Theorem
\ref{th:back} was discussed. The memory model of \cite{arXiv:CKSVZ13}
is considerably more developed in order to allow allocation and deallocation
of memory. However the step between (D) and (E) was not considered
there, leading to a program analysis which is based on an existing shape analysis.
Since the goal of this section is not to develop a program analysis
but rather give the reader intuition via an example, we did not strive
to make the formulas here most efficient or small. We will consider
the development of a full program analysis based on this logic in
future work.

redpajama_set_name: RedPajamaArXiv