text:
\section{Appendix: additional proofs}
\label{appendix}

{\bf Lemma~\ref{lemma:aux}}. {\em For $h \in \SET{2,3}$, all $s \in X,
  w \in \Omega$ we have that $w \in (\omega \,
  {\fmorph{{\cal T}}{}{s}})_h$ if and only if $(\eta \, s)_h \cap
  \fmorph{{\cal T}}{-1}{w} \not=\emptyset$.}

\begin{proof}
Since $\fmorph{{\cal T}}{}{\cdot}$ is a ${\cal T}$-homomorphism, we can make the following derivation\\\\
\noindent
$
\noindent\hspace*{.20in}\vspace{0.1in}
(\omega \, \fmorph{{\cal T}}{}{s})_h
\hint{=}{Def. of $\mathop{\raisebox{0.5pt}{\scriptsize $\circ$}}$}
((\omega \mathop{\raisebox{0.5pt}{\scriptsize $\circ$}} \fmorph{{\cal T}}{}{\cdot})s)_h
\hint{=}{$\fmorph{{\cal T}}{}{\cdot}$ is a ${\cal T}$-homomorphism}
((({\cal T} \, \fmorph{{\cal T}}{}{\cdot}) \mathop{\raisebox{0.5pt}{\scriptsize $\circ$}} \eta) s)_h
\hint{=}{Def. of $\mathop{\raisebox{0.5pt}{\scriptsize $\circ$}}$}
(({\cal T} \, \fmorph{{\cal T}}{}{\cdot})(\eta \, s))_h
\hint{=}{Def. of $({\cal T}\,\fmorph{{\cal T}}{}{\cdot})$}
\fmorph{{\cal T}}{}{(\eta\, s)_h}
$\\\\
So, $w \in (\omega \, \fmorph{{\cal T}}{}{s})_h$ if and only if $w\in \fmorph{{\cal T}}{}{(\eta\, s)_h}$.
But $w\in \fmorph{{\cal T}}{}{(\eta\, s)_h}$ if and only if there exists $s' \in (\eta\, s)_h$ such that $w = \fmorph{{\cal T}}{}{s'}$, i.e. if and only if $s' \in \fmorph{{\cal T}}{-1}{w}$.
So, $w \in (\omega \, \fmorph{{\cal T}}{}{s})_h$ if and only there exists
$s' \in (\eta\, s)_h  \cap \fmorph{{\cal T}}{-1}{w}$. \\
This proves the assert.
\qed
\end{proof}

\noindent
{\bf Lemma~\ref{lemma:slcseqsubcsbisim}}. {\em If quasi-discrete closure model $\mathcal{M}$ is finite-closure and back-finite-closure, then $\slcseq \, \subseteq\,  \altcmbisim$.}

\begin{proof}
We prove that the equivalence relation $\slcseq$ is a bisimulation  by showing that for all
$(x_1,x_2) \in \slcseq$ the five conditions of Definition~\ref{def:CMB} are satisfied\footnote{Note
that Definition~\ref{def:CMB} is used for defining $\cmbisim$, but recall that
$\altcmbisim$ coincides with $\cmbisim$.}:
\begin{enumerate}
\item $(x_1,x_2) \in \slcseq$ implies $\mathcal{M}, x_1 \models p$ if and only if $\mathcal{M}, x_2 \models p$ for
all $p \in AP$, which implies in turn that $\invpeval x_1 = \invpeval x_2 $;
\item suppose there exists $x_1' \in \forwclosure{x_1}$ such that $(x_1',x_2') \not\in\slcseq$ for all $x_2' \in \forwclosure{x_2}$. Note that  $x_1' \not=x_1$ because $x_2 \in
\forwclosure{x_2}\not=\emptyset$ and $(x_1,x_2) \in \slcseq$; moreover
$\forwclosure{x_2}$ is finite since $\mathcal{M}$ is finite-closure. Let then
$\forwclosure{x_2}=\SET{y_1, \ldots , y_n}$, with $(x_1',y_i) \not\in\slcseq$, for $i=1\ldots n$.
This implies that there would exist formulas ${\bf F}_1, \ldots , {\bf F}_n$ such that
$\mathcal{M}, x_1' \models {\bf F}_i$ and $\mathcal{M}, y_i \not\models {\bf F}_i$, for $i=1\ldots n$, by definition of $\slcseq$.
Thus we would have $\mathcal{M}, x_1' \models \bigwedge_{j=1}^{n} {\bf F}_j$ and
$\mathcal{M}, y_i \not\models \bigwedge_{j=1}^{n} {\bf F}_j$ for $i=1\ldots n$, which would imply
$\mathcal{M}, x_1 \models \lrcs{(\bigwedge_{j=1}^{n} {\bf F}_j)}{\bot}$ and
$\mathcal{M}, x_2 \not\models \lrcs{(\bigwedge_{j=1}^{n} {\bf F}_j)}{\bot}$, and this would
contradict $(x_1,x_2) \in\slcseq$. Thus we get that for all $x_1' \in \forwclosure{x_1}$ there exists
$x_2' \in \forwclosure{x_2}$ such that $(x_1',x_2')\in \slcseq$;
\item symmetric to the case above;
\item suppose  there exists $x_1' \in \backclosure{x_1}$ such that $(x_1',x_2') \not\in\slcseq$ for all $x_2' \in \backclosure{x_2}$. Note that  $x_1' \not=x_1$ because $x_2 \in
\backclosure{x_2}\not=\emptyset$ and $(x_1,x_2) \in \slcseq$; moreover
$\backclosure{x_2}$ is finite since $\mathcal{M}$ is finite-back-closure. Let then
$\backclosure{x_2}=\SET{y_1, \ldots , y_n}$, with $(x_1',y_i) \not\in\slcseq$, for $i=1\ldots n$.
This implies that there would exist formulas ${\bf F}_1, \ldots , {\bf F}_n$ such that
$\mathcal{M}, x_1' \models {\bf F}_i$ and $\mathcal{M}, y_i \not\models {\bf F}_i$, for $i=1\ldots n$, by definition of $\slcseq$.
Thus we would have $\mathcal{M}, x_1' \models \bigwedge_{j=1}^{n} {\bf F}_j$ and
$\mathcal{M}, y_i \not\models \bigwedge_{j=1}^{n} {\bf F}_j$ for $i=1\ldots n$, which would imply
$\mathcal{M}, x_1 \models \lrcd{(\bigwedge_{j=1}^{n} {\bf F}_j)}{\bot}$ and
$\mathcal{M}, x_2 \not\models \lrcd{(\bigwedge_{j=1}^{n} {\bf F}_j)}{\bot}$, and this would
contradict $(x_1,x_2) \in\slcseq$. Thus we get that for all $x_1' \in \backclosure{x_1}$ there exists
$x_2' \in \backclosure{x_2}$ such that $(x_1',x_2')\in \slcseq$;
\item symmetric to the case above. \qed
\end{enumerate}
\end{proof}

\noindent
{\bf Lemma~\ref{lemma:csbisimsubslcseq}}. {\em
If $\mathcal{M}$ is a quasi-discrete closure model, then $ \altcmbisim\, \subseteq\,  \slcseq$.}

\medskip
\noindent The proof requires the following lemma.

\begin{lemma}\label{lemma:CFBB}
    For all quasi-discrete models $\mathcal{M} = ((X,\closurename{R}), {\cal V})$,
    formulas $\Phi$ and $\Psi$, and $x,x' \in X$ the following holds:
    \begin{enumerate}
    \item
    if $x' \in \forwclosure{x}$ and $\mathcal{M},x' \models \Phi$ then $\mathcal{M}, x \models \lrcs{\Phi}{\Psi}$;
    \item
    if $x' \in \backclosure{x}$ and $\mathcal{M},x' \models \Phi$ then $\mathcal{M}, x \models \lrcd{\Phi}{\Psi}$.
    \end{enumerate}
\end{lemma}

\begin{proof}(of Lemma~\ref{lemma:CFBB})
    Keeping in mind that $Y \subseteq \mathcal{C}{}{Y}$ for all $Y \subseteq X$
    \begin{enumerate}
    \item
    take  $\pi: \mathbb{N} \to X$ with $\pi(0) = x$ and $\pi(j) = x'$ for all $j\in \mathbb{N}, j>0$;
    $\pi$ is a path since for all $N \subseteq \mathbb{N}$ we have
    $$
    \pi(\mathcal{C}{Succ}{N})=
    \left\{
    \begin{array}{l}
    \emptyset, \mbox{ if } N=\emptyset,\\
    \SET{x'}, \mbox{ if } 0\not\in N\not=\emptyset,\\
    \SET{x,x'}, \mbox{ if } 0\in N.
    \end{array}
    \right.
    \quad
    \mathcal{C}{R}{\pi(N)}=
    \left\{
    \begin{array}{l}
    \emptyset, \mbox{ if } N=\emptyset,\\
    \mathcal{C}{R}{\SET{x'}}, \mbox{ if } 0\not\in N\not=\emptyset,\\
    \mathcal{C}{R}{\SET{x,x'}}, \mbox{ if } 0\in N.\\
    \end{array}
    \right.
    $$
    so that $\pi(\mathcal{C}{Succ}{N}) \subseteq \mathcal{C}{R}{(\pi N)}$;
    \item
    note that if $x' \in \backclosure{x}$ then $x \in \forwclosure{x'}$ and
    take  $\pi: \mathbb{N} \to X$ with $\pi(0) = x'$ and $\pi(j) = x$ for all $j\in \mathbb{N}, j>0$;
    $\pi$ is a path since for all $N \subseteq \mathbb{N}$ we have
    $$
    \pi(\mathcal{C}{Succ}{N})=
    \left\{
    \begin{array}{l}
    \emptyset, \mbox{ if } N=\emptyset,\\
    \SET{x}, \mbox{ if } 0\not\in N\not=\emptyset,\\
    \SET{x,x'}, \mbox{ if } 0\in N.
    \end{array}
    \right.
    \quad
    \mathcal{C}{R}{\pi(N)}=
    \left\{
    \begin{array}{l}
    \emptyset, \mbox{ if } N=\emptyset,\\
    \mathcal{C}{R}{\SET{x}}, \mbox{ if } 0\not\in N\not=\emptyset,\\
    \mathcal{C}{R}{\SET{x,x'}}, \mbox{ if } 0\in N.
    \end{array}
    \right.
    $$
    so that $\pi(\mathcal{C}{Succ}{N}) \subseteq \mathcal{C}{R}{(\pi N)}$.\qed
    \end{enumerate}
\end{proof}

\begin{proof}(of Lemma~\ref{lemma:csbisimsubslcseq})
By induction on the structure of ${\bf F}$ we prove that, for all
$x_1, x_2 \in X$ and for all $ SLCS\xspace$  formulas ${\bf F}$ ,  if $(x_1,x_2) \in \altcmbisim$, then
$\mathcal{M}, x_1 \models {\bf F}$ if and only if $\mathcal{M}, x_2 \models {\bf F}$.

\noindent
{\bf Base case} $p$:\\
$(x_1,x_2) \in \altcmbisim$ implies $\invpeval x_1 =\invpeval x_2 $ which implies in turn
$\mathcal{M}, x_1 \models p$ if and only if $\mathcal{M}, x_2 \models p$, for all $p\in AP$.\\

\noindent
{\bf Induction steps}\\
We assume the induction hypothesis---for all $x_1,x_2 \in X$, if $(x_1,x_2) \in \altcmbisim$, then the following holds
$\mathcal{M}, x_1 \models {\bf F}$ if and only if $\mathcal{M}, x_2 \models {\bf F}$ for any $SLCS\xspace$  formula $\Phi$---and we prove the following cases, for any $(x_1,x_2) \in \altcmbisim$:\\
{\bf Case} $\neg{\bf F}$:\\
Suppose $\mathcal{M}, x_1 \models \neg{\bf F}$ and $\mathcal{M}, x_2 \not\models \neg{\bf F}$.
This would imply $\mathcal{M}, x_1 \not\models {\bf F}$ and $\mathcal{M}, x_2 \models {\bf F}$ and since
$(x_1,x_2) \in \altcmbisim$, this would contradict the induction hypothesis.

\noindent
{\bf Case} $\Phi\, \land \Psi$:\\
Suppose $\mathcal{M}, x_1 \models \Phi\, \land \Psi$ and $\mathcal{M}, x_2 \not\models \Phi\, \land \Psi$
and w.l.g. assume $\mathcal{M}, x_2 \not\models \Phi$.
Then we would get $\mathcal{M}, x_1 \models \Phi$ and $\mathcal{M}, x_2 \not\models \Phi$ and since
$(x_1,x_2) \in \altcmbisim$, this would contradict the induction hypothesis.

\noindent
{\bf Case} $\lrcs{\Phi}{\Psi}$:\\
Suppose $\mathcal{M}, x_1 \models \lrcs{\Phi}{\Psi}$ and $\mathcal{M}, x_2 \not\models \lrcs{\Phi}{\Psi}$.
$\mathcal{M}, x_1 \models \lrcs{\Phi}{\Psi}$ means there exists path $\pi_1$ and index $\ell$ such that
$\pi_1(0)=x_1, \mathcal{M},\pi_1(\ell) \models \Phi$ and $\mathcal{M},\pi_1(j) \models \Psi$ for all
$j \in I_{\ell}$ where we define $I_n$ as $I_n = \SET{1,\ldots n-1}$. We distinguish three cases:
\begin{itemize}
\item $\ell=0$: in this case, by definition of $\lrcs{\Phi}{\Psi}$, $\mathcal{M}, x_1 \models \Phi$;
on the other hand, since  $\mathcal{M}, x_2 \not\models \lrcs{\Phi}{\Psi}$
by hypothesis, it should hold $\mathcal{M}, x_2 \not\models \Phi$, but since
$(x_1,x_2) \in \altcmbisim$, this would contradict the induction hypothesis;
\item  $\ell=1$: in this case $\mathcal{M}, \pi_1(1) \models \Phi$ and, by continuity of $\pi_1$,
we would have that $\pi_1(1)\in\mathcal{C}{R}{\SET{x_1}}$;
in fact, continuity of $\pi_1$ implies $\pi_1(\mathcal{C}{R}{\SET{0}}) \subseteq
\mathcal{C}{\succ}{(\pi_1(\SET{0}))}$, so that we get the following derivation:
$
\pi_1(1) \in \SET{\pi_1(0),\pi_1(1)} \\ = \pi_1(\SET{0,1}) =
\pi_1(\mathcal{C}{\succ}{\SET{0}}) \subseteq
\mathcal{C}{R}{(\pi_1(\SET{0}))} =
\mathcal{C}{R}{\SET{\pi_1(0)}} =
\mathcal{C}{R}{\SET{x_1}}
$;
that is, there exists $x_1' \in\forwclosure{x_1}$  such that
$\mathcal{M}, x_1' \models \Phi$; on the other hand, since  $\mathcal{M}, x_2 \not\models \lrcs{\Phi}{\Psi}$
by hypothesis, it should hold $\mathcal{M}, x_2' \not\models \Phi$ for all $x_2' \in\forwclosure{x_2}$,
due to Lemma~\ref{lemma:CFBB}(1) below;
moreover, we know that $(x_1,x_2) \in \altcmbisim$, which, by definition of $\altcmbisim$, and recalling that
$\altcmbisim$ coincides with $\cmbisim$, implies that there would exist $x_2' \in\forwclosure{x_2}$
such that $(x_1',x_2') \in \altcmbisim$; but then we would have
$\mathcal{M}, x_1' \models \Phi$ and $\mathcal{M}, x_2' \not\models \Phi$ that contradicts the induction hypothesis;
\item $\ell>1$: in this case we can build a path $\pi_2$ as follows: $\pi_2(0)=x_2$,
{$\pi_2(j) \in \; \forwclosure{\pi_2(j-1)}$} for $j\in I_{\ell}$, and $(\pi_1(j),\pi_2(j))\in \altcmbisim$ for
$j=0, \ldots \ell-1$; in fact $(\pi_1(0),\pi_2(0))\in \altcmbisim$ by hypothesis and this
implies there exists $x_2' \in \forwclosure{\pi_2(0)}$ such that $(\pi_1(1),x_2')\in \altcmbisim$ and we
let $\pi_2(1)=x_2'$; a similar reasoning can now be applied starting from
$(\pi_1(1),\pi_2(1))\in \altcmbisim$, $(\pi_1(2),\pi_2(2))\in \altcmbisim$
and so on till $(\pi_1(\ell-1),\pi_2(\ell-1))\in \altcmbisim$; since $\mathcal{M},\pi_1(j) \models \Psi$ for
all $j\in I_{\ell}$, by the induction hypothesis we get that also $\mathcal{M},\pi_2(j) \models \Psi$ for
all $j\in I_{\ell}$; note moreover that  $\mathcal{M},\pi_2(j) \not\models \Phi$ for all $j=0,\ldots,\ell-1$ since, by hypothesis,
$\mathcal{M}, x_2 \not\models \lrcs{\Phi}{\Psi}$ and, for the same reason, it should also be the case that
$\mathcal{M},z \not\models \Phi$ for all $z \in \forwclosure{\pi_2(\ell-1)}$; and since
$(\pi_1(\ell-1),\pi_2(\ell-1))\in \altcmbisim$ there should be a $z \in \forwclosure{\pi_2(\ell-1)}$
such that  $(\pi_1(\ell), z) \in \altcmbisim$; but then, the induction hypothesis would be violated
by $\mathcal{M}, \pi_1(\ell) \models \Phi$ and $\mathcal{M}, z \not\models \Phi$.
\end{itemize}

\noindent
{\bf Case} $\lrcd{\Phi}{\Psi}$:\\
Suppose $\mathcal{M}, x_1 \models \lrcd{\Phi}{\Psi}$ and $\mathcal{M}, x_2 \not\models \lrcd{\Phi}{\Psi}$.
$\mathcal{M}, x_1 \models \lrcd{\Phi}{\Psi}$ means there exists path $\pi_1$ and index $\ell$ such that
$\pi_1(\ell)=x_1, \mathcal{M},\pi_1(0) \models \Phi$ and $\mathcal{M},\pi_1(j) \models \Psi$ for all
$j \in I_{\ell}$. We distinguish three cases:
\begin{itemize}
\item $\ell=0$: in this case, by definition of $\lrcd{\Phi}{\Psi}$, $\mathcal{M}, x_1 \models \Phi$;
on the other hand, since  $\mathcal{M}, x_2 \not\models \lrcd{\Phi}{\Psi}$
by hypothesis, it should hold that $\mathcal{M}, x_2 \not\models \Phi$, but since
$(x_1,x_2) \in \altcmbisim$, this would contradict the induction hypothesis;
\item  $\ell=1$: in this case we have $\mathcal{M}, \pi_1(0) \models \Phi$ and  $\pi_1(1) = x_1$.
We first note that, by continuity of $\pi_1$, we have $x_1 \in \mathcal{C}{R}{\SET{\pi_1(0)}}$:
$
x_1 =
\pi_1(1) \in
\SET{\pi_1(0),\pi_1(1)} =
\pi_1(\SET{0,1})=
\pi_1(\mathcal{C}{\succ}{\SET{0}}) \subseteq
\mathcal{C}{R}{\pi_1(\SET{0})}=
\mathcal{C}{R}{(\SET{\pi_1(0)})}
$.
This means that there exists $x_1' \in \backclosure{x_1}$ such that $\mathcal{M}, x_1' \models \Phi$, namely $x_1'=\pi_1(0)$. We also know that $\mathcal{M}, x_2' \not\models \Phi$ for all
 $x_2' \in \backclosure{x_2}$, otherwise, by Lemma~\ref{lemma:CFBB}(2) below, $\mathcal{M}, x_2 \models \lrcd{\Phi}{\Psi}$ would hold,
 which is not the case by hypothesis. On the other hand, again by hypothesis we know that
$(x_1,x_2) \in \altcmbisim$, and so, given that $x_1' \in \backclosure{x_1}$, there must also be
some $x_2'' \in \backclosure{x_2}$ such that $(x_1',x_2'') \in \altcmbisim$. But this,
by the induction hypothesis, implies that $\mathcal{M}, x_2'' \models \Phi$ which
contradicts the fact that $\mathcal{M}, x_2' \not\models \Phi$ for all
 $x_2' \in \backclosure{x_2}$.
\item $\ell>1$: in this case we can build a path $\pi_2$ as follows: $\pi_2(\ell)=x_2$,
$\quad \pi_2(j) \; \in \; \forwclosure{\pi_2(j-1)}$ for $j\in I_{\ell}$, and $(\pi_1(j),\pi_2(j))\in \altcmbisim$ for
$j=0, \ldots \ell-1$; in fact $(\pi_1(\ell),\pi_2(\ell))\in \altcmbisim$ by hypothesis and this
implies there exists $x_2' \in \backclosure{x_2}$ such that $(\pi_1(\ell-1),x_2')\in \altcmbisim$,
because $\pi_1(\ell -1)\in \backclosure{x_1}$.
We let $\pi_2(\ell-1)=x_2'$; a similar reasoning can now be applied starting from
$(\pi_1(\ell-1),\pi_2(\ell-1))\in \altcmbisim$,
and so on till $(\pi_1(1),\pi_2(1))\in \altcmbisim$.
Since $\mathcal{M},\pi_1(j) \models \Psi$ for all $j\in I_{\ell}$, by the induction
hypothesis we get that also $\mathcal{M},\pi_2(j) \models \Psi$ for
all $j\in I_{\ell}$; note moreover that  $\mathcal{M},\pi_2(j) \not\models \Phi$ for all $j=0,\ldots,\ell-1$, because
$\mathcal{M}, x_2 \not\models \lrcd{\Phi}{\Psi}$ and, for the same reason, it should also be the case that
$\mathcal{M},z \not\models \Phi$ for all $z \in \backclosure{\SET{\pi_2(1)}}$.
But we know that $(\pi_1(1),\pi_2(1)) \in \altcmbisim$ and that
$\pi_1(0) \in\backclosure{\pi_1(1)}$, so there should be $z \in \backclosure{\pi_2(1)}$
and $(\pi_1(0),z) \in \altcmbisim$ and that $\mathcal{M}, \pi_1(0)\models \Phi$. For the
induction hypothesis, then, we should have also $\mathcal{M}, z \models \Phi$, which brings
to contradiction.
\end{itemize}
This completes the proof.
\end{proof}

\noindent
{\bf Lemma~\ref{lemma:restrict}}. {\em
For ${\bf F}_1,{\bf F}_2$ formulas of $\SMCSm$ of Equation~\ref{eq:sublogic},
\begin{enumerate}
\item
if $\mathcal{M}, x_1 \models \lrcs{{\bf F}_1}{{\bf F}_2}$
and $\mathcal{M}, x_2 \not\models \lrcs{{\bf F}_1}{{\bf F}_2}$
then there exists $\Lambda_{{\bf F}_1,{\bf F}_2}$
in the language of Equation~\ref{eq:sublogic} such that
$\mathcal{M}, x_1 \models \Lambda_{{\bf F}_1,{\bf F}_2} $
and $\mathcal{M}, x_2 \not\models \Lambda_{{\bf F}_1,{\bf F}_2} $;
\item
if $\mathcal{M}, x_1 \models \lrcd{{\bf F}_1}{{\bf F}_2}$
and $\mathcal{M}, x_2 \not\models \lrcd{{\bf F}_1}{{\bf F}_2}$
then there exists $\Lambda_{{\bf F}_1,{\bf F}_2}$
in the language of Equation~\ref{eq:sublogic} such that
$\mathcal{M}, x_1 \models \Lambda_{{\bf F}_1,{\bf F}_2} $
and $\mathcal{M}, x_2 \not\models \Lambda_{{\bf F}_1,{\bf F}_2} $.
\end{enumerate}
}

\begin{proof}
$ $\\
For what concerns item (1),
there are three cases for $\mathcal{M}, x_1 \models \lrcs{{\bf F}_1}{{\bf F}_2}$.\\
{\bf Case 1:} $\ell = 0$.\\
By definition of the ${\stackrel{\rightarrow}{\rho}}$ operator, in this case we have $\mathcal{M}, x_1 \models {\bf F}_1$.
On the other hand, since $\mathcal{M}, x_2 \not\models \lrcs{{\bf F}_1}{{\bf F}_2}$,
we have $\mathcal{M}, x_2 \not\models {\bf F}_1$, otherwise
$\mathcal{M}, x_2 \models \lrcs{{\bf F}_1}{{\bf F}_2}$ would hold, by definition of ${\stackrel{\rightarrow}{\rho}}$.
So, in this case  $\Lambda_{{\bf F}_1,{\bf F}_2} = {\bf F}_1$.\\
{\bf Case 2:} $\ell = 1$.\\
By definition of the ${\stackrel{\rightarrow}{\rho}}$ operator, in this case we have that
there exists a path $\pi_1$ such that $\pi_1(0)=x_1$ and
$\mathcal{M}, \pi_1(1) \models {\bf F}_1$.
This means that
$\mathcal{M}, x_1 \models \lrcs{{\bf F}_1}{\bot}$. On the other hand,
from the fact that $\mathcal{M}, x_2 \not\models \lrcs{{\bf F}_1}{{\bf F}_2}$ we get,
again by definition of  ${\stackrel{\rightarrow}{\rho}}$,
$\mathcal{M}, x_2 \not\models \lrcs{{\bf F}_1}{\bot}$.
So, in this case, $\Lambda_{{\bf F}_1,{\bf F}_2} = \lrcs{{\bf F}_1}{\bot}$.
\\
{\bf Case 3:} $\ell = k>1$.\\
By definition of the ${\stackrel{\rightarrow}{\rho}}$ operator, in this case we have that
there exists a path $\pi_1$ such that $\pi_1(0)=x_1$,
$\mathcal{M}, \pi_1(k) \models {\bf F}_1$ and $\mathcal{M}, \pi_1(j) \models {\bf F}_2$, for
$0<j<k$.

\noindent
It  is easy to see that:\\
$\mathcal{M}, \pi_1(k-1) \models {\bf F}_2 \, \land \,
\lrcs{{\bf F}_1}{\bot}$\\
$\mathcal{M}, \pi_1(k-2) \models {\bf F}_2 \, \land \,
\lrcs{({\bf F}_2 \, \land \, \lrcs{{\bf F}_1}{\bot})}{\bot}$\\
\vdots\\
$\mathcal{M}, x_1  \models \Psi$
where
$\Psi =
\underbrace{
\lrcs
{({\bf F}_2 \, \land \,
\lrcs{(\ldots \, \land \, \lrcs{({\bf F}_2 \, \land \, \lrcs{{\bf F}_1}{\bot})}{\bot} \ldots}{\bot})
)
}
{\bot}
}_{k \mbox{ times } {\stackrel{\rightarrow}{\rho}}}
$,\\
and that:
$\mathcal{M}, x_2  \models \Psi$
does not hold, otherwise one could easily build a
path $\pi_2$ with $\pi_2(0)=x_2$,
$\mathcal{M}, \pi_2(k) \models {\bf F}_1$ and $\mathcal{M}, \pi_2(j) \models {\bf F}_2$, for
$0<j<k$ and, consequently we would have $\mathcal{M}, x_2 \models \lrcs{{\bf F}_1}{{\bf F}_2}$.
So, in this case, $\Lambda_{{\bf F}_1,{\bf F}_2} = \Psi$.

\noindent
For what concerns point (2),
there are three cases for $\mathcal{M}, x_1 \models \lrcd{{\bf F}_1}{{\bf F}_2}$.\\
{\bf Case 1:} $\ell = 0$.\\
By definition of the ${\stackrel{\leftarrow}{\rho}}$ operator, in this case we have $\mathcal{M}, x_1 \models {\bf F}_1$.
On the other hand, since $\mathcal{M}, x_2 \not\models \lrcd{{\bf F}_1}{{\bf F}_2}$,
we have $\mathcal{M}, x_2 \not\models {\bf F}_1$, otherwise
$\mathcal{M}, x_2 \models \lrcd{{\bf F}_1}{{\bf F}_2}$ would hold, by definition of ${\stackrel{\leftarrow}{\rho}}$.
So, in this case  $\Lambda_{{\bf F}_1,{\bf F}_2} = {\bf F}_1$.\\
{\bf Case 2:} $\ell = 1$.\\
By definition of the ${\stackrel{\leftarrow}{\rho}}$ operator, in this case we have that
there exists a path $\pi_1$ such that $\mathcal{M}, \pi_1(0) \models {\bf F}_1$ and
$\pi_1(1)=x_1$.
This means that
$\mathcal{M}, x_1 \models \lrcd{{\bf F}_1}{\bot}$. On the other hand,
from the fact that $\mathcal{M}, x_2 \not\models \lrcd{{\bf F}_1}{{\bf F}_2}$ we get,
again by definition of  ${\stackrel{\leftarrow}{\rho}}$,
$\mathcal{M}, x_2 \not\models \lrcd{{\bf F}_1}{\bot}$.
So, in this case, $\Lambda_{{\bf F}_1,{\bf F}_2} = \lrcd{{\bf F}_1}{\bot}$.
\\
{\bf Case 3:} $\ell = k>1$.\\
By definition of the ${\stackrel{\leftarrow}{\rho}}$ operator, in this case we have that
there exists a path $\pi_1$ such that $\mathcal{M}, \pi_1(0) \models {\bf F}_1$,
$\pi_1(k)=x_1$, and $\mathcal{M}, \pi_1(j) \models {\bf F}_2$, for
$0<j<k$.

\noindent
It  is easy to see that:\\
$\mathcal{M}, \pi_1(1) \models {\bf F}_2 \, \land \,
\lrcd{{\bf F}_1}{\bot}$\\
$\mathcal{M}, \pi_1(2) \models {\bf F}_2 \, \land \,
\lrcd{({\bf F}_2 \, \land \, \lrcd{{\bf F}_1}{\bot})}{\bot}$\\
\vdots\\
$\mathcal{M}, x_1  \models \Gamma$
where
$\Gamma =
\underbrace{
\lrcd
{({\bf F}_2 \, \land \,
\lrcd{(\ldots \, \land \, \lrcd{({\bf F}_2 \, \land \, \lrcd{{\bf F}_1}{\bot})}{\bot} \ldots}{\bot})
)
}
{\bot}
}_{k \mbox{ times } {\stackrel{\leftarrow}{\rho}}}
$,\\
and that:\\
$\mathcal{M}, x_2  \models \Gamma$
does not hold, otherwise one could easily build a
path $\pi_2$ with $\mathcal{M}, \pi_2(0) \models {\bf F}_1$,  $\pi_2(k)=x_2$,
and $\mathcal{M}, \pi_2(j) \models {\bf F}_2$, for
$0<j<k$ and, consequently we would have $\mathcal{M}, x_2 \models \lrcd{{\bf F}_1}{{\bf F}_2}$.
So, in this case $\Lambda_{{\bf F}_1,{\bf F}_2} = \Gamma$.
\qed
\end{proof}

\noindent{\bf Lemma~\ref{lem:quotientsOfClosureCoalgebras}.}
    Consider $((X,\closurename{X}),\calV)$ and ${\cal X} = (X,\eta)$ as in
    Definition \ref{def:closureCoalgebraOfAModel}. Let ${\cal Y} = (Y,\theta)$ be a
    $\textbf{C}$-coalgebra. Let $f : {\cal X} \twoheadrightarrow {\cal Y}$ be a
    surjective coalgebra homomorphism. Define $\mathcal{C}{Y}{(B \subseteq Y)} =
    \{ y \in Y \mid B \in (\theta y)_2 \}$. Then $(Y,\closurename{Y})$ is a
    closure space.

    \medskip

    \noindent The proof requires the following lemma and its corollary.

    \begin{lemma}\label{lem:closure-and-image}
        Consider $((X,\closurename{X}),\calV)$ and ${\cal X} = (X,\eta)$ as in
    Definition \ref{def:closureCoalgebraOfAModel}. Let ${\cal Y} = (Y,\theta)$ be a $\textbf{C}$-coalgebra. Let $f : {\cal X}
    \to {\cal Y}$ be a (not necessarily surjective)
    coalgebra homomorphism. Define $\mathcal{C}{Y}{(B \subseteq Y)} = \{ y \in Y
    \mid B \in (\theta y)_2 \}$. It holds that $\forall A \subseteq X . \forall
    x \in X . x \in \mathcal{C}{X}{A} \iff f x \in \mathcal{C}{Y}{(\pws f)A}$, that
    is, $\mathcal{C}{X}{A} = f^{-1}(\mathcal{C}{Y}{(\pws f)A})$.
    \end{lemma}

    \begin{corollary}\label{cor:closure-and-epi-image}
        Under the conditions of Lemma~\ref{lem:quotientsOfClosureCoalgebras}, that is, whenever Lemma~\ref{lem:closure-and-image} holds, and $f$ is surjective, for $B \subseteq Y$, we have $\mathcal{C}{Y}{B} = (\pws f) \mathcal{C}{X}{f^{-1}B}$.
    \end{corollary}

    \begin{proof}(of Lemma~\ref{lem:closure-and-image})
    $\nh{}
    x \in \mathcal{C}{X}{A} \iff A \in (\eta x)_2 \iff (\pws f) A \in ((\textbf{C} f) \eta x)_2 \hint{\iff}{\text{$f$ is a coalgebra homomorphism}} (\pws f) A \in (\theta f x)_2 \iff f x \in \mathcal{C}{Y}{(\pws f) A}
    $\qed
    \end{proof}

\begin{proof}(of Lemma~\ref{lem:quotientsOfClosureCoalgebras})

    \medskip
    \noindent {\bf If $\mathcal{C}{X}{\emptyset} = \emptyset$ holds}, we have:
    $\nh{}
    \mathcal{C}{Y}{\emptyset}
    \hint = {\text{Corollary~\ref{cor:closure-and-epi-image}}}
    (\pws f)(\mathcal{C}{X}{\emptyset})
    \hint{=}{\text{Hypothesis on $\closurename{X}$}}
    \pws f \emptyset
    \nh =
    \emptyset
    $\qed

    \medskip \noindent {\bf If $\forall A \subseteq X . A \subseteq \mathcal{C}{X}{A}$ holds}, for $B \subseteq Y$, by the hypothesis $f^{-1}B \subseteq \mathcal{C}{X}{f^{-1} B}$, and $f$ being surjective, $B \subseteq (\pws f) \mathcal{C}{X}{f^{-1} B}$, and by Corollary~\ref{cor:closure-and-epi-image}, $B \subseteq \mathcal{C}{Y}{B}$. \qed

    \medskip \noindent {\bf If $\forall A,B \subseteq X . (\mathcal{C}{X}{A})\cup (\mathcal{C}{X}{B}) = \mathcal{C}{X}{(A \cup B)}$ holds}, for $C,D \subseteq Y$, we have
    $\nh{}
    \mathcal{C}{Y}{(C \cup D)}
    \hint = {\text{Corollary~\ref{cor:closure-and-epi-image}}}
    (\pws f)(\mathcal{C}{X}{f^{-1}(C \cup D)})
    \nh =
    (\pws f)(\mathcal{C}{X}{((f^{-1}C) \cup (f^{-1}D))})
    \hint = {\text{Hypothesis on $\closurename{X}$}}
    (\pws f)((\mathcal{C}{X}{f^{-1}C}) \cup  (\mathcal{C}{X}{f^{-1}D}))
    \nh =
    ((\pws f)(\mathcal{C}{X}{f^{-1}C})) \cup  ((\pws f)(\mathcal{C}{X}{f^{-1}D}))
    \hint = {\text{Corollary~\ref{cor:closure-and-epi-image}}}
    (\mathcal{C}{Y}{C}) \cup (\mathcal{C}{Y}{D})
    $\qed
\end{proof}

\noindent \textbf{Lemma \ref{lem:closure-of-equivalent-points}.}
    Let $f$ be the function mapping each element of $X$ into its equivalence classs up to $\inflogeq$. For all $x_1,x_2 \in X$ and $A \subseteq X$,  it holds that $((x_1 \inflogeq x_2) \land x_1 \in \mathcal{C}{X} A) \implies x_2 \in \closurename{X} f^{-1} (\pws f) A$.
\medskip

\begin{proof}
    For any $x \in X$ let $\chi_x$ be a formula that holds on any $x'$ if and only if $x' \inflogeq x$; such a formula is the (possibly infinite) conjunction of the formulas telling apart $[x]$ from the other equivalence classes of $\inflogeq$. Let $\Sigma = \bigwedge_{z \notin f^{-1} (\pws f) A} \lnot \chi_z$. We have $\mathcal{M},y \models \Sigma \iff y \in f^{-1} (\pws f) A$.

    It is true that $A \subseteq f^{-1} (\pws f) A$. Therefore, by properties of closure spaces, we have $\mathcal{C}{X}{A} \subseteq \mathcal{C}{X}f^{-1} (\pws f) A$. Thus, by the hypothesis $x_1 \in \mathcal{C}{X} A$, we have $\mathcal{M}, x_1 \models \mathcal{N} \Sigma$. By logical equivalence, also $\mathcal{M}, x_2 \models \mathcal{N} \Sigma$. Therefore $x_2 \in \closurename{X}{f^{-1}(\pws f) A}$. \qed
\end{proof}

\section{Bisimilarity for Quasi-discrete Closure Models}
\label{sec:CMBisimilarity}

In this section we give a back-and-forth definition of bisimilarity in
quasi-discrete closure spaces, and an alternative
characterization that makes explicit use of the underlying closure.

\begin{definition}
  \label{def:CMB}
  Given quasi-discrete closure model $\mathcal{M}=((X,\closurename{R}),
  \calV)$ based on~$R$, a non-empty relation $B \subseteq X
  \times X$ is a \emph{bisimulation relation} if for all $x_1,x_2 \in
  X$ such that $(x_1,x_2) \in B$, all five conditions below hold:
  \begin{enumerate}
  \item $\invpeval{x_1}=\invpeval{x_2}$
  \item for all $x_1' \in \forwclosure{x_1}$ there exists $x_2' \in
    \forwclosure{x_2}$ such that $(x_1',x_2') \in B$
  \item for all $x_2' \in \forwclosure{x_2}$ there exists $x_1' \in
    \forwclosure{x_1}$ such that $(x_1',x_2') \in B$
  \item for all $x_1' \in \backclosure{x_1}$ there exists $x_2' \in
    \backclosure{}{x_2}$ such that $(x_1',x_2') \in B$
  \item for all $x_2' \in \backclosure{}{x_2}$ there exists $x_1' \in
    \backclosure{}{x_1}$ such that $(x_1',x_2') \in B.$
  \end{enumerate}
  We say that $x_1$ and~$x_2$ are \emph{bisimilar} (written $x_1
  \cmbisim^{\mathcal{M}} x_2$) if there exists a bisimulation relation~$B$
  for~$X$ such that $(x_1,x_2) \in B$.
\end{definition}

\noindent
In the sequel, for the sake of notational simplicity, we will write
$\cmbisim$ instead of $\cmbisim^{\mathcal{M}}$ whenever this does not cause
confusion.

  \begin{figure}[h]
    \centering
    \centerline{\resizebox{0.7in}{!}
      {\includegraphics{figs/RemOneCounterex}}}
    \caption{A model}\label{fig:RemOneCounterex}
  \end{figure}

\begin{remark}
  \label{rem:BaFbis}
  Bisimilarity for quasi-discrete closure models is reminiscent to strong
  back-and-forth bisimilarity~\cite{De+90} and is stronger than a
  spatial version of standard bisimilarity that would include only
  items 1 to~3 above.

  In order to illustrate this, consider the model~$\mathcal{M}$ of
  Figure~\ref{fig:RemOneCounterex}, where $\mathcal{M} =
  ((X,\closurename{}),{\cal V})$ with $X = \SET{x_1,x_2,x'_1, x'_2}$,
  the closure operator~$\closurename{}$ defined by
  $\mathcal{C}{}{x_j}=\SET{x_j}$ and $\mathcal{C}{}{x'_j}=\SET{x_j,x'_j }$
  for $j = 1,2$ and valuation~${\cal V}$ such that $\invpeval x'_1 \neq
  \invpeval x'_2$ but $\invpeval x_1 = \invpeval x_2$. Furthermore,
  let $B$ be the reflexive and symmetric closure of
  $\SET{(x_1,x_2)}$. Then $B$ would be a standard bisimulation showing
  the points $x_1$ and~$x_2$ bisimilar, since only items 1 to 3 of
  Definition~\ref{def:CMB} are considered.  However, we have $x_1
  \not\cmbisim x_2$ according to Definition~\ref{def:CMB}, because of
  items 4 and~5. As we will see in Section~\ref{sec:SLCSEq}, this is
  directly related to the semantics of logic operator~${\stackrel{\leftarrow}{\rho}}$.
\end{remark}

\noindent
Given a quasi-discrete closure model $\mathcal{M}=((X,\closurename{R}),
\calV)$, it is easy to see that $\cmbisim^{\mathcal{M}}$ is an
equivalence relation and it is itself a bisimulation relation, namely
the union of all bisimulation relations, i.e.\ the largest (coarsest)
bisimulation relation.

In the following, we provide an alternative, equivalent, definition of
bisimilarity, which will prove useful for the developments in
Section~\ref{sec:CMCoalgebraically} and Section~\ref{sec:SLCSEq}.

\begin{definition}
  \label{def:altCMB}
  Given quasi-discrete closure model $\mathcal{M}=((X,\closurename{R}),
  \calV)$ based on $R$, a non-empty equivalence relation $B
  \subseteq X \times X$ is a \emph{bisimulation relation} if for all
  $x_1,x_2 \in X$ such that $(x_1,x_2) \in B$ it holds that
  \begin{enumerate}
  \item $\invpeval{x_1}=\invpeval{x_2}$, and
    \smallskip
  \item for all equivalence classes $C \in X/B$ both the following conditions hold:
    \begin{enumerate}
    \item $(\forwclosure{x_1}) \cap C \not= \emptyset$ iff
      $(\forwclosure{x_2}) \cap C \not= \emptyset$
    \item $(\backclosure{x_1}) \cap C \not= \emptyset$ iff
      $(\backclosure{}{x_2}) \cap C \not= \emptyset.$
    \end{enumerate}
  \end{enumerate}
  We say that $x_1$ and~$x_2$ are \emph{bisimilar}, notation $x_1
  \altcmbisim^{\mathcal{M}} x_2$) if there exists a bisimulation
  relation~$B$ such that $(x_1,x_2) \in B$.
\end{definition}

\noindent
In the following, for the sake of notational simplicity, we will write
$\altcmbisim$ instead of $\altcmbisim^{\mathcal{M}}$ whenever this does not
cause confusion.

Given a quasi-discrete closure model $\mathcal{M} = ((X,\closurename{R}),
\calV)$, also for~$\altcmbisim^{\mathcal{M}}$ it is easy to see that
it is an equivalence relation and that it is in fact the largest
(coarsest) bisimulation relation. In addition, it is straightforward
to show that $\cmbisim^{\mathcal{M}}$ is a bisimulation relation according
to Definition~\ref{def:altCMB}. So, ${\cmbisim^{\mathcal{M}}} \, \subseteq
\, {\altcmbisim^{\mathcal{M}}}$. Moreover, it also holds that
$\altcmbisim^{\mathcal{M}}$ is a bisimulation relation according to
Definition~\ref{def:CMB} and therefore ${\altcmbisim^{\mathcal{M}}} \,
\subseteq \, {\cmbisim^{\mathcal{M}}}$. Consequently the two equivalences
coincide.

\begin{figure}
\centerline{\resizebox{4cm}{!}{\includegraphics{figs/ExaUno}}}
\caption{Model $\mathcal{M}_1$.}\label{fig:ExaUno}
\end{figure}

\begin{example}
  \label{exa:ExaUno}
  In Figure~\ref{fig:ExaUno} a quasi-discrete closure model $\mathcal{M}_1
  = ((X_1,\closurename{R_1}),{\cal V}_{\!1})$ is shown where $X_1$
  contains 11 elements, each represented by a coloured square box,
  which we call a \emph{cell}. The relation~$R_1$ is the so-called
  \emph{orthogonal adjacency} relation~\cite{RLG13}, i.e.\ the
  reflexive and symmetric relation such that two cells are related iff
  they share an edge. Note, $X_1$ is not path-connected.

  The set $AP$ of atomic predicates is the set $\SET{\mathtt{red},
    \mathtt{blue}, \mathtt{green}, \mathtt{yellow}}$ and
  ${\cal V}_{\!1}$ associates each predicate (i.e.\ colour) to the set
  of cells of that specific colour\footnote{Spaces like $\mathcal{M}_1$ can
    be thought of as digital images where each cell represents a
    distinct pixel and the background of the image has been filtered
    out.}; in this example, each cell satisfies
  exactly one atomic proposition. The two red cells are
  $\cmbisim^{\mathcal{M}_1\!\!}-$bisimilar. In order to see this,
  consider the relation~$B_1$ which is the minimal reflexive and
  symmetric binary relation on~$X_1$ such that
  \begin{itemize}
  \item the two red points are related;
  \item the blue (green, yellow, respectively) point of the left-hand
    component is related to each blue (green, yellow, respectively)
    point of the right-hand component.
  \end{itemize}
It is easy to see that $B_1$ satisfies the conditions of
Definition~\ref{def:CMB}. For instance, the (forward and backward) closure of
the left-hand side red cell contains only the cell itself and the blue adjacent
one and, for each such cell, there is one in the right-hand side of the same
colour and related to the former by~$B_1$. Similarly, the closure of the
right-hand side red cell contains only the cell itself and the two blue adjacent
ones and, for each such cell, there is one in the left-hand side with the same
colour and related to the former by~$B_1$. Similar reasoning applies to all
other pairs of~$B_1$. Finally, the two red cell are related by bisimulation
relation~ $B_1$ and so they are bisimilar.
\end{example}

\begin{figure}
\centering
\subfloat[][]

\includegraphics[height=0.7cm]{figs/MatOneThree.pdf}
\label{fig:MatOneTree}
}\hspace{0.1in}
\centering
\subfloat[][]

\includegraphics[height=1.6cm]{figs/MatThreeThree.pdf}
\label{fig:MatThreeThree}
}\hspace{0.1in}
\centering
\subfloat[][]

\includegraphics[height=2cm]{figs/MatFourFour.pdf}
\label{fig:MatFourFour}
}\hspace{0.1in}
\subfloat[][]

\includegraphics[height=3cm]{figs/MatFiveFive.pdf}
\label{fig:MatFiveFive}
}
\caption{Models $\mathcal{M}_a$ (a), $\mathcal{M}_b$ (b),
$\mathcal{M}_c$ (c), and $\mathcal{M}_d$ (d).}\label{fig:ExaDue}
\end{figure}

\begin{example}
  \label{exa:ExaDue}
  For the sake of exposition, in this example, we will use matrix
  notation for referring to cells in Figure~\ref{fig:ExaDue}. Thus,
  $a_{2}$ and~$b_{22}$ refer to the red cells in
  Figure~\ref{fig:ExaDue}(a) and~\ref{fig:ExaDue}(b), respectively,
  whereas the four
  red cells in Figure~\ref{fig:ExaDue}(c) are referred to as $c_{22},
  c_{23}, c_{32}, c_{33}$ and so on. We consider four models $\mathcal{M}_j
  = ((X_j,\closurename{R_j}),{\cal V}_{\!j})$, for $j = a,b,c,d$.
  with
$X_a = \ZET{a_i}{1 \leqslant i \leqslant 3}$,
$X_b = \ZET{b_{ij}}{1 \leqslant i,j \leqslant 3}$,
$X_c = \ZET{c_{ij}}{1 \leqslant i,j \leqslant 4}$,
$X_d = \ZET{d_{ij}}{1 \leqslant i,j \leqslant 5}$.
Differently from Example~\ref{exa:ExaUno}, in each of the four models
$\mathcal{M}_j$, we assume an \emph{orthodiagonal adjacency
  relation}~$R_j$, namely, the reflexive and symmetric relation such
that two cells in $\mathcal{M}_j$ are related iff they share an edge \emph{or} a vertex~\cite{RLG13}. For instance, $\SET{(c_{11},c_{12}),
  (c_{11},c_{22})} \subseteq R_c$. This choice of the adjacency
relation simplifies the description of the example\footnote{In fact,
  as we will see, using the orthodiagonal relation makes the corner
  cells of $\mathcal{M}_j$, for $j\in \SET{b,c,d}$, bisimilar to all other
  blue cells of the model, which would not be the case, had we used the orthogonal relation.}.
The set~$AP$ of atomic propositions is the set $\SET{\mathtt{red},
  \mathtt{blue}}$, with
${\cal V}_{\!a} \,\mathtt{red} = \SET{a_2}$,
${\cal V}_{\!b} \,\mathtt{red} = \SET{b_{22}}$,
${\cal V}_{\!c} \,\mathtt{red} = \bigcup_{i,j=2,2}^{3,3}\SET{c_{ij}}$, and
${\cal V}_{\!d} \,\mathtt{red} = \bigcup_{i,j=2,2}^{4,4}\SET{d_{ij}}$, with
${\cal V}_{\!j} \,\mathtt{blue} = X_j \setminus ({\cal V}_{\!j} \,\mathtt{red})$ for $j \in \SET{a,b,c,d}$.
We use the shorthand
$\gamma \mkern1mu x = \calV^{\mbox{\,\scriptsize --1}}_j
\mkern1mu x$ for $x \in X_j$ and $j = a,b,c,d$.
Note, since $R_j$ is reflexive, $\gamma \mkern1mu x$ includes the
point~$x$ itself.
Moreover, the relations~$B_j$ are defined as $B_j = \ZET{(x,y) \in
  X_j^2}{\gamma \mkern1mu x = \gamma \mkern1mu y}$, for $j \in
\SET{a,b,c}$.

Clearly $a_1 \altcmbisim^{\mathcal{M}_a} a_3$ since $(a_1,a_3) \in B_a$,
which is a bisimulation. Take for instance $\mathcal{C}{R_a}{\!a_1} =
\SET{a_1,a_2}$ and note that $(a_1,a_3) \in B_a$ with $a_3 \in
\mathcal{C}{R_a}{\!a_3}$ and, similarly, $(a_2,a_2) \in B_a$ with $a_2
\in \mathcal{C}{R_a}{\!a_3}$. The reasoning for the other cells of~$X_a$
is similar.

It is also easy to see that for all $x,y \in X_b$ we have $x
\altcmbisim^{\mathcal{M}_b} y$ iff $\gamma \mkern1mu x = \gamma \mkern1mu
y$; for instance, for each element~$z_1$ of~$\mathcal{C}{R_b}{b_{11}} =
\SET{b_{11}, b_{12}, b_{21},b_{22}}$ there exists an element~$z_2$
of~$\mathcal{C}{R_b}{b_{23}} = \SET{b_{12},b_{13}, b_{22},
  b_{23},b_{32},b_{33}}$ such that $(z_1,z_2) \in B_b$, which is a
bisimulation containing also $(b_{11}, b_{23})$.

Let us now consider the model $\mathcal{M}_{ab}=((X_a \cup X_b,
\closurename{(R_a \cup R_b)}),{\cal V}_{\!ab})$ where ${\cal V}_{\!ab} \,p
= {{\cal V}_{\!a} \mkern1mu p} \mkern1mu \cup \mkern1mu {{\cal V}_{\!b}
  \mkern1mu p}$. We define the relation $B_{ab} \subseteq (X_a \cup
X_b)$ by $B_{ab} =\ZET{(x,y) \in X_a \cup X_b}{\gamma \mkern1mu x =
  \gamma \mkern1mu y}$. The reader is invited to prove that $a_2
\altcmbisim^{\mathcal{M}_{ab}} b_{22}$.
Similar reasoning shows that $B_c$ is a bisimulation for~$\mathcal{M}_c$
and that the quotient $X_{c/\!\!\altcmbisim^{\mathcal{M}_c}} = \SET{\ZET{x \in
    X_c}{\gamma \mkern1mu x = \mathtt{red}},\ZET{x \in X_c}{\gamma
    \mkern1mu x = \mathtt{blue}}}$ is a two-element set.
Also, for model $\mathcal{M}_{bc} = (((X_b \cup X_c), \closurename{R_b \cup
  R_c}), {\cal V}_{\!bc})$, with ${\cal V}_{\!bc} \mkern1mu p =
{\cal V}_{\!b} \mkern1mu p \cup {\cal V}_{\!c} \mkern1mu p$, we have
$c_{ij} \altcmbisim^{\mathcal{M}_{bc}} b_{22}$ for $i,j \in \SET{2,3}$, due
to the existence of the bisimulation $B_{bc} = \ZET{(x,y) \in X_b \cup
  X_c}{\gamma \mkern1mu x = \gamma \mkern1mu y}$.

In general, if we take as a model the union~$\mathcal{M}_{abc}$ of $\mathcal{M}_a$,
$\mathcal{M}_b$ and~$\mathcal{M}_c$, i.e.\ $\mathcal{M}_{abc}= (((X_a \cup X_b \cup X_c)),
\closurename{R_a \cup R_b \cup R_c}, {\cal V}_{\!abc})$, with ${\cal V}_{\!abc}
\mkern1mu p = {\cal V}_{\!a} \mkern1mu p \cup {\cal V}_{\!b} \mkern1mu p \cup
{\cal V}_{\!c} \, p$, we can easily see that all blue cells are bisimilar to one
another and all red cells are bisimilar to one another (and no blue cell is
bisimilar to any red one). In fact, as hinted above, there exists a minimal
model with just two cells, one red and one blue, that are adjacent (in this
case, the orthogonal and the orthodiagonal relations coincide); all red (blue,
respectively) cells of $\mathcal{M}_{abc}$ are equivalent to the red (blue,
respectively) cell of the minimal model.

Finally, let us consider cell~$d_{33}$ and, say, $d_{22}$ in
model~$\mathcal{M}_d$.  It is easy to see that $d_{22}
\not\altcmbisim^{\mathcal{M}_d}d_{33}$. In fact, $\mathcal{C}{R_d}{d_{33}} =
\ZET{x\in X_d}{\gamma \mkern1mu x = \mathtt{red}}$ and there is $y \in
\mathcal{C}{R_d}{d_{22}}$ such that $\gamma \,y = \mathtt{blue}$. Thus, any
bisimulation~$B$ should include $(y,z)$ with $z \in
\mathcal{C}{R_d}{d_{33}}$, because of the transfer condition 2 of
Definition~\ref{def:CMB} with respect to $(d_{22},d_{33})$, but this
is impossible because $(y,z) \in B$ would violate condition 3 of
Definition~\ref{def:CMB} because $\gamma \mkern1mu y =
\mathtt{blue} \neq \mathtt{red} = \gamma \mkern1mu z$.
\end{example}

\section{Quasi-discrete Closure Models Coalgebraically}
\label{sec:CMCoalgebraically}

Let the quasi-discrete closure model $\mathcal{M}=((X,\closurename{}), {\cal V})$ be
finitely closed and finitely backward closed (but not necessarily finite).  We
can represent~$\mathcal{M}$ as a pair $(X,\eta_{\mathcal{M}})$, with the function
$\eta_{\mathcal{M}} : X \to (\fpws{AP}) \times (\fpws{X}) \times (\fpws{X})$ such
that $\eta_{\mathcal{M}} x = (\invpeval{x}, \forwclosure{x}, \backclosure{x})$. In
the sequel we will write~$\eta$ instead of~$\eta_{\mathcal{M}}$, when this does not
cause confusion. Note that not all pairs~$(X,\eta)$ represent closure models,
but only those for which $(\eta \,x)_3 = \ZET{x' \in X}{x \in (\eta x')_2}$ and
$(\eta \,x)_2 =\ZET{x' \in X}{x \in (\eta x')_3}$.

\begin{example}
  Model~$\mathcal{M}_a$ of Figure~\ref{fig:ExaDue} corresponds to the pair
  $(\SET{a_1,a_2,a_3},\eta_a)$ with
  $\eta_a \, a_1 =(\SET{\mathtt{blue}}, \SET{a_1,a_2}, \SET{a_1,a_2})$,
  $\eta_a \, a_2 =(\SET{\mathtt{red}}, \SET{a_1,a_2,a_3},
  \SET{a_1,a_2,a_3})$, and
  $\eta_a \, a_3 =(\SET{\mathtt{blue}}, \SET{a_2,a_3},
  \SET{a_2,a_3})$. The other models of the figure can be represented
  similarly.
\end{example}

\noindent
The following is a reformulation of bisimilarity in terms of the
function~$\eta_{\mathcal{M}}$.

\begin{definition}\label{def:ETB}
  An equivalence relation $B \subseteq X \times X$ is an
  $\eta$-bisimulation if $(x_1,x_2) \in B$ implies that the following
  holds:
  \begin{enumerate}
  \item $(\eta \, x_1)_1 = (\eta \, x_2)_1$, and
  \item for all $C \in X/B$ it holds that
    \begin{enumerate}
    \item $(\eta \, x_1)_2 \cap C \not=\emptyset \mbox{ iff } (\eta \,
      x_2)_2 \cap C \neq \emptyset$, and
    \item $(\eta \, x_1)_3 \cap C \neq \emptyset \mbox{ iff } (\eta \,
      x_2)_3 \cap C \neq \emptyset.$
    \end{enumerate}
  \end{enumerate}
  We say that $x_1$ and~$x_2$ are $\eta$-\emph{bisimilar}, notation $x_1
  \ebisim x_2$, if there exists an $\eta$-bisimulation relation~$B$ such
  that $(x_1,x_2) \in B$.
\end{definition}

\begin{example}
  With reference to model~$\mathcal{M}_a$ of Figure~\ref{fig:ExaDue} and
  $(\SET{a_1,a_2,a_3},\eta_a)$ above, it is easy to see that $a_1$
  and~$a_3$ are $\eta_a$-{bisimilar}.
\end{example}

\noindent
The following lemma follows directly from Definition~\ref{def:altCMB}
and Definition~\ref{def:ETB}.

\begin{lemma}
  \label{lemma:ebisISaltcmbisim}
  $\ebisim$ coincides with $\altcmbisim$.
\end{lemma}

\begin{definition}
  \label{def:simplerfunctor}
  The functor ${\cal T}: \textbf{Set} \to \textbf{Set}$ assigns to a set~$X$ the product
  set $\fpws{AP} \times \fpws{X} \times \fpws{X}$ and to a mapping $f
  : X \to Y$ the mapping ${\cal T} \mkern1mu f : (\fpws{AP} \to \fpws{X}
  \to \fpws{X}) \to (\fpws{AP} \times \fpws{Y} \times \fpws{Y})$
  where, for all $v \in \fpws{AP}$ and $z,z' \in \fpws{X}$, $({\cal T} f)
  \mkern1mu v \mkern1mu z \mkern1mu z' = (v,(f z),(f z'))$.
\end{definition}

\noindent
Clearly, the model~$\mathcal{M}$, represented as $(X,\eta)$, can be interpreted
as a coalgebra  of functor~${\cal T}$.

\begin{lemma}
  \label{lemma:calTfinalco}
  The functor ${\cal T}$ has a final coalgebra.
\end{lemma}

\begin{proof}
  Constants, finite products, and the finite powerset are
  $\omega$-accessible functors. The class of $\kappa$-accessible
  functors for any~$\kappa$ is closed with respect to composition, and
  $\kappa$-accessible functors have final coalgebras. $ $\hfill $\bullet$
\end{proof}

\noindent
We recall that two elements~$x_1, x_2$ of an ${\cal T}$-coalgebra~${\cal X}$
are behavioural equivalent if $\fmorph{{\cal T}}{{\cal X}}{x_1} =
\fmorph{{\cal T}}{{\cal X}}{x_2}$, denoted $x_1 \beq{{\cal T}}{{\cal X}} x_2$,
where $\fmorph{{\cal T}}{{\cal X}}{\cdot}$ is the unique morphism
from~${\cal X}$ to the final coalgebra of functor~${\cal T}$.

The following theorem shows that behavioural equivalence and $\eta$-bisimilarity coincide. The proof follows the same pattern as that of Theorem 4.3 in \cite{LMV15a}.

\begin{theorem}
  \label{theo:etabisbeh}
  \mbox{%
  Behavioural equivalence and $\eta$-bisimilarity coincide,
  i.e.\ $\beq{{\cal T}}{} \, = \, \ebisim$.}
\end{theorem}

\begin{proof}

  Let $x_1, x_2 \in X$.  We
  first prove that ${x_1 \ebisim x_2}$ implies $x_1 \beq{{\cal T}}{}
  x_2$.  So, assume ${x_1 \ebisim x_2}$.  Let $B \subseteq X \times X$
  be an $\eta$-bisimulation with $(x_1,x_2)\in B$ and recall that
  $(X,\eta)$ is a ${\cal T}$-coalgebra. We turn the collection of
  equivalence classes~$X/B$ into a ${\cal T}$-coalgebra
  $\mathcal{M}/B = (X/B,\varrho_B)$ where, for $s \in X$
  \begin{displaymath}
    \varrho_B \, [s]_B  = (
    (\eta \mkern1mu s)_1,
    \ZET{C\in X/B}{(\eta \mkern1mu s)_2 \cap C \neq \emptyset},
    \ZET{C\in X/B}{(\eta \mkern1mu s)_3 \cap C \neq \emptyset})
  \end{displaymath}
  This is well-defined since $B$ is an $\eta$-bisimulation: if
  $(s,s')\in B$ then
  we have
  \begin{displaymath}
    \def1.0{1.3}
    \begin{array}{rcll}
      \varrho_B \mkern1mu [s]_B
      & = &
      ((\eta \mkern1mu s)_1,
      \ZET{C\in X/B}{(\eta \mkern1mu s)_2 \cap C \neq \emptyset},
      \ZET{C\in X/B}{(\eta \mkern1mu s)_3 \cap C \neq \emptyset})
      \\ & & \qquad \text{(def.\ of $\varrho_B$)}
      \\
      & = &
      ((\eta \mkern1mu s')_1,
      \ZET{C\in X/B}{(\eta \mkern1mu s')_2 \cap C \neq \emptyset},
      \ZET{C\in X/B}{(\eta \mkern1mu  s')_3 \cap C \neq \emptyset})
      \\ & & \qquad \text{($(s,s')\in B$; $B$ is an $\eta$-bisimulation)}
      \\
      & = & \varrho_B \, [s']_B
      \qquad \text{(def.\ of $\varrho_B$).}
    \end{array}
    \def1.0{1.0}
  \end{displaymath}
  The canonical mapping $\varepsilon_B : X \to X/B$ is a
  ${\cal T}$-homomorphism, i.e.\ $({\cal T} \,\varepsilon_B) \mathop{\raisebox{0.5pt}{\scriptsize $\circ$}} \eta =
  \varrho_B \mathop{\raisebox{0.5pt}{\scriptsize $\circ$}} \varepsilon_B$ as can be verified as follows.
For  $s \in X$, we have
\begin{displaymath}
    \def1.0{1.3}
    \begin{array}{rcll}
      ({\cal T}\, \varepsilon_B)(\eta \mkern1mu s)
      & = & ((
      \eta \mkern1mu s)_1,
      \varepsilon_B \mkern1mu (\eta \mkern1mu s)_2,
      \varepsilon_B \mkern1mu (\eta \mkern1mu s)_3 )
      & \text{(def.\ of ${\cal T}$)}
      \\ & = &
      ((\eta \mkern1mu s)_1,
      \ZET{[t]_B}{t \in (\eta \mkern1mu s)_2},
      \ZET{[t]_B}{t \in (\eta \mkern1mu s)_3})
      \qquad \mbox{} &
      \text{(def.\ of $\varepsilon_B$)}
      \\ & = &
      \multicolumn{2}{l}{%
        ((\eta \mkern1mu s)_1,
        \ZET{C\in X/B }{(\eta \mkern1mu s)_2 \cap C \neq \emptyset},
        \ZET{C\in X/B }{(\eta \mkern1mu s)_3 \cap C \neq \emptyset})
      }

      \\
      & = & \varrho_B [s]_B & \text{(def.\ of $\varrho_B$)}
      \\
      & = & \varrho_B (\varepsilon_B\, s) & \text{(def.\ of $\varepsilon_B$).}
    \end{array}
    \def1.0{1.0}
  \end{displaymath}
  Thus, $({\cal T} \,\varepsilon_B) \mathop{\raisebox{0.5pt}{\scriptsize $\circ$}} \eta = \varrho_B \mathop{\raisebox{0.5pt}{\scriptsize $\circ$}}
  \varepsilon_B$, i.e.\ $\varepsilon_B$ is a ${\cal T}$-homomorphism.
  Therefore, by uniqueness of a final morphism, we have
  $\fmorph{{\cal T}}{\mathcal{M}}{\cdot} = \fmorph{{\cal T}}{{\mathcal{M}_B}}{\cdot}
  \mathop{\raisebox{0.5pt}{\scriptsize $\circ$}} \, \varepsilon_B$.  In particular, with respect
  to~$\mathcal{M}$, this implies $\fmorph{{\cal T}}{\mathcal{M}}{x_1} =
  \fmorph{{\cal T}}{\mathcal{M}}{x_2}$ since $(x_1,x_2)\in B$ and so
  $(\varepsilon_B \, x_1) = (\varepsilon_B \, x_2)$.  Thus, $x_1
  \beq{{\cal T}}{} x_2$.

  For the reverse---i.e.\ ${x_1 \beq{{\cal T}}{} x_2 }$ implies ${x_1
    \ebisim x_2}$---assume $x_1 \beq{{\cal T}}{} x_2$, i.e.
  $\fmorph{{\cal T}}{\mathcal{M}}{x_1} = \fmorph{{\cal T}}{\mathcal{M}}{x_2}$, for
  $x_1,x_2 \in X$. Define the relation $R \subseteq X \times X$
  such that $(x_1,x_2) \in R$ iff $\fmorph{{\cal T}}{\mathcal{M}}{x_1} =
  \fmorph{{\cal T}}{\mathcal{M}}{x_2}$. We first show that $R$ is an
  $\eta$-bisimulation. Suppose $(s',s'') \in R$ and recall that
  $\fmorph{{\cal T}}{\mathcal{M}}{\cdot} : (X,\eta) \to (\Omega,\omega)$ is a
  ${\cal T}$-homomorphism. For what concerns the first condition of
  Definition~\ref{def:ETB} we have
  \begin{displaymath}
    \def1.0{1.0}
    \begin{array}{rcll}
      (\eta \mkern1mu s')_1 & = &
      (({\cal T} \, \fmorph{{\cal T}}{}{\cdot})(\eta \,s'))_1
      & \text{(def.\ of ${\cal T}$)}
      \\ & = &
      ((({\cal T} \,\fmorph{{\cal T}}{}{\cdot}) \mathop{\raisebox{0.5pt}{\scriptsize $\circ$}} \eta) \, s')_1
      \\ & = &
      (( \omega \mathop{\raisebox{0.5pt}{\scriptsize $\circ$}} \fmorph{{\cal T}}{}{\cdot})s')_1
      & \text{($\fmorph{{\cal T}}{}{\cdot} : (X,\eta) \to
        (\Omega,\omega)$ is homomorphism.)}
      \\ & = &
      (\omega \, \fmorph{{\cal T}}{}{s'})_1

      \\ & = &
      (\omega \, \fmorph{{\cal T}}{}{s''})_1
      & \text{($\fmorph{{\cal T}}{}{s'} =
        \fmorph{{\cal T}}{}{s''}$ since $(s',s'') \in R$)}
      \\ & = &
      ((\omega \mathop{\raisebox{0.5pt}{\scriptsize $\circ$}} \fmorph{{\cal T}}{}{\cdot})s'')_1

      \\ & = &
      ((({\cal T} \,\fmorph{{\cal T}}{}{\cdot}) \mathop{\raisebox{0.5pt}{\scriptsize $\circ$}} \eta) \, s'')_1
      & \text{($({\cal T} \,\fmorph{{\cal T}}{}{\cdot}) \mathop{\raisebox{0.5pt}{\scriptsize $\circ$}} \eta =
        \omega \mathop{\raisebox{0.5pt}{\scriptsize $\circ$}} \fmorph{{\cal T}}{}{\cdot}$)}
      \\ & = &
      (({\cal T} \, \fmorph{{\cal T}}{}{\cdot})(\eta \,s''))_1

      \\ & = &
      (\eta \mkern1mu s'')_1
      & \text{(def.\ of ${\cal T}$).}
    \end{array}
    \def1.0{1.0}
  \end{displaymath}
  For what concerns the second condition of Definition~\ref{def:ETB}
  we have, for $h \in \SET{2,3}$ and all $C \in X/R$, that
\begin{displaymath}
  \def1.0{1.3}
  \begin{array}{rcll}
    \multicolumn{4}{l}{(\eta \mkern1mu s')_h \cap C \neq \emptyset}
    \\
    \mbox{\qquad} & \Leftrightarrow &
    (\eta \, s')_h \cap \fmorph{{\cal T}}{-1}{w} \neq \emptyset \mbox{\qquad} &
    \\ & &
    \multicolumn{2}{l}{\qquad \text{(def.\ of ${\fmorph{{\cal T}}{-1}{\cdot}}$;
      def.\ of~$R$; $w = \fmorph{{\cal T}}{}{t}$ for all $t \in C$)}}
    \\ & \Leftrightarrow &
    w \in (\omega {\fmorph{{\cal T}}{}{s'}})_h

    & \text{(by Lemma~\ref{lemma:aux} below)}
    \\ & \Leftrightarrow &
    w \in (\omega {\fmorph{{\cal T}}{}{s''}})_h

    & \text{($ \fmorph{{\cal T}}{}{s'} =
      \fmorph{{\cal T}}{}{s''}$ since $(s',s'') \in R$)}
    \\ & \Leftrightarrow &
    (\eta \mkern1mu s'')_h \cap \fmorph{{\cal T}}{-1}{w} \neq \emptyset

    & \text{(by Lemma~\ref{lemma:aux} below)}
    \\ & \Leftrightarrow &
    (\eta \mkern1mu s'')_h \cap C \neq \emptyset
    \\ & &
    \multicolumn{2}{l}{\qquad \text{(def.\ of ${\fmorph{{\cal T}}{-1}{\cdot}}$;
        def.\ of~$R$; $w = \fmorph{{\cal T}}{}{t}$ for all $t \in C$)}.}
  \end{array}
  \def1.0{1.0}
\end{displaymath}
Since both conditions of Definition~\ref{def:ETB} are fulfilled,
$R$ is an $\eta$-bisimulation relation and hence, since $(x_1,x_2)\in R$,
we get ${x_1 \ebisim x_2}$. This completes the proof. $ $\hfill $\bullet$
\end{proof}

\noindent
In the proof of Theorem~\ref{theo:etabisbeh} we have made use of the
following result.

\begin{lemma}
  \label{lemma:aux}
  For $h \in \SET{2,3}$, all $s \in X, w \in \Omega$ we have that $w
  \in (\omega \, {\fmorph{{\cal T}}{}{s}})_h$ if and only if $(\eta \,
  s)_h \cap \fmorph{{\cal T}}{-1}{w} \not=\emptyset$.
\end{lemma}

\begin{proof}
See Appendix \ref{appendix}.
\end{proof}

\noindent
From Theorem~\ref{theo:etabisbeh} and
Lemma~\ref{lemma:ebisISaltcmbisim} we get complete correspondence of
behavioural equivalence and bisimilarity for quasi-discrete closure
models .

\begin{corollary}
  \label{coro:bisbeh}
  Given a quasi-discrete closure model $\mathcal{M} = ((X,\closurename{R}),
  \calV)$ based on~$R$, for all $x_1, x_2 \in X$ it holds that
  $x_1 \altcmbisim^{\mathcal{M}} x_2$ iff $x_1 \beq{{\cal T}}{\mathcal{M}} x_2$.
\end{corollary}

\begin{example}
  \label{exa:ExaTre}
  With reference to Example~\ref{exa:ExaDue}, we see that the minimal
  coalgebra for the models $\mathcal{M}_a, \mathcal{M}_b$ and~$\mathcal{M}_c$ is
  represented by $(\SET{\tau_1,\tau_2},\mu)$ where $\mu \mkern1mu
  \tau_1 = (\mathtt{blue}, \SET{\tau_1,\tau_2}, \SET{\tau_1,\tau_2})$,
  and $\mu \mkern1mu \tau_2 = (\mathtt{red}, \SET{\tau_1,\tau_2},
  \SET{\tau_1,\tau_2})$. The quotient morphisms are the obvious ones;
  for instance, letting model~$\mathcal{M}_c$ be represented by the
  coalgebra\footnote{For the sake of readability, here we use the same
    names~$c_{ij}$ for the elements of the carrier of the relevant
    coalgebra as those we used for defining the model $\mathcal{M}_c$,
    although everything is to be intended up to isomorphisms.}

  $(X_c, \eta_c)$,
  $h_c :  (X_c, \eta_c) \to ((\tau_1,\tau_2),\mu)$ maps $c_{22},
  c_{23}, c_{32}$, and $c_{33}$ to~$\tau_2$, and all other elements
  to~$\tau_1$.
  The minimal coalgebra for~$\mathcal{M}_d$ is
  $(\SET{\tau_3,\tau_4,\tau_5},\nu)$, where
  $\nu \mkern1mu \tau_3 = (\mathtt{red}, \SET{\tau_3,\tau_4},
  \SET{\tau_3,\tau_4})$,
  $\nu \mkern1mu \tau_4 = (\mathtt{red}, \SET{\tau_3,\tau_4,\tau_5},
  \SET{\tau_3,\tau_4,\tau_5})$, and
  $\nu \mkern1mu \tau_5 = (\mathtt{blue},\SET{\tau_4,\tau_5},
  \SET{\tau_4,\tau_5})$. The minimal models obtained using \texttt{MiniLogicA} are reported in Figure~\ref{fig:minimized-examples}.

  Note that $h_d:(X_d, \eta_d) \to ((\tau_3,\tau_4,\tau_5),\nu)$ maps
  $d_{33}$ to~$\tau_3$, the elements of $\lbrace \, d_{ij} \mid 2
  \leqslant i,j \leqslant 4 \, \rbrace \setminus \SET{d_{33}}$
  to~$\tau_4$, and all the other elements to~$\tau_5$.
  Finally, consider the union~$\mathcal{M}_{abcd}$ of~model $\mathcal{M}_{abc}$
  and model~$\mathcal{M}_d$.  In this case, the minimal coalgebra is
  (isomorphic to) $(\SET{\tau_1, \tau_2, \tau_3, \tau_4, \tau_5},\mu+\nu)$
  where $(\mu+\nu) \mkern1mu \tau = \mu \mkern1mu \tau$ if $\tau =
  \tau_1, \tau_2$ and $(\mu+\nu) \mkern1mu \tau = \nu \mkern1mu \tau$
  if~$\tau = \tau_3, \tau_4, \tau_5$.

\end{example}

\begin{figure}
  \centering
  \fbox{
    \subfloat[][]
    { \includegraphics[trim=0pt 15pt 15pt 20pt,clip,height=50pt]{examples/redBlueF3c.pdf}
      \label{fig:minimized-examples-a}
    }
    \subfloat[][]
    { \includegraphics[trim=0 15pt 15pt 20pt,clip,height=50pt]{examples/redBlueF3d.pdf}
      \label{fig:minimized-examples-b}
    }
  }
  \caption{\label{fig:minimized-examples}Minimal models obtained by running {\tt MiniLogicA} on the images of Figure~\ref{fig:ExaDue}. Models $\mathcal{M}_a, \mathcal{M}_b$ and~$\mathcal{M}_c$ are all equivalent to the model on the left, whereas $\mathcal{M}_d$ is equivalent to the model on the right.}
\end{figure}

\section{Concluding Remarks}
\label{sec:discussion}

In the context of spatial logics and model checking for closure spaces, we have
developed a coalgebraic definition of spatial bisimilarity, a minimization
algorithm, and a free and open source minimisation tool. Bisimilarity
characterises logical equivalence of a finitary logic with two spatial
reachability operators. Furthermore, we have generalised the definition of
topo-bismilarity from topological spaces to closure spaces, proving that the
more general definition still behaves as topo-bisimilarity, in that it
characterises equivalence of infinitary modal logic. Finally, we have provided a
coalgebraic characterisation in the more general setting. Indeed, one of the
primary motivations for our work is the expectation that the tool can be
refined, and the implementation can be integrated with the state-of-the-art
spatial model checker {\ttfamily{VoxLogicA}}\xspace{}, to improve its efficiency, especially when
spatial structures are procedurally generated (e.g.\ by a graph rewriting
procedure or by a process calculus). However, we can identify a number of
theoretical questions, that have the potential to lead to interesting
developments of the research line of spatial model checking.

One major issue that has not yet been addressed is a treatment of logics with
reachability, in the more general setting of Section~\ref{sec:generalization}.
One major difficulty here is that the notion of a \emph{path} has not been
defined in the literature for closure spaces; in \cite{CLLM16} it was emphasized
(see Section 2.4) that the well-known topological definition does not generalise
in the expected way, as it is not compatible with another fundamental notion,
that of paths in a finite graph. Identifying a general notion of path would
allow us to interpret reachability operators in general closure spaces. Such
development is not a merely theoretical exercise. We expect that there are
classes of non-quasi-discrete spaces, that may be finitely represented. For
instance, variants of the polyhedra-based approach of~\cite{BMMP18} may be
relevant for dealing with Euclidean spaces, and in practical terms, for
reasoning about 3D~\emph{meshes} that are of common use in Computer Graphics.
Also spaces that are the union of different components, based either on
polyhedra or on graphs, can give rise to a \emph{hybrid spatial model checking}
approach in the same vein as the celebrated results on model checking of hybrid
systems in the temporal case (see~\cite{Doyen2018}).

Future work should also be devoted to clarifying the generality of the notion of
a closure coalgebra, and to provide a more thorough comparison of closure
coalgebras and neighbourhood frames. In this context, it is also relevant to
investigate the link between closure coalgebras and the treatment of monotone
logics of~\cite{HK04}, given that monotonicity of closure is used in both
directions for the proof of
Theorem~\ref{thm:closureCoalgebraLogicalEquivalence}.

\section{Extension to Generic Closure Spaces}
\label{sec:generalization}

In this section we provide first a set-theoretic and next a
coalgebraic notion of bisimilarity for closure models that aren't
necessarily quasi-discrete, and we prove that both coincide with
logical equivalence as induced by an infinitary modal logic, here
called IML\xspace, which, compared to $SLCS\xspace$, does not include
reachability operators. Instead, $\mathcal{N} {\bf F}$~is the basic
operator---endowed with the classical closure semantics. Also,
infinitary conjunction is allowed.

\begin{equation}
  \label{def:infsyntax}
  {\bf F}  ::=  p  \,\mid\, \neg \, {\bf F} \,\mid\, \textstyle{\linfand{i \in I}}
  \: {\bf F}_i \,\mid\, \mathcal{N} {\bf F}
\end{equation}
where $p \in AP$, and $I$~is a set.

For a closure model $((X,\closurename{}),{\cal V})$ we have, as expected,
$\mathcal{M}, x \models p$ $\Leftrightarrow$ $x \in {\cal V} p$, $\mathcal{M}, x
\models \mathcal{N} {\bf F}$ $\Leftrightarrow$ $x \in \mathcal{C}{} {\ZET{y
    \!}{\! \mathcal{M}, y \models {\bf F}}}$, $\mathcal{M},x \models \lnot {\bf F}$
  $\Leftrightarrow$ $\mathcal{M},x \not \models {\bf F}$, and finally
  $\mathcal{M},x \models \linfand{i \in I} {\bf F}_i$ $\Leftrightarrow$ $\mathcal{M},x
  \models {\bf F}_i$ for all~$i \in I$.

\begin{definition}
  \label{def:LEQ}
  The equivalence relation $\inflogeq^{\mathcal{M}} \subseteq X \times X$
  is defined by $x_1 \inflogeq^{\mathcal{M}} x_2$ iff for all
  IML\xspace\ formulas ${\bf F}$ we have that $\mathcal{M}, x_1 \models {\bf F}
  \Leftrightarrow \mathcal{M}, x_2 \models {\bf F}$.
\end{definition}

\noindent
In the sequel, $\inflogeq^{\mathcal{M}}$ will be often abbreviated
by~$\inflogeq$.  The following definition extends the notion of
bisimulation for topological spaces (see~\cite{BeB07}, for example) to
general closure models.

\begin{definition}
  \label{def:GCMB}
  Given a closure model $\mathcal{M} = ((X,\closurename{}), \calV)$, a
  non-empty equivalence relation $B \subseteq X \times X$ is called a
  \emph{bisimulation relation} if, for all $x_1,x_2 \in X$ such that
  $(x_1,x_2) \in B$, the next two conditions are satisfied.
  \begin{enumerate}
  \item $\invpeval{x_1} = \invpeval{x_2}$.
  \item For all $X_1 \subseteq X$ such that $x_1 \in
    \interior{}{X_1}$, there is $X_2 \subseteq X$ such that $x_2 \in
    \interior{}{X_2}$ and, reversely, for all $x_2' \in X_2$ there
    exists $x_1' \in X_1$ such that $(x_1',x_2') \in B$.
  \end{enumerate}
  We say that $x_1$ and~$x_2$ are {\em bisimilar}, notation $x_1
  \gcmbisim x_2$, if there exists a bisimulation relation~$B$ for~$X$
  such that $(x_1,x_2) \in B$.
\end{definition}

\begin{remark}
  The definition of~\cite{BeB07} (given for topological models)
  differs from the definition above in that the sets~$X_{i}$ are
  required to be \emph{open} neighbourhoods. In topology, a subset~$S$
  is an open neighbourhood of a point~$x$ whenever there is an open
  set~$O$ with $x \in O \subseteq S$, or, equivalently, $x \in
  \interior{}{S}$. Therefore, in a topological space,
  Definition~\ref{def:GCMB} coincides with the one
  of~\cite{BeB07}. However, in general closure models, this is
  different. For instance consider a graph with three nodes $a,b,c$,
  and relation $R = \{(a,b),(b,c)\}$. Let $S = \{b,c\}$. We have
  $\interior{}{S} = S \setminus \mathcal{C}{}{\overline S} = S \setminus
  \mathcal{C}{}{\{a\}} = S \setminus \{a,b\} = \{c\} \neq S$, therefore
  $S$~is not open (see also~\cite{CLLM16}, Remark 2.19).  Similarly,
  $\{c\}$~is not open as $\interior{}{\{c\}} = \emptyset$. Thus
  $S$~does not include an open set containing~$c$. However, $c \in
  \interior{}{S}$.
\end{remark}

\noindent
Below, we show that logical equivalence in~IML\xspace coincides with
bisimilarity from Definition~\ref{def:GCMB}.
The following two lemmas are required.

\begin{lemma}
  \label{lem:closure-cap-interior}
  For all $X_1,X_2 \subseteq X$, if $(\mathcal{C}{}{X_1}) \cap
  (\interior{}{X_2}) \neq \emptyset$ then $X_1 \cap X_2 \neq
  \emptyset$.
\end{lemma}

\begin{proof}
  We prove that $X_1 \cap X_2 = \emptyset$ implies $(\mathcal{C}{}{X_1})
  \cap (\interior{}{X_2}) = \emptyset$. Suppose $X_1 \cap X_2 =
  \emptyset$. Then $X_1 \subseteq \overline X_2$, thus
  $\mathcal{C}{}{X_1} \subseteq \mathcal{C}{}{\overline X_2}$. Since
  $\interior{}{X_2} = \overline{\mathcal{C}{}{(\overline X_2)}}$, it
  follows that $(\interior{}{X_2}) \cap (\mathcal{C}{}{X_1}) =
  \emptyset$. \qed
\end{proof}

\begin{lemma}
  \label{lem:interior-implies-closure}
  For all $S \subseteq X$ and $y \in X$, if for all $C \subseteq X$ it
  holds that $y \in \interior{}{C}$ implies $C \cap S \neq \emptyset$,
  then $y \in \mathcal{C}{}{S}$.

\end{lemma}

\begin{proof}
  By contradiction.  Suppose $y \notin \mathcal{C}{}{S}$ under the
  hypothesis of the lemma. Then $y \in \overline{\mathcal{C}{}{S}}$,
  i.e.\ $y \in \overline{\overline{\interior{}{(\overline{S})}}} =
  \interior{}{(\overline{S})}$. But then, by the hypothesis, taking $C
  = \overline{S}$ since $\overline{S} \subseteq X$, we would have that
  $\overline{S} \cap S \neq \emptyset$. \qed
\end{proof}

\noindent
With the two lemmas in place, we are in a position to prove the next
results.

\begin{theorem}
  Given a closure model $\mathcal{M} = ((X,\closurename{}), \calV)$, any
  bisimulation~$B$ according to Definition~\ref{def:GCMB} is included
  in~$\inflogeq^\mathcal{M}$.
\end{theorem}

\begin{proof}
  By induction on the structure of~${\bf F}$.

  ${\bf F} = \mathcal{N} {\bf F}'$. Suppose $B$ is a bisimulation, $(x,y) \in
  B$ and, without loss of generality, $\mathcal{M},x \not \models {\bf F}$
  and $\mathcal{M}, y \models {\bf F}$. Let $F \subseteq X$ be the set of
  points satisfying~${\bf F}'$. We have $y \in \mathcal{C}{}{F}$ and $x \in
  \overline{\mathcal{C}{}{F}} =
  \overline{\overline{\interior{}{(\overline F)}}} =
  \interior{}{(\overline F)}$. Let $X_1 = \overline F$. By $x \in
  \interior{}{X_1}$, let $X_2$ be chosen according to
  Definition~\ref{def:GCMB}, with $y \in \interior{}{X_2}$. By
  Lemma~\ref{lem:closure-cap-interior} we have $F \cap X_2 \neq
  \emptyset$, since $y \in (\mathcal{C}{}{F}) \cap
  (\interior{}{X_2})$. Let $y' \in F \cap X_2$. We have $\mathcal{M}, y'
  \models \Phi'$, since $y' \in F$. Since $B$ is a bisimulation
  according to Definition~\ref{def:GCMB}, there is $x' \in X_1$ with
  $(x',y')\in B$. By the induction hypothesis $\mathcal{M}, x' \models
  {\bf F}'$, thus $x' \in F$, which contradicts $x' \in X_1 = \overline
  F$.
\end{proof}

\begin{theorem}\label{theo:inflogeq:bisim}
  Given model $\mathcal{M}=((X,\closurename{}), \calV)$,
  $\inflogeq^\mathcal{M}$ is a bisimulation according to
  Definition~\ref{def:GCMB}.
\end{theorem}

\begin{proof}
  Suppose $x \inflogeq y$. Let $X_1$ be such that $x \in
  \interior{}{X_1}$. Suppose there is no~$X_2$ respecting the
  conditions of Definition~\ref{def:GCMB}. Then, either there is no $C
  \subseteq X$ such that $y \in \interior{}{C}$ or for each such~$C$
  there is $y_{\mkern1mu C} \in C$ such that $x'\inflogeq y_{\mkern1mu
    C}$ for \emph{no} $x' \in X_1$. In the first case we would have
  that, for all $C \subseteq X$, $y \notin
  \overline{\mathcal{C}{}{(\overline{C})}}$, i.e.\ $y \in
  \mathcal{C}{}{(\overline{C})}$. This would imply in turn that $y \in
  \mathcal{C}{}{(\overline{X})} = \emptyset$, which is absurd. In the
  second case, let $S$ be the set of all the~$y_{\mkern1mu C}$ as
  above. We have $y \in \mathcal{C}{}{S}$ by
  Lemma~\ref{lem:interior-implies-closure}. For each $a \in X_1$ and
  $s \in S$, $a$ and~$s$ are not logically equivalent: let
  ${\bf F}_{(a,s)}$ be a formula such that $\mathcal{M},a \not \models
  {\bf F}_{(a,s)}$ and $\mathcal{M},s \models {\bf F}_{(a,s)}$. Let ${\bf F} =
  \bigwedge_{\, s} \lnot \bigwedge_{\, a} {\bf F}_{(a,s)}$. We have that
  $\mathcal{M}, x' \models {\bf F}$ for all $x' \in X_1 $ and $\mathcal{M}, y'
  \not \models {\bf F}$ for all $y' \in S$. To see the latter, observe
  that $\lnot \Phi = \bigvee_{\! s} \bigwedge_{\, a}
  \Phi_{(a,s)}$. For each $a$, each $y' \in S$ satisfies at least
  $\bigwedge_{\, a} {\bf F}_{(a,y')}$. Thus, we have a formula~$\Phi$ with
  $X_1 \subseteq F = \{ \, z \in X \mid z \models \Phi \, \}$ and $S
  \subseteq \overline F$. By $x \in \interior{}{X_1}$ and monotonicity
  of interior, we have $x \in \interior{}{F}$, thus $\mathcal{M}, x \models
  \lnot \mathcal{N} (\lnot {\bf F})$. On the other hand, by $y \in
  \mathcal{C}{}{S}$ and monotonicity of closure, we have $y \in
  \mathcal{C}{}{(\overline F)}$, thus $\mathcal{M}, y \models \mathcal{N} (\lnot
  {\bf F})$, contradicting the hypothesis $x \inflogeq y$.  \qed
\end{proof}

\noindent
The characterisation given by Definition~\ref{def:GCMB} has the merit of
extending the existing topological definition to closure spaces. However, in the
setting of this paper it is worthwhile to investigate also a coalgebraic
definition, which we do in the remainder of this section.  Since our main objective is to characterise logical equivalence,
we will not define \emph{frames}, but just \emph{models}, which we will call
\emph{closure coalgebras}.

\begin{definition}\label{def:closureCoalgebra}
  A \emph{closure coalgebra} is a coalgebra for the \emph{closure
    functor} $\textbf{C} X = \pws{(AP)} \times \pws{(\pws{X})}$,
  where $\pws{-}$ is the covariant powerset functor. The action of the functor on arrows maps $f : X \to Y$ to
  $\textbf{C} f: (\pws{(AP)} \times \pws{(\pws{X})}) \to (\pws{(AP)} \times \pws{(\pws{Y})})$ such that
  $\textbf{C} f (v, S)=(v,\{(\pws f) A | A \in S\})$.

\end{definition}

\noindent
We note in passing
that a general coalgebraic treatment of modal logics -- even the non-normal ones
-- can be done starting from \emph{neighbourhood frames}~\cite{HKP09}, employing
coalgebras for the functor $2^{2^{-}}$ (where $2^{-}$ is the contravariant power
set functor). Our definition is similar, but in contrast we employ the
\emph{covariant} powerset functor~$\pws{}$, which we find particularly
profitable, as the obtained theory is akin\footnote{In order to make Definition~\ref{def:closureCoalgebra} a proper generalisation of Definition~\ref{def:simplerfunctor}, one needs to identify the correct notion of \emph{path} for closure coalgebras (more on this in Section~\ref{sec:discussion}).} to the developments of Section~\ref{sec:CMCoalgebraically}.
The remainder of this section is aimed at determining a correspondence
between closure models, closure coalgebras, and their quotients.

\begin{definition}
  \label{def:closureCoalgebraOfAModel}
  Given a closure model $((X,\closurename{}),\calV)$, define the
  coalgebra $\eta : X \to \textbf{C} X$ by $\eta(x) =
  ( \mkern1mu \pevalname^{\mbox{-} \mkern-2mu \mbox{\scriptsize 1}}{}x,\{ \, A \subseteq X \mid x \in
  \closurename{} A \mkern1mu \})$.
\end{definition}

\noindent It is straightforward to check that if $f : {\cal X} \to {\cal Y}$ is a
$\textbf{C}$-coalgebra homomorphism, and both ${\cal X}$ and ${\cal Y}$ have been
obtained from closure models using
Definition~\ref{def:closureCoalgebraOfAModel}, then $f$ is a continuous function
in the sense of Definition~\ref{def:ContinuousFunction}. From now on, we shall
not rely on the existence of a final coalgebra, as this is not the case for the
(unbounded) powerset functor. However, we can employ maximal quotients instead,
for the purpose of this paper. Therefore, we will redefine behavioural
equivalence from Section~\ref{sec:Preliminaries}.

\begin{definition}
  \label{def:behaviouralEquivalenceNew}
  Given a set functor~${\cal F}$ and a ${\cal F}$-coalgebra ${\cal X} =
  (X,\alpha)$ with $\alpha : X \to {\cal F} X$, the relation
  $\beq{{\cal F}}{{\cal X}}$, defined by
  \smallskip \\
  \centerline{%
  \begin{math}
    x \beq{{\cal F}}{{\cal X}} y
    \Leftrightarrow
    \exists {\cal Y} = (Y, \beta) . \exists f : {\cal X} \to {\cal Y} . f(x) = f(y)
  \end{math}}
  \smallskip
  is called \emph{behavioural equivalence}.
\end{definition}

\noindent
In Definition~\ref{def:behaviouralEquivalenceNew} we use the word
\emph{equivalence}, but this should not be taken for granted, of
course. Clearly, $\beq{}{}$~is reflexive and symmetric, but
transitivity is in principle to be shown. However (see
\cite{Hughes2001}, Theorem 1.2.4) pushouts in a $\textbf{Set}$-based category
of coalgebras exist and are computed in the base category, which
immediately yields transitivity of~$\beq{}{}$. It is also obvious that
when a final coalgebra exists, $\beq{}{}$~coincides with the kernel of
the final morphism from~${\cal X}$.

\begin{lemma}
  \label{lem:quotientsOfClosureCoalgebras}
Consider a model $\mathcal{M} = ((X,\closurename{X}),\calV)$ and ${\cal X} =
(X,\eta)$ as in Definition \ref{def:closureCoalgebraOfAModel}. Let ${\cal Y} =
(Y,\theta)$ be a $\textbf{C}$-coalgebra. Let $f : {\cal X} \twoheadrightarrow
{\cal Y}$ be a surjective coalgebra homomorphism. Define $\mathcal{C}{Y}{(B \subseteq
Y)} = \{ \, y \in Y \mid B \in (\theta y)_2 \, \}$. Then $(Y,\closurename{Y})$
is a closure space.
\end{lemma}

\begin{proof}
  See Appendix~\ref{appendix}.
\end{proof}

\noindent
The proof of Theorem~\ref{thm:closureCoalgebraLogicalEquivalence} below
requires the following lemma, whose proof crucially relies on the fact
that $A \subseteq B$ implies $\closurename{} \mkern-2mu A \subseteq
\closurename{}B$.

\begin{lemma}
  \label{lem:closure-of-equivalent-points}
  Let $f$ be the function mapping each element of~$X$ into its
  equivalence class up to~$\inflogeq$. Then it holds that $((x_1
  \inflogeq x_2) \land x_1 \in \mathcal{C}{} \mkern-2mu A)$ implies $x_2
  \in \closurename{} f^{-1} (\pws f) A$, for all $x_1,x_2 \in X$ and
  $A \subseteq X$.
\end{lemma}

\begin{proof}
  See Appendix~\ref{appendix}.
\end{proof}

\noindent
With Lemma~\ref{lem:quotientsOfClosureCoalgebras} and
Lemma~\ref{lem:closure-of-equivalent-points} available, we arrive at
the following result.

\begin{theorem}
  \label{thm:closureCoalgebraLogicalEquivalence}
  Consider a closure model $\mathcal{M} = ((X,\closurename{}),\calV)$
  and ${\cal X} = (X,\eta)$, with~$\eta$ as in
  Definition~\ref{def:closureCoalgebraOfAModel}. It holds that the
  relations $\inflogeq^{\mathcal{M}}$ and $\beq{\textbf{C}}{{\cal X}}$
  coincide.
\end{theorem}

\begin{proof}
    First, let us prove that if we have $\mathcal{M}, x_1 \models \Phi
    \Leftrightarrow \mathcal{M}, x_2 \models \Phi$ for all ${\bf F}$ and $x_1,
    x_2 \in X$, then there are a coalgebra ${\cal Y} = (Y,\theta)$ and a
    coalgebra homomorphism $f :X \to Y$ with $f x_1 = f x_2$.  Let $Y$
    be the set of equivalence classes of~$X$ under
    $\inflogeq^{\mathcal{M}}$.  Let $f$ be the canonical map, mapping each
    $x \in X$ to its equivalence class~$[x]$ with respect
    to~$\inflogeq^{\mathcal{M}}$. Note that each element of~$Y$ is of the
    form~$f \mkern-1mu x$ for some~$x$. Define $tx = \{ \, (\pws f) A
    \mid A \in (\eta x)_2 \, \}$, and let $\theta(f x) = ((\eta
    \mkern1mu x)_1,t(x))$. Observe that such a definition makes $f$ a
    coalgebra homomorphism by construction, that is, $\theta \circ f =
    (\textbf{C} f) \circ \eta$. We need to show that the
    definition of~$\theta$ is independent from the representative~$x$,
    i.e.\ whenever $x_1 \inflogeq x_2$, we have $\theta (f x_1) =
    \theta (f x_2)$.  Indeed, it is obvious that $(\eta x_1)_1 = (\eta
    x_2)_1$, since by logical equivalence $x_1$ and~$x_2$ satisfy the
    same atomic propositions. We thus need to show that $t\, x_1 = t\,
    x_2$. All elements of~$t\, x_1$ are of the form $(\pws f) A$ with
    $x_1 \in \mathcal{C}{X} \mkern-2mu A$. By
    Lemma~\ref{lem:closure-of-equivalent-points}, we then have $x_2
    \in \closurename{X}(f^{-1}(\pws f)A)$, thus $f^{-1}((\pws f)A) \in
    (\eta x_2)_2$ by definition of~$\eta$.  Therefore, $(\pws f)
    (f^{-1} (\pws f) \mkern-0mu A) \in t x_2$ by definition of~$t$,
    and since $(\pws f) f^{-1} ((\pws f) \mkern-0mu A) = (\pws f)
    \mkern-0mu A$, we obtain $t\, x_1 \subseteq t\, x_2$.  The same
    reasoning can also be used in the other direction, proving that
    the two sets are equal.

    Next, we shall prove that if $((X,\closurename X),\calV{})$
    is a closure model, with corresponding $\textbf{C}$-coalgebra
    $(X,\eta)$, $({\cal Y},\theta)$ is a
    $\textbf{C}$-coalgebra, $f : X \to Y$ is a coalgebra
    homomorphism, and $f x_1 = f x_2$, then we have that $\mathcal{M}, x_1
    \models \Phi \iff \mathcal{M}, x_2 \models \Phi$ for all~$\Phi$.  We
    will actually prove a slightly stronger statement, based upon
    Lemma~\ref{lem:quotientsOfClosureCoalgebras}. Given that the
    category of $\textbf{C}$-coalgebras has a epi-mono
    factorization system inherited from~$\textbf{Set}$ (that is, each
    coalgebra homomorphism can be written as $m\circ e$ where $e$~is
    surjective and $m$~is injective), let us restrict, without loss of
    generality, to the case when $f$ is surjective.  By
    Lemma~\ref{lem:quotientsOfClosureCoalgebras}, there is a closure
    operator $\closurename Y$ such that $\mathcal{M}' = ((Y,\closurename
    Y),\theta_1)$ is a closure model. Therefore, we can also interpret
    formulas on points of~$Y$.  Once this is established, under the
    hypothesis that $f$~is a (surjective) homomorphism, we shall prove
    that for all $x \in X$, we have $\mathcal{M}, x \models \Phi \iff
    \mathcal{M}', fx \models \Phi$ for all~$\Phi$.  This entails the main
    thesis as follows: whenever $f x_1 = f x_2$, for all~$\Phi$, we
    have $\mathcal{M}, x_1 \models \Phi \iff \mathcal{M}',f x_1 \models \Phi
    \iff \mathcal{M}', f x_2 \models \Phi \iff \mathcal{M}, x_2 \models \Phi$.  The proof proceeds by induction
    on the structure of~$\Phi$. The relevant case is that for formulas
    of the form~$\mathcal{N} \Phi$. The proof of this case is split into two
    directions.  Below, for any $\Phi$, we denote by~$S^X_\Phi$ the
    set $\{ \, x \in X \mid \mathcal{M}, x \models \Phi \, \}$ and
    with~$S^Y_\Phi$ the set $\{ \, y \in Y \mid \mathcal{M}', y \models
    \Phi \, \}$.

    ($\Rightarrow$) If $\mathcal{M}, x \models \mathcal{N} \Phi$, then $x \in
    \closurename X S^X_\Phi$ by definition of satisfaction, hence
    $S^X_\Phi \in (\eta \mkern1mu x)_2$ by definition of~$\eta$, thus
    $(\pws f) S^X_\Phi \in (\theta f x)_2$ since $f$~is a coalgebra
    homomorphism, and therefore $f x \in \closurename{Y} ((\pws
    f)S^X_\Phi)$.

    Now observe that whenever $y \in (\pws f) S^X_\Phi$, we have that
    $y = f \mkern-1mu x$ and $\mathcal{M}, x \models \Phi$ for
    some~$x$. Therefore, by inductive hypothesis, $\mathcal{M}',y \models
    \Phi$. In other words, $(\pws f) S^X\Phi \subseteq S^Y_\Phi$. By
    properties of closure, we have $\mathcal{C} Y {((\pws f)S^X\Phi)}
    \subseteq \mathcal{C} Y {S^Y_\Phi}$. Thus, by the above derivation,
    we have $f \mkern-1mu x \in \mathcal{C} Y {S^Y_\Phi}$, that is
    $\mathcal{M}', f x \models \mathcal{N} \Phi$.

    ($\Leftarrow$) If $\mathcal{M}', f x \models \mathcal{N} \Phi$, then $f x
    \in \mathcal{C}{Y} S^Y_\Phi$ by definition of~$S^Y_\Phi$, hence
    $S^Y_\Phi \in (\theta f x)_2$ by definition of~$\theta$, and
    $S^Y_\Phi \in ((\textbf{C} f) (\eta \mkern1mu x))_2$ since $f$~is a
    coalgebra homomorphism. Thus $(\pws f) A = S^Y_\Phi$ for some $A
    \in (\eta \mkern1mu x)_2$, hence $(\pws f) A = S^Y_\Phi$ and $x
    \in \mathcal{C} X A$, from which it follows that $\mathcal{M}',f x'
    \models \Phi$ for all $x' \in A$. By induction hypothesis,
    $\mathcal{M},x' \models \Phi$ for all $x' \in A$, hence $A \subseteq
    S^X_\Phi$ and $\mathcal{C} X \mkern-2mu A \subseteq \mathcal{C} X
    \mkern-1mu S^X_\Phi$ by
    monotonicity of closure. It follows that $x \in \mathcal{C} X \mkern-1mu
    S^X_\Phi$ and $\mathcal{M}, x \models \mathcal{N} \Phi$, as was to be shown.
    \qed

\end{proof}

\section{Introduction}
\label{sec:Introduction}

Traditional modal logic enjoys a topological interpretation, according to which
the modal formula $\diamond\mkern1mu \Phi$ is true at a point~$x$ of a topological space,
whenever $x$ belongs to the \emph{topological closure} of the set of points at
which $\Phi$ is true. This fundamental observation has led to a variety of
extensions of the basic framework, with different proof systems and
computational properties, cf.~\cite{HBSL}.

\emph{Model checking} has been studied for the case of spatial logics only
recently. In order to retain the topological flavour, but aiming at analysis of
more general structures, also encompassing graphs, the \emph{Spatial Logic for
Closure Spaces} ($SLCS\xspace$) has been proposed by Ciancia et al.\ in~\cite{CLLM14}
together with an algorithm for model checking of finite models. The logic
$SLCS\xspace$ is interpreted on \emph{closure spaces} (a generalization of topological
spaces where the closure operator is not necessarily idempotent). We refer the
reader to~\cite{CLLM16} for a full account of the logic and its main features
and properties -- including its extension with a \emph{collective} fragment. The
logic and its model checkers {\ttfamily{topochecker}}\xspace~\cite{CGLLM15} and
{\ttfamily{VoxLogicA}}\xspace~\cite{BCLM19} have been applied to several case
studies~\cite{CLLM16,CGLLM15,CGGLLM18} including a declarative approach to
medical image analysis~\cite{BCLM16,BCLM19,BCLM19a,BBCLM19}. An encoding of the
discrete Region Connection Calculus RCC8D of~\cite{RLG13} into the collective
variant of $SLCS\xspace$ has been proposed in~\cite{CLM19}. The logic has also
inspired other approaches to spatial reasoning in the context of signal temporal
logic and system monitoring~\cite{BBLN17,NBCLM18} and in the verification of cyber-physical systems \cite{TKG17}.

In this work, we initiate the study of bisimilarity and minimization algorithms
for spatial structures, employing equivalence relations on points of a closure
space that are \emph{adequate} with respect to spatial logical equivalence. That
is, we require that two points are bisimilar if and only if they satisfy the
same formulas of a (chosen) spatial logical language. For the topological case,
one such equivalence has been provided by Aiello and Van Benthem~\cite{BeB07},
under the name of \emph{topo-bisimilarity}. This relation is adequate with
respect to logical equivalence of basic infinitary modal logic, i.e.\ a boolean
logic with one modal operator, and infinitary conjunction/\-disjunction. In
contrast, besides basic modalities, the logic $SLCS\xspace$ features operators that
make use of reachability via paths of bounded and unbounded length (for
instance, the \emph{surrounded} and \emph{touch} operators of~\cite{CLLM16}).
Although the study of such operators has not been developed in full detail in
the classical spatial logics literature, they have proved useful in case
studies. For instance, the ability to identify two areas, characterised by given
logical formulas, that additionally are in contact with each other, while
retaining the point-based approach of topo-logics, has been the key to derive a
segmentation algorithm that labels brain tumours in three-dimensional medical
images, with accuracy in par with manual segmentation, and best-in-class machine
learning methods~\cite{BCLM19}.

In the present paper, we focus on two different, related problems. First of all,
we identify a spatial definition of bisimilarity for quasi-discrete models
(those that correspond to graphs), and a minimization algorithm for
\emph{finite} models, in the setting of logics with reachability. This is
directly aimed at supporting the future developments of the spatial model
checking methodology that is currently in use, e.g.\ in~\cite{BCLM19}. In
Section~\ref{sec:CMBisimilarity} we present a set-theoretical definition, and
provide some examples. In Section~\ref{sec:CMCoalgebraically}, we provide a
coalgebraic rendition of such an equivalence. In Section~\ref{sec:SLCSEq}, we
prove adequacy with respect to logical equivalence of a logic with two
reachability operators (corresponding to the two directions of ``reaching'' and
``being reached''). In Section~\ref{sec:tool} we introduce an open source tool
that is able to minimize finite models via coalgebraic partition refinement.

The second research question that we address here, is whether the theory of
topo-bisimilarity of~\cite{BeB07}, characterising infinitary modal logic
(without reachability operators), can be generalised to closure models (not
limited to the quasi-discrete ones). In Section~\ref{sec:generalization}, we
first provide a consistent generalization, obtained by appropriately replacing
the notion of an \emph{open neighbourhood} with one that is equivalent in the
restricted setting of topological spaces, but not in the more general one. The
defined equivalence relation is adequate for infinitary modal logic when
interpreted on closure spaces. Then, we provide a coalgebraic definition. We
prove that logical equivalence of infinitary modal logic can be characterised as
behavioural equivalence for coalgebras of the \emph{closure functor}
$\pws(\pws(-))$. The notion we propose is similar in spirit to
\emph{neighbourhood frames} (see~\cite{HKP09}), although we use the
\emph{covariant} power set, therefore staying closer to the more classical
 literature on coalgebras in Computer Science.

Although the results we present are sound and stable, we consider them as a
preliminary foundation. Future work will be devoted to the characterisation of
logical equivalence for variants of the considered logics (for instance, those
that cannot express one-step modalities, logics with distances, etc.). We
provide some discussion on these matters in Section~\ref{sec:discussion}.

\section{Preliminaries}
\label{sec:Preliminaries}

Given set~$X$ and relation $R \subseteq X \times X$, we let $R^{\,t}$
denote the \emph{transitive closure} of~$R$ and let $R^{-1}$ denote
the inverse of~$R$, i.e.\ $R^{-1} = \ZET{(x_1,x_2)}{(x_2,x_1)\in R}$.
For $x \in X$, we let $[x]_R$ denote the equivalence class of~$x$ (we
will omit the subscript whenever this does not cause confusion).  We
let $\pws{}$ denote the covariant powerset functor; for $f : X \to Y$
and $A \subseteq X$, its action on arrows $\pws{}f \, A$, often
abbreviated to $f \, A$, is defined as $\ZET{fa}{a \in A}$.
Similarly, $\fpws{X}$ denotes the covariant \emph{finite} powerset
functor. For $f : X \to Y$ a function, we denote by $f^{-1} : \pws Y \to \pws X$ its ``relational'' inverse, that is the function mapping $B \subseteq Y$ to $\{ x \in X \mid f x \in B \}$. We will often use currying for function type definitions and
applications, when this does not create confusion.

\begin{definition}\label{def:ClosureSpaces}
 A \emph{closure space} is a pair $(X,\closurename{})$ where $X$ is a
 non-empty set (of {\em points}) and \emph{$\closurename{} : \pws{X} \to
   \pws{X}$} is a function satisfying the following axioms.
 \begin{enumerate}
 \item $\mathcal{C}{}{\emptyset} = \emptyset$
 \item $A \subseteq \mathcal{C}{}{A}$ for all  $A \subseteq X$
 \item $\mathcal{C}{}{(A_1 \cup A_2)} = \mathcal{C}{}{A_1} \cup
   \mathcal{C}{}{A_2}$ for all $A_1,A_2\subseteq X$
 \end{enumerate}
\end{definition}

\noindent
The definition of a closure space goes back to Eduard Čech.  By the Kuratowski
definition, topological spaces coincide with the sub-class of closure spaces for
which also the \emph{idempotence} axiom $\mathcal{C}{}{(\mathcal{C}{}{A})} =
\mathcal{C}{}{A}$ holds. The \emph{interior} operator is the dual of closure:
$\interior{}{A} = \overline{\mathcal{C}{}{(\overline{A})}}$.
Given a relation $R \subseteq X \times X$, the function
$\closurename{R}: \pws{X} \to \pws{X}$ with \emph{$\mathcal{C}{R}(A) = A
  \cup \ZET{x}{\exists \mkern1mu a \in A \colon a \, R \,x}$}
satisfies the axioms of Definition~\ref{def:ClosureSpaces}, thus
making $(X,\closurename{R})$ a closure space. We say that
$(X,\closurename{R})$ is \emph{based on}~$R$. It can be shown that the
sub-class of closure spaces that can be generated by a relation as
above coincides with the class of \emph{quasi-discrete} closure
spaces, i.e.\ closure spaces where every $x \in X$ has a minimal
neighbourhood or, equivalently, for each $A \subseteq X, \,
\mathcal{C}{}{A} = \bigcup_{a \in A} \mathcal{C}{}{\SET{a}}$. Thus discrete
structures, like graphs or Kripke structures can be seen
as quasi-discrete closure spaces. With reference to a quasi-discrete
closure space $(X,\closurename{R})$ based on a relation~$R$, we define
the abbreviations $\stackrel{\rightarrow}{\closurename{}}, \stackrel{\leftarrow}{\closurename{}} : X \to \pws{X}$
by $\forwclosure{x} = \mathcal{C}{R}(\SET{x})$ and $\backclosure{x} =
\mathcal{C}{{R^{-1}}}(\SET{x})$.

\begin{definition}\label{def:ContinuousFunction}
  A \emph{continuous function} from closure space
  $(X_1,\closurename{1})$ to closure space $(X_2,\closurename{2})$ is
  a function $f : X_1 \to X_2$ such that, for all sets $A \subseteq
  X_1$, it holds that $f (\mathcal{C}{1}{A}) \subseteq \mathcal{C}{2}{(f\,A)}$.
\end{definition}

\noindent
We fix a set $AP$ of \emph{atomic predicates}.  A closure model
$\mathcal{M}=((X,\closurename{}), \calV)$ is a pair with
$(X,\closurename{})$ a closure space, and $\calV: AP \to \pws{X}$
the (atomic predicate) valuation (function). We define $\pevalname^{\mbox{-} \mkern-2mu \mbox{\scriptsize 1}}:
\pws{X} \to \pws{AP}$ with \emph{$\invpeval{A} = \ZET{p \in
    AP}{\exists \mkern1mu a \in A \colon a \in {\cal V} p}$} and we let
$\invpeval{}{x}$ abbreviate $\invpeval{}{\SET{x}}$. We say that a
closure model $\mathcal{M} = ((X,\closurename{}), \calV)$ is
quasi-discrete if $(X,\closurename{})$ is quasi-discrete.  A
quasi-discrete closure model $((X,\closurename{R}), \calV)$ is
\emph{finitely closed} if $\forwclosure{}{x}$ is finite for all $x \in
X$. Similarly, we say that $\mathcal{M}$ is \emph{finitely backward closed}
if $\backclosure{}{x}$ is finite for all $x \in X$.

In the following definition, $(\mathbb{N}, \closurename{\succ})$ is the
quasi-discrete closure space of the natural numbers $\mathbb{N}$ with the
{\em successor} relation $\succ$.

\begin{definition}
  \label{def:qspath}
  A quasi-discrete \emph{path} $\pi$ in $(X,\closurename{})$ is a
  continuous function from $(\mathbb{N}, \closurename{\succ})$ to
  $(X,\closurename{})$.
\end{definition}

\noindent
We recall some basic definitions from coalgebra. See e.g.~\cite{Rut00}
for more details. For a functor ${\cal F} : \textbf{Set} \to \textbf{Set}$ on the
category $\textbf{Set}$ of sets and functions, a \emph{coalgebra}~${\cal X}$
of~${\cal F}$ is a set~$X$ together with a mapping $\alpha : X \to {\cal F}
X$.  A \emph{homomorphism} between two ${\cal F}$-coalgebras ${\cal X} =
(X,\alpha)$ and~${\cal Y} = (Y,\beta)$ is a function $f : X \to Y$ such
that $({\cal F} f) \mathop{\raisebox{0.5pt}{\scriptsize $\circ$}} \alpha = \beta \mathop{\raisebox{0.5pt}{\scriptsize $\circ$}} f$. An
${\cal F}$-coalgebra $(\Omega_{{\cal F}},\omega_{{\cal F}})$ is called
\emph{final}, if there exists, for every ${\cal F}$-coalgebra
${\cal X}=(X,\alpha)$, a unique homomorphism
$\fmorph{{\cal F}}{{\cal X}}{\cdot} : (X,\alpha) \to
(\Omega_{{\cal F}},\omega_{{\cal F}})$. Two elements~$x_1, x_2$ of an
${\cal F}$-coalgebra~${\cal X}$ are called {\em behavioural equivalent} with
respect to~${\cal F}$ if $\fmorph{{\cal F}}{{\cal X}}{x_1} =
\fmorph{{\cal F}}{{\cal X}}{x_2}$, denoted $x_1 \beq{{\cal F}}{{\cal X}} x_2$.  In
the notation $\fmorph{{\cal F}}{{\cal X}}{\cdot}$ as well as
$\beq{{\cal F}}{{\cal X}}$, the indication of the specific coalgebra~${\cal X}$
will be omitted when clear from the context.
A functor~${\cal F}$ is called \emph{$\kappa$-accessible} if it preserves
$\kappa$-filtered colimits for some cardinal number~$\kappa$. However,
in the category~$\textbf{Set}$, we have the following characterization of
accessibility: for every set~$X$ and any element $\xi \in {\cal F} X$,
there exists a subset $Y \subseteq X$ with ${|} Y {|} < \kappa$, such
that $\xi \in {\cal F} Y$. It holds that a functor has a final coalgebra
if it is $\kappa$-accessible for some cardinal
number~$\kappa$. See~\cite{AP04:tcs}.

\section{$SLCS\xspace\ $ and logical equivalence}
\label{sec:SLCSEq}

We use the following version of the logic~$SLCS\xspace$ for a given set
atomic propositions~$AP$.

\begin{equation}
  \label{def:syntax}
  {\bf F}  ::=  p  \,\mid\,  \neg \, {\bf F}  \,\mid\,  {\bf F} \, \lor \, {\bf F}  \,\mid\,
  \lrcs{{\bf F}}{{\bf F}}   \,\mid\,  \lrcd{{\bf F}}{{\bf F}}
\end{equation}
Satisfaction $\mathcal{M}, x \models {\bf F}$ of a formula~${\bf F}$ at point
$x \in X$ in a quasi-discrete closure model $\mathcal{M} = ((X,\closurename{R}), {\cal V})$ is defined in Figure~\ref{def:satisfaction} by induction on the structure of formulas.

\begin{figure}
\centering
\emph{%
\fbox{%
\begin{math}
\begin{array}{r c l c l c l l}
\mathcal{M},x & \models  & p \in P & \Leftrightarrow & x  \in {\cal V} p \\
\mathcal{M},x & \models  & \neg \,{\bf F} & \Leftrightarrow & \mathcal{M},x  \models {\bf F} \mbox{ does not hold}\\
\mathcal{M},x & \models  & {\bf F}_1\, \lor \,{\bf F}_2 & \Leftrightarrow &
\mathcal{M},x  \models {\bf F}_1 \mbox{ or } \mathcal{M},x  \models {\bf F}_2\\
\mathcal{M},x & \models  & \lrcs{{\bf F}_1}{{\bf F}_2} & \Leftrightarrow &
\mbox{there exists a path } \pi  \mbox{ and an index } \ell \mbox{
  such that
}\\
 & &  & &
\mbox{\hspace{0.1in}}\pi(0)=x \, \mbox{ and } \,  \mathcal{M}, \pi(\ell) \models {\bf F}_1 \mbox{ and }\\
 & &  & &
\mbox{\hspace{0.1in}}
\mathcal{M}, \pi(j) \models {\bf F}_2, \mbox{ for all } j \mbox{ with }
0<j<\ell \\
\mathcal{M},x & \models  & \lrcd{{\bf F}_1}{{\bf F}_2} & \Leftrightarrow &
\mbox{there exists a path } \pi  \mbox{ and an index } \ell \mbox{
  such that
} \\
 & &  & &
\mbox{\hspace{0.1in}}\pi(\ell)=x \, \mbox{ and } \,  \mathcal{M}, \pi(0) \models {\bf F}_1 \mbox{ and }\\
 & &  & &
\mbox{\hspace{0.1in}}
\mathcal{M}, \pi(j) \models {\bf F}_2, \mbox{ for all } j \mbox{ with } 0<j<\ell\\
\end{array}
\end{math}
}
}
\caption{Definition of the satisfaction relation\label{def:satisfaction}}
\end{figure}

\noindent
Some useful abbreviations are defined in
Figure~\ref{def:abbreviations}.
The operator~$\mathcal{N}$ is the \emph{near} operator, namely the logical
counterpart of the closure function of closure spaces: $x$~satisfies
$\mathcal{N} {\bf F}$ iff it is ``close'' to~${\bf F}$, as defined
in~\cite{CLLM16}\footnote{In~\cite{CLLM16} the following definition
  has been used: $\mathcal{M}, x \models \mathcal{N} {\bf F} \Leftrightarrow x \in
  \mathcal{C}{R}{\ZET{y}{\mathcal{M}, y \models {\bf F}}}$; it is easy to show
  that $\mathcal{M}, x \models \mathcal{N} {\bf F}$ if and only if $\mathcal{M}, x
  \models \lrcd{{\bf F}}{\bot}$.}.
The operator~$\mathcal{S}$ is the \emph{surrounded}
\footnote{Named ``spatial until'' and denoted by ``${\cal U}$''
  in~\cite{CLLM14}.} operator: a point $x$ satisfies ${\bf F}_1 \,
\mathcal{S} \, {\bf F}_2$ if it satisfies~${\bf F}_1$ and no path starting
at~$x$ can reach any point satisfying $\neg \, {\bf F}_1$ without first
passing by a point satisfying~${\bf F}_2$, i.e.\ $x$~lays in an area
that satisfies~${\bf F}_1$ and that is surrounded by points satisfying
${\bf F}_2$.
The operator~$\calP$ is the \emph{propagation} operator introduced
in~\cite{CLLM16}: $x$~satisfies ${\bf F}_1 \, \calP \, {\bf F}_2$ if it
satisfies~${\bf F}_2$ and it is reachable from a point
satisfying~${\bf F}_1$ via a path such that all of its points, except
possibly the starting point, satisfy~${\bf F}_2$. For more derived
operators the reader is referred to~\cite{CLLM16}.

\begin{example} Consider Example~\ref{exa:ExaDue}. All the red points in Figure~\ref{fig:ExaDue}(a-c) satisfy $\mathcal{N}\, {\tt blue}$. The middle point in Figure~\ref{fig:ExaDue}(d) (point $d_{33}$) does not satisfy such formula, although it satisfies $\lrcs{\tt blue}{\tt red}$.
\end{example}

\begin{figure}
\centering
\emph{%
\fbox{%
\begin{math}
\begin{array}{l c l}
  {\bf F}_1 \, \land \, {\bf F}_2 & \equiv & \neg (\neg {\bf F}_1 \, \lor
  \, \neg {\bf F}_2) \\
  \bot & \equiv & p \, \land \, \neg p \\
  \top & \equiv & \neg\bot \\
  \mathcal{N} {\bf F} & \equiv & \lrcd{{\bf F}}{\bot} \\
  {\bf F}_1 \, \mathcal{S} \, {\bf F}_2 & \equiv & {\bf F}_1 \, \land \,
  \neg(\lrcs{\neg({\bf F}_1 \, \lor \, {\bf F}_2)}{\neg {\bf F}_2}) \\
  {\bf F}_1 \, \calP \, {\bf F}_2 & \equiv & {\bf F}_2 \land
  \lrcd{{\bf F}_1}{{\bf F}_2}
\end{array}
\end{math}
}
}
\caption{Derived operators~\label{def:abbreviations}}
\end{figure}

\begin{definition}
  \label{def:SLCSEQ}
  The $SLCS\xspace $\ equivalence relation with respect to model~$\mathcal{M}$,
  namely $\slcseq^{\mathcal{M}} \subseteq X \times X$, is defined as
  follows: $x_1 \slcseq^{\mathcal{M}} x_2$ iff for all $SLCS\xspace$
  formulas~${\bf F}$ we have that $\mathcal{M}, x_1 \models {\bf F}
  \Leftrightarrow \mathcal{M}, x_2 \models {\bf F}$.
\end{definition}

\noindent
In the following, for the sake of notational simplicity, we will write
$\slcseq$ instead of $\slcseq^{\mathcal{M}}$ whenever this cannot cause
confusion.

\begin{lemma}
  \label{lemma:slcseqsubcsbisim}
  If a quasi-discrete closure model~$\mathcal{M}$ is finitely closed and
  finitely backward closed, then $\slcseq \, \subseteq\,  \altcmbisim$.
\end{lemma}

\begin{proof}
See Appendix~\ref{appendix}.
\end{proof}

\begin{lemma}\label{lemma:csbisimsubslcseq}
If $\mathcal{M}$ is a quasi-discrete closure model, then $\altcmbisim\, \subseteq\,  \slcseq$.
\end{lemma}

\begin{proof}
See Appendix~\ref{appendix}.
\end{proof}

\noindent
Lemma~\ref{lemma:slcseqsubcsbisim} and
Lemma~\ref{lemma:csbisimsubslcseq} bring the following result.

\begin{theorem}
  \label{correspondence}
  If closure model $\mathcal{M} = ((X,\closurename{}), {\cal V})$ is
  quasi-discrete, finitely closed, and finitely backward closed,
  then for all $x_1,x_2 \in X$, $ x_1 \, \altcmbisim\, x_2$ iff we
  have $x_1 \, \slcseq\, x_2$.
\end{theorem}

\begin{example} Let us provide formulas that uniquely characterise each of the points in Figure~\ref{fig:minimized-examples}, proving that there are no different, bisimilar points in that figure, when it is considered as a single model by taking the disjoint union of the models (a) and (b).
Let $\Phi_1 = {\tt blue} \land \mathcal{N} {\tt red}$, $\Phi_2 = {\tt red} \land \mathcal{N} {\tt blue}$, $\Phi_3 =  {\tt red} \land \lnot \mathcal{N} {\tt blue}$.
The blue point in Figure~\ref{fig:minimized-examples}(a) is the only point satisfying $\Phi_1 \land \lnot \lrcs{\Phi_3}{\top}$. The red point in Figure~\ref{fig:minimized-examples}(a) is the only point satisfying $\Phi_2 \land \lnot \mathcal{N} \Phi_3$. The blue point in Figure~\ref{fig:minimized-examples}(b) is the only point satisfying $\Phi_1 \land \lrcs{\Phi_3}{\top}$. The middle red point in Figure~\ref{fig:minimized-examples}(b) is the only point satisfying $\Phi_2 \land \mathcal{N} \Phi_3$. The rightmost red point in Figure~\ref{fig:minimized-examples}(b) is the only point satisfying $\Phi_3$.
\end{example}

\noindent
We close this section with a stronger version of
Lemma~\ref{lemma:slcseqsubcsbisim}, and consequently of
Theorem~\ref{correspondence}.  Let us consider the sub-logic $\SMCSm$
of~$SLCS\xspace$ given by
\begin{equation}\label{eq:sublogic}
  {\bf F}  ::=  p  \,\mid\,  \neg \, {\bf F}  \,\mid\,  {\bf F} \, \lor \, {\bf F}  \,\mid\,
  \lrcs{{\bf F}}{\bot} \,\mid\, \lrcd{{\bf F}}{\bot}
\end{equation}
and let $x_1 \, \slcsmeq\, x_2$ denote the logical equivalence with
respect to the sub-logic~$\SMCSm$.

Lemma~\ref{lemma:restrict} below lays the basis for showing that for
two points $x_1$ and~$x_2$ with $x_1 \, \slcsmeq\, x_2$ also holds
that $x_1 \, \slcseq\, x_2$, i.e.\ using the full version
$\lrcs{{\bf F}_1}{{\bf F}_2}$ and $\lrcd{{\bf F}_1}{{\bf F}_2}$ of the
${\stackrel{\rightarrow}{\rho}}$ and~${\stackrel{\leftarrow}{\rho}}$ operators does not add discriminatory
power with respect to using the restricted versions
$\lrcs{{\bf F}}{\bot}$ and $\lrcd{{\bf F}}{\bot}$.

\begin{lemma}
  \label{lemma:restrict}
  Formulas ${\bf F}_1,{\bf F}_2$ of~$\SMCSm$ of Equation~\ref{eq:sublogic}
  satisfy the following.
  \begin{enumerate}
  \item If $\mathcal{M}, x_1 \models \lrcs{{\bf F}_1}{{\bf F}_2}$ and $\mathcal{M},
    x_2 \not\models \lrcs{{\bf F}_1}{{\bf F}_2}$ then there exists
    $\Lambda_{{\bf F}_1,{\bf F}_2}$ in the language of
    Equation~\ref{eq:sublogic} such that $\mathcal{M}, x_1 \models
    \Lambda_{{\bf F}_1,{\bf F}_2} $ and $\mathcal{M}, x_2 \not\models
    \Lambda_{{\bf F}_1,{\bf F}_2} $.
  \item If $\mathcal{M}, x_1 \models \lrcd{{\bf F}_1}{{\bf F}_2}$ and $\mathcal{M},
    x_2 \not\models \lrcd{{\bf F}_1}{{\bf F}_2}$ then there exists
    $\Lambda_{{\bf F}_1,{\bf F}_2}$ in the language of
    Equation~\ref{eq:sublogic} such that $\mathcal{M}, x_1 \models
    \Lambda_{{\bf F}_1,{\bf F}_2} $ and $\mathcal{M}, x_2 \not\models
    \Lambda_{{\bf F}_1,{\bf F}_2} $.
\end{enumerate}
\end{lemma}

\begin{proof}
See Appendix~\ref{appendix}.
\end{proof}

\noindent
Using the above lemma, one can then prove the following result.

\begin{theorem}
  \label{correspondencem}
  If closure model $\mathcal{M} = ((X,\closurename{}), {\cal V})$ is
  quasi-discrete, finitely closing, and finitely backward closing,
  then for all $x_1,x_2 \in X$ we have $ x_1 \, \altcmbisim\, x_2$ iff
  $x_1 \, \slcsmeq\, x_2$.
\end{theorem}

\begin{remark}
  \label{rem:BaFLog}
  With reference to Remark~\ref{rem:BaFbis} it is easy to see that
  while $\mathcal{M}, x_1 \models \lrcd{p}{\bot}$, we have $\mathcal{M}, x_2
  \not\models \lrcd{p}{\bot}$.
\end{remark}

\section{A tool for spatial minimization}
\label{sec:tool}

One of the major advantages of defining bisimilarity coalgebraically
is the availability of the partition refinement algorithm, sometimes
referred to as \emph{iteration along the final sequence} (see
e.g.~\cite{AdamekBHKMS12}). In the category $\textbf{Set}$, the formulation of
the algorithm is particularly simple and quite similar to classical
results such as~\cite{HOPCROFT1971189}. In
Algorithm~\ref{fig:coalgebraic-partition-refinement}, we illustrate
the algorithm. For $q$ a function, we let $\mathit{ker}(q)$ be its
\emph{kernel}, namely the partition of the domain induced by~$q$.

\begin{algorithm}
    \textbf{function} \texttt{minimizeRec} ($\eta : X \to {\cal F} X$,$q :
    X \to {\cal F}^k \{*\}$)

    \quad \textbf{let} $q' = ({\cal F} q) \circ \eta$

    \quad \textbf{if} ($\mathit{ker}(q) = \mathit{ker}(q')$)
    \textbf{then}

    \qquad \textbf{return}~$q$

    \quad \textbf{else}

    \qquad \textbf{return} \texttt{minimizeRec($\eta$,$q'$)}

    \textbf{function} \texttt{minimize}($\eta : X \to {\cal F} X$)

    \quad \textbf{return} \texttt{minimizeRec($\mathit{\eta}$,$\lambda
      x . * $)}
\caption{The coalgebraic partition refinement algorithm in $\textbf{Set}$.}
\label{fig:coalgebraic-partition-refinement}
\label{alg:minimize}
\end{algorithm}

\noindent The function \texttt{minimize} accepts as input a ${\cal F}$-coalgebra $\eta$ and returns the bisimilarity quotient of its carrier set. Minimization is implemented via the function \texttt{minimizeRec}, which accepts as input the coalgebra map $\eta$, and a surjective function $q$, whose kernel is a partition of the carrier set. Such function is initialised to $\lambda x . *$, where $*$ is the only element of the singleton $\{ * \}$, that is, the algorithm starts by assuming that all the elements of the carrier are bisimilar. The algorithm then applies one \emph{refinement} step, by applying the functor ${\cal F}$ to $q$ and composing the result with $\eta$; this yields a new function $q' = ({\cal F} q) \circ \eta$. Note that such function is ``almost always'' surjective\footnote{Function $q'$ may actually fail to be surjective when the carrier is empty. All $\textbf{Set}$ functors preserve epimorphisms from non-empty sets. If the carrier is empty then so are both $q$ and $q'$, therefore the algorithm terminates in one step.}. Intuitively, at each iteration,  function $q'$ is obtained from $q$ by splitting the partitions induced by $q$ according to the ``observations'' that are obtained ``in one more step'' from $\eta$.     If $q$ and $({\cal F} q) \circ \eta$ represent the same partition -- that is, the two functions have the same kernel -- the algorithm returns $q$, which denotes the coarsest partition that does not identify non-bisimilar states; otherwise, the procedure is iterated. Termination is guaranteed on finite models as for each finite model, there are  only a finite number of partitions.

Algorithm \ref{alg:minimize}, instantiated using the functor ${\cal T}$ of
Section~\ref{sec:CMCoalgebraically}, has been implemented in a multi-platform
tool called \textbf{MiniLogicA}, which is available for the major operating
systems at \url{https://github.com/vincenzoml/MiniLogicA} under a permissive
open source license. The tool is implemented in the language F\#\footnote{See
\url{https://fsharp.org}.}. The tool can load arbitrary (possibly directed)
graphs, with explicit labelling of nodes with atomic propositions. Such labelled
graphs are interpreted as quasi-discrete closure models. Additionally, the tool
can load digital images, that are interpreted as symmetric, grid-shaped graphs,
therefore as quasi-discrete models. More precisely, each pixel is interpreted as
a node of a graph, and atomic propositions are derived from RGB colour
components, whereas connectivity is derived from the union of the relations
between pixels ``have an edge in common'' and ``have a vertex in common'' (in 2
dimensions, this corresponds to the classical \emph{orthodiagonal connectivity},
that is, each non-border pixel is connected to 8 other pixels). The tool
currently supports 2D images, but support of the same formats as {\ttfamily{VoxLogicA}}\xspace{} is
planned. The tool outputs graphs in the graphviz format\footnote{See
\url{https://www.graphviz.org}.}, with labels using atomic propositions, or
colours according to the pixel colours of the input in the case of images.

redpajama_set_name: RedPajamaArXiv