# On Bisimilarity for Polyhedral Models and SLCS

Vincenzo Ciancia, David Gabelaia, Diego Latella, Mieke Massink, Erik Vink

► To cite this version:

Vincenzo Ciancia, David Gabelaia, Diego Latella, Mieke Massink, Erik Vink. On Bisimilarity for Polyhedral Models and SLCS. 43th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2023, Lisbon, Portugal. pp.132-151, 10.1007/978-3-031-35355-0_9. hal-04731935

HAL Id: hal-04731935

https://inria.hal.science/hal-04731935v1

Submitted on 11 Oct 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
<figure><img src="image_2.png" /></figure>

ifip

International Federation for Information Processing

This document is the original author manuscript of a paper submitted to an IFIP
conference proceedings or other IFIP publication by Springer Nature. As such, there
may be some differences in the official published version of the paper. Such
differences, if any, are usually due to reformatting during preparation for publication or
minor corrections made by the author(s) during final proofreading of the publication
manuscript.
# On Bisimilarity for Polyhedral Models and SLCS

Vincenzo Ciancia¹(✉) ID, David Gabelaia² ID, Diego Latella¹ ID,
Mieke Massink¹ ID, and Erik P. de Vink³ ID

¹ Consiglio Nazionale delle Ricerche - ISTI, Pisa, Italy

{Vincenzo.Ciancia,Diego.Latella,Mieke.Massink}@cnr.it

² TSU Razmadze Mathematical Institute, Tbilisi, Georgia

³ Eindhoven University of Technology, Eindhoven, The Netherlands
evink@win.tue.nl

**Abstract.** The notion of bisimilarity plays an important role in concurrency theory. It provides formal support to the idea of processes having “equivalent behaviour” and is a powerful tool for model reduction. Furthermore, bisimilarity typically coincides with logical equivalence of an appropriate modal logic enabling model checking to be applied on reduced models. Recently, notions of bisimilarity have been proposed also for models of space, including those based on polyhedra. The latter are central in many domains of application that exploit mesh processing and typically consist of millions of cells, the basic components of face-poset models, discrete representations of polyhedral models. This paper builds on the *polyhedral semantics* of the Spatial Logic for Closure Spaces (SLCS) for which the geometric spatial model checker *PolyLogicA* has been developed, that is based on face-poset models. We propose a novel notion of spatial bisimilarity for face-poset models, called $\pm$-bisimilarity. We show that it coincides with logical equivalence induced by SLCS on such models. The latter corresponds to logical equivalence with respect to SLCS on polyhedra which, in turn, coincides with simplicial bisimilarity, a notion of bisimilarity for continuous spaces.

**Keywords:** Bisimulation relations · Spatial bisimilarity · Spatial logics · Logical equivalence · Spatial model checking · Polyhedral models

## 1 Introduction

In concurrency theory, the notion of bisimilarity plays an important role. It provides formal support to the idea of processes having “equivalent behaviour”

Research partially supported by MUR projects PRIN 2017FTXR7S, “IT-MaTTerS”, PRIN 2020TL3X8X “T-LADIES”, bilateral project between CNR (Italy) and SRNSFG (Georgia) “Model Checking for Polyhedral Logic” (#CNR-22-010), and European Union - Next Generation EU - Italian MUR project PNRR PRI ECS00000017 PRR.AP008.003 “THE - Tuscany Health Ecosystem”. The authors are listed in alphabetical order, as they equally contributed to the work presented in this paper.
and is a powerful tool for model reduction. Furthermore, bisimilarity often coincides with logical equivalence of appropriate modal logics enabling techniques for enhancing model checking [32, 33, 43]. Recently, notions of bisimilarity have been proposed also for models of space [11, 19], including polyhedral models [12].

In this work we are following a *topological* approach to spatial logic. This approach has its origin in the early ideas by McKinsey and Tarski [42], who gave a topological interpretation of the “necessarily” operator of the S4 modal logic. The approach was extended to consider *Closure Spaces* (CS) [50], a generalisation of topological spaces, covering also discrete spaces such as general graphs, following work by Galton [29, 30] and Smyth and Webster [47], among others. Recent work by Ciancia et al. (see [24, 25]) builds on these theoretical developments using CSs, or better, *Closure Models* (CMs), as the underlying framework for the *Spatial Logic for Closure Spaces* (SLCS). A closure model is composed of a CS together with a valuation function mapping every atomic proposition letter *p* of a given set into the set of points in the space satisfying *p*. A spatio-temporal model checker, *topochecker* [22], has been developed for the subclass of finite closure spaces. Spatial and spatio-temporal logics and related model checking tools have been used in several application domains such as collective and distributed systems [5, 20, 26, 41, 45, 48]. Moreover, the spatial model-checker *VoxLogicA*<fnref n="1" /> [10] has been developed, that is optimised for digital 2D and 3D images, interpreted as a special case of finite closure spaces, and has been applied successfully in the area of medical imaging [7–10].

However, for the 2D and 3D visualisation of continuous spatial objects, both in medical imaging and virtual reality, polyhedral models of *continuous* space are often used. Such spatial models consist of a suitable splitting of the image of an object into areas of different size, known as *meshes*. These include triangular surface meshes or tetrahedral volume meshes (see for example [37]). In [12], an interpretation of *SLCS* on polyhedral models has been defined along with a novel notion of bisimilarity for such models, namely *simplicial bisimilarity*. Moreover, the theoretical foundations have been developed for polyhedral model checking, including a global model checking algorithm for *SLCS* and its implementation in the *PolyLogicA* (see footnote 1) tool. A visualiser for models and model checking results has been developed as well. Figure 1 provides an example of the use of polyhedral model checking to visualise some part of interest in a 3D tetrahedral volume mesh of a maze composed of 147,245 cells. A cell (see Fig. 2) is the basic element of the face-poset model, a discrete representation of a polyhedral model. In [12], also a relational interpretation of *SLCS* on face-poset models has been proposed and it has been shown that the mapping of polyhedral models to face-poset models preserves and reflects the logic. Figure 1b highlights the result of polyhedral *SLCS* model checking for a set of spatial reachability properties, for the maze in Fig. 1a, characterising those white rooms and their connecting gray corridors, from which both a red and a green room can be reached, without passing by black rooms. For details on the property specification and model checking experiments see [12].

<footnote n="1">¹ Available from the *VoxLogicA* repository at https://github.com/vincenzoml/VoxLogicA.</footnote>
It should be pointed out that, often, images consist of a very large number of cells—much larger than in the example mentioned above—typically several millions or more.

*Contribution.* The main contribution of the present paper is the development of a novel notion of spatial bisimulation, namely ±-bisimilarity on face-poset models representing polyhedral models. We show that two cells are logically equivalent according to the relational interpretation of SLCS (see [12]) if and only if they are ±-bisimilar. A direct consequence of this result is that two points in a polyhedral model are logically equivalent if and only if the unique cells they belong to are ±-bisimilar in the face-poset model. This result paves the way to face-poset model reduction based on ±-bisimilarity, while preserving the SLCS properties of the polyhedral models they represent. We illustrate this by means of a running example of a polyhedral model and the reduction of its discrete representation modulo ±-bisimilarity (see Figs. 3, 4, 5 and 8). As a corollary, we note that two points in a polyhedral model are simplicial bisimilar if and only if their corresponding cells in the face-poset are ±-bisimilar. These results also show how suitable adaptations of notions and results that constitute a flourishing area of research in the field of concurrency theory can be exploited in other domains as well, including theories of space and spatially distributed systems. All in all, our results allow for model-checking of SLCS formulas on a continuous spatial model by conducting actual computations on the minimal face-poset representation.

*Further Related Work.* In the domain of geographic information systems (GIS) simplicial complexes are used as an efficient data structure to store large geospatial data sets [14] in 2D or 3D. They also form the core of several important tools in this domain such as the GeoToolKit [6]. Polyhedral model checking techniques

<figure><img src="image_3.png" /><figcaption>**Fig. 1.** (a) 3D maze with green, white and black rooms, and one red room somewhere in the middle. (b) Polyhedral model checking result highlighting white rooms and their connecting grey corridors from which both a red and a green room can be reached without passing by black rooms. Source [12]. (Color figure online)</figcaption></figure>
could potentially enrich the spatial query languages that are currently used in
this database-oriented domain.

Polyhedra are also used in the theoretical foundations of real-time and hybrid
model checking (see for example [3, 4, 13, 35, 36] and references therein). In that
context polyhedra, and their related notions such as template polyhedra [13, 46]
and zonotopes [31], are obtained from sets of linear inequalities involving real-
time constraints on system behaviour and are a natural representation of sets
of states of such systems. However, in the present paper we focus on spatial
properties of continuous space rather than on behavioural properties of systems.

In [34], coalgebraic bisimilarity has been developed for a general kind of
models, generalising the topological ones, known as Neighbourhood Frames. To
the best of our knowledge, the notions of path and reachability are not part of
that framework (that is, bisimilarity in neighbourhood semantics is based on a
one-step relation rather than on paths), thus the results therein, although more
general than the theory of CSs, cannot be directly reused in the setting of our
current work. In [38,39] the spatial logic SLCS is studied from a model-theoretic
perspective. In particular, in [38] the authors focus on issues of expressivity of
SLCS in relation to topological connectedness and separation. In [39] it is shown
that the logic admits finite models for quasi-discrete neighbourhood models, but
it does not do it for general neighbourhood models. The work in [40] introduces
bisimulation relations that characterise spatial logics with reachability in sim-
plicial complexes. It uses SLCS, but with different simplex semantics.

Spatial logics have also been proposed to describe situations in which modal
operators are interpreted syntactically against the structure of agents in a process
calculus. Some classical examples can be found in [16,17]. A recent example
following such an approach is given in [49]. It concerns model checking of security
aspects in cyber-physical systems, in a spatial context based on the idea of
bigraphical reactive systems introduced by Milner [44].

The work on *spatial model checking* for logics with reachability originated
in [24] and was further developed in [25], which includes also a comparison to
the work of Aiello on spatial *until* operators (see e.g. [1]). In [2], Aiello envisaged
practical applications of topological logics with an *until* operator to minimisation
of images. Recent work in [19,27] builds on—and extends—that vision, taking
CoPa-bisimilarity as a suitable equivalence for spatial minimisation.

## 2 Background and Notation

We first introduce some background concepts and related notation. For a function $f : X \rightarrow Y$, and subsets $A \subseteq X$ and $B \subseteq Y$, we define $f(A)$ and $f^{-1}(B)$ as $\{f(a) | a \in A\}$ and $\{a | f(a) \in B\}$, respectively. The restriction of $f$ on $A$ is denoted by $f|A$. The set of natural numbers and that of real numbers are denoted by $\mathbb{N}$ and $\mathbb{R}$, respectively. We use the standard interval notation: for $x, y \in \mathbb{R}$ we let $[x, y]$ be the set $\{r \in \mathbb{R} | x \leq r \leq y\}$, $[x, y) = \{r \in \mathbb{R} | x \leq r < y\}$ and so on, where $[x, y]$ is equipped with the Euclidean topology inherited from $\mathbb{R}$. We use a similar notation for intervals over $\mathbb{N}$: for $n, m \in \mathbb{N}$ [$m; n$] denotes
<figure><img src="image_4.png" /><figcaption>**Fig. 2.** (a) A simplicial complex (actually a simplex itself). (b) Decomposed into its simplexes as faces. (c) Partitioned into its cells. (d) A triangular surface mesh of a dolphin [18].</figcaption></figure>

the set {$i \in \mathbb{N} | m \le i \le n$}, $[m; n)$ denotes the set {$i \in \mathbb{N} | m \le i < n$}, and similarly for $(m; n]$ and $(m; n)$.

In the remainder of this section, we recall the main results concerning the interpretation of SLCS on polyhedral models. The interested reader is referred to [12] for a detailed treatment of the subject. Section 2.1 below recalls the basic notions of simplex, simplicial complex and polyhedral model. Then, in Sect. 2.2 simplicial bisimilarity and the SLCS interpretation on polyhedral models are briefly reviewed as well as their relationship. The discrete representation of polyhedral models in terms of face-poset models and the SLCS interpretation on the latter is recalled in Sect. 2.3 where their formal relationship is also shown.

## 2.1 Simplex, Simplicial Complexes and Polyhedra

The notions of simplex, simplicial complex and polyhedron form the basis for geometrical reasoning in a finite setting, amenable to polyhedral model-checking and related techniques. A simplex is the convex hull of a set of affinely independent points<fnref n="2" />, namely the vertices of the simplex.

**Definition 1 (Simplex).** A simplex $\sigma$ of dimension $d$ is the convex hull of a finite set $\{v_0, \dots, v_d\} \subseteq \mathbb{R}^m$ of $d+1$ affinely independent points, i.e. $\sigma = \{\lambda_0 v_0 + \dots + \lambda_d v_d | \lambda_0, \dots, \lambda_d \in [0, 1] \text{ and } \sum_{i=0}^d \lambda_i = 1\}$. •

Note that a simplex is a subset of the ambient space $\mathbb{R}^m$ and so it inherits its topological structure. Given a simplex $\sigma$ with vertices $v_0, \dots, v_d$, any subset of $\{v_0, \dots, v_d\}$ spans a simplex $\sigma'$ in turn: we say that $\sigma'$ is a face of $\sigma$, written $\sigma' \subseteq \sigma$. Clearly, $\subseteq$ is a partial order relation.

The relative interior of a simplex plays a similar role as the notion of “interior” in topology and is defined as follows:

**Definition 2 (Relative Interior of a Simplex).** Given a simplex $\sigma$ with vertices $\{v_0, \dots, v_d\}$ the relative interior $\tilde{\sigma}$ of $\sigma$ is the set $\{\lambda_0 v_0 + \dots + \lambda_d v_d | \lambda_0, \dots, \lambda_d \in (0, 1] \text{ and } \sum_{i=0}^d \lambda_i = 1\}$. •

<footnote n="2">² $v_0, \dots, v_d$ are affinely independent if $v_1 - v_0, \dots, v_d - v_0$ are linearly independent. In particular, this condition implies that $d \le m$.</footnote>
We write $\tilde{\sigma}' \preceq \tilde{\sigma}$ whenever $\sigma' \sqsubseteq \sigma$, noting that $\preceq$ is a partial order as well and that $\tilde{\sigma}' \preceq \tilde{\sigma}$ if and only if $\tilde{\sigma}'$ is included in the topological closure of $\tilde{\sigma}$.

The notion of simplicial complex builds upon that of simplex and is the fundamental tool for constructing complex geometrical objects as sets of points in $\mathbb{R}^m$, namely polyhedra, out of simplexes.

**Definition 3 (Simplicial Complex and Polyhedron).** A simplicial complex $K$ is a finite collection of simplexes of $\mathbb{R}^m$ such that: (i) if $\sigma \in K$ and $\sigma' \sqsubseteq \sigma$ then also $\sigma' \in K$; (ii) if $\sigma, \sigma' \in K$ then $\sigma \cap \sigma' \sqsubseteq \sigma$ and $\sigma \cap \sigma' \sqsubseteq \sigma'$. The polyhedron $|K|$ of $K$ is the set-theoretic union of the simplexes in $K$. •

Relations $\sqsubseteq$ and $\preceq$ on simplexes are inherited by simplicial complexes: relation $\sqsubseteq$ on simplicial complex $K$ is the union of the face relations on the simplexes composing $K$, and similarly for $\preceq$. Note that different simplicial complexes can give rise to the same polyhedron and that the set $\tilde{K} = \{\tilde{\sigma} | \sigma \in K \setminus \{\emptyset\}\}$ of non-empty relative interiors of the simplexes of a simplicial complex $K$ forms a partition of polyhedron $|K|$. The elements of $\tilde{K}$ are called *cells* and $(\tilde{K}, \preceq)$ is the face-poset of $K$. Note that, by definition of partition, each $x \in |K|$ belongs to a unique cell in the face-poset. We recall that the polyhedron $|K|$ is a subset of the ambient space $\mathbb{R}^m$ and so inherits its topological structure.

*Example.* Figure 2 shows a triangle as an example of a simplicial complex, and its simplexes in the face relation. The triangle can be partitioned into 7 cells (see Fig. 2c): its interior (ABC, an open triangle), three open segments (AB, BC, AC, the sides without endpoints) and the three vertices (A, B, C). Each vertex is a face of two open segments (and of the open triangle itself), and each open segment is a face of the open triangle. The figure shows also a small example of a triangular surface mesh of a dolphin (Fig. 2d).

Paths play a fundamental role in the definition of SLCS and are defined below:

**Definition 4 (Topological and Simplicial Path).** A topological path in a topological space $P$ is a total, continuous function $\pi : [0, 1] \to P$. Given a polyhedron $|K|$, a topological path $\pi : [0, 1] \to |K|$ is simplicial if and only if there is a finite sequence $r_0 = 0 < \dots < r_n = 1$ of values in $[0, 1]$ and cells $\tilde{\sigma}_1, \dots, \tilde{\sigma}_n \in \tilde{K}$ such that, for all $i = 1, \dots, n$, we have $\pi((r_{i-1}, r_i)) \subseteq \tilde{\sigma}_i$. •

In the polyhedral semantics of SLCS proposed in [12], all the points of a polyhedral model that belong to the same cell are required to satisfy the same set of atomic proposition letters. This is reflected in the definition below:

**Definition 5 (Polyhedral Model).** For simplicial complex $K$ and set of proposition letters $\mathbf{AP}$, a polyhedral model is a pair $(|K|, V)$ where $V : \mathbf{AP} \to \mathcal{P}(|K|)$ is a valuation function such that, for all $p \in \mathbf{AP}$, $V(p)$ is a union of cells in $\tilde{K}$. •

## 2.2 Simplicial Bisimulation and SLCS on Polyhedral Models

The notion of simplicial bisimilarity for polyhedra is central in the theory of the polyhedral interpretation of SLCS, together with Theorem 1 below [12]. Simplicial
<figure><img src="image_5.png" /><figcaption>**Fig. 3.** An example of simplicial bisimilarity. Adapted from [12]. (Color figure online)</figcaption></figure>

bisimilarity is based on the notion of topological paths and is recalled below as well. The use of paths is reminiscent to the definition of stuttering equivalence for Kripke structures or branching bisimilarity for process calculi [15, 28, 33]. However, here, the notion is cast in the setting of continuous space.

**Definition 6 (Simplicial Bisimulation).** Given a Polyhedral Model $\mathcal{X} = (|K|, V)$, a symmetric binary relation $B \subseteq |K| \times |K|$ is a simplicial bisimulation if, for all $x_1, x_2 \in |K|$, $B(x_1, x_2)$ implies the following:

1. $V^{-1}(\{x_1\}) = V^{-1}(\{x_2\})$;

2. for each simplicial path $\pi_1$ with $\pi_1(0) = x_1$ there is a simplicial path $\pi_2$ with $\pi_2(0) = x_2$ such that $B(\pi_1(t), \pi_2(t))$ for all $t \in [0, 1]$; •

In [12] it has been shown that, for any given polyhedral model the largest simplicial bisimulation exists. We call it *Simplicial Bisimilarity* and we write $x_1 \sim x_2$ whenever $x_1$ and $x_2$ are simplicial bisimilar.

*Example.* Figure 3 illustrates simplicial bisimilarity. Figure 3a shows a polyhedral model composed of four triangles forming two adjacent squares. Atomic proposition letters are represented by colours (e.g. red points satisfy **red**, green points satisfy **green** etc.). Figure 3b shows the nine equivalence classes induced by simplicial bisimilarity in the polyhedral model of Fig. 3a. Different classes are shown using different colours.<fnref n="3" /> From the figure it is clear that, for instance, no point, call it $x_1$, in the yellow class (i.e. open segment *CD*) is bisimilar to any point, call it $x_2$, in the cyan class. This is because there are simplicial paths $\pi_1$ starting from $x_1$ that *immediately* enter the green area of Fig. 3a (i.e. $V^{-1}(\pi_1(\varepsilon)) = \textbf{green}$ for any small $\varepsilon > 0$) whereas this is impossible for any simplicial path $\pi_2$ starting from $x_2$ ($V^{-1}(\pi_2(\varepsilon)) = \textbf{red}$ for any small $\varepsilon > 0$ and every such path $\pi_2$). This implies that $B(x_1, x_2)$ for no simplicial bisimulation $B$. In fact, the second condition of Definition 6 would be violated since $B(\pi_1(\varepsilon), \pi_2(\varepsilon))$ cannot hold for $\varepsilon$ as above. Similarly, a simplicial path starting from point *D* (i.e. the only point in the orange) can *immediately* enter the red area of Fig. 3a. On the other hand, no simplicial path starting from any other point satisfying **gray** can do that.

<footnote n="3">³ Note that the colours of the classes have only an illustrative purpose; in particular they have nothing to do with the colours expressing the evaluation function of atomic proposition letters.</footnote>
Note, in particular, that any point in the gray segment *CE* can reach the red area via a simplicial path, but any such path must first go through part of *CE* itself and/or the green area *CDE*. So, also in this case, the second condition of Definition 6 would be violated. Figures 3c and 3d show an example of pairs of simplicial paths that witness $x \sim y$.

The following definition introduces the variant of SLCS for polyhedral models proposed in [12]. In the present paper, we denote it by SLCS<sub>γ</sub>.

**Definition 7 (SLCS on polyhedral models - SLCS<sub>γ</sub>).* The abstract language of SLCS<sub>γ</sub> is the following: $\Phi ::= p | \neg\Phi | \Phi_1 \wedge \Phi_2 | \gamma(\Phi_1, \Phi_2)$.

The satisfaction relation of SLCS<sub>γ</sub> with respect to a given polyhedral model $\mathcal{X} = (|K|, V)$, SLCS<sub>γ</sub> formula $\Phi$, and $x \in |K|$ is defined recursively on the structure of $\Phi$ as follows:

$$ 
\begin{array}{l@{\qquad}l}
\mathcal{X}, x \models p & \Leftrightarrow x \in V(p); \\
\mathcal{X}, x \models \neg\Phi & \Leftrightarrow \mathcal{X}, x \models \Phi \text{ does not hold;} \\
\mathcal{X}, x \models \Phi_1 \wedge \Phi_2 & \Leftrightarrow \mathcal{X}, x \models \Phi_1 \text{ and } \mathcal{X}, x \models \Phi_2; \\
\mathcal{X}, x \models \gamma(\Phi_1, \Phi_2) & \Leftrightarrow \text{a topological path } \pi : [0, 1] \to |K| \text{ exists such that } \pi(0) = x, \\
& \phantom{\Leftrightarrow} \mathcal{X}, \pi(1) \models \Phi_2, \text{ and } \mathcal{X}, \pi(r) \models \Phi_1 \text{ for all } r \in (0, 1).
\end{array}
$$

•

Note that the above definition generalises the classical topological interpretation of the □ modality as interior. In fact, □Φ is equivalent to ¬γ(¬Φ, true) (see [12]).

*Example.* Again with reference to model $\mathcal{X}$ of Fig. 3a, it is easy to see that any point in the yellow class satisfies, for instance, $\gamma(\text{green}, true)$, and also $\gamma(\text{green}, red)$ and $red \wedge \gamma(\text{green}, red)$.

**Definition 8 (SLCS<sub>γ</sub> Logical Equivalence).** Given Polyhedral Model $\mathcal{X} = (|K|, V)$ and $x_1, x_2 \in |K|$ we say that $x_1$ and $x_2$ are logically equivalent with respect to SLCS<sub>γ</sub>, written $x_1 \cong_{SLCS_\gamma} x_2$, if and only if, for all SLCS<sub>γ</sub> formulas $\Phi$ the following holds: $\mathcal{M}(\mathcal{X}), x_1 \models \Phi$ if and only if $\mathcal{M}(\mathcal{X}), x_2 \models \Phi$. •

Logical equivalence coincides with simplicial bisimilarity [12]:

**Theorem 1 (Corollary 6.5 of [12]).** Given Polyhedral Model $\mathcal{X} = (|K|, V)$, $x_1, x_2 \in |K|$ the following holds: $x_1 \cong_{SLCS_\gamma} x_2$ if and only if $x_1 \sim x_2$. □

## 2.3 Face-Poset Models and SLCS

The following definition characterises the discrete representation of polyhedral models we will use in the rest of the paper (see Fig. 4).

**Definition 9 (face-poset model).** Given Polyhedral Model $\mathcal{X} = (|K|, V)$, the face-poset model $\mathcal{M}(\mathcal{X})$ is the Kripke model $(W, \leq, \mathcal{V})$ where $(W, \leq) = (\tilde{K}, \leq)$ is the face-poset of $K$ and $\tilde{\sigma} \in \mathcal{V}(p)$ if and only if $\tilde{\sigma} \subseteq V(p)$. •
Below, we recall the definition of ±-paths introduced in [12]. They faithfully represent, in the face-poset model, topological paths in the polyhedral one. Consider, for instance, the polyhedron consisting of a segment from a given point P to a point Q and its related face-poset. A path starting from, say, point P can “immediately enter” the open segment PQ, whereas a path starting from a point within the open segment cannot “immediately proceed” to P (nor to Q); it has to first traverse a fraction of the open segment PQ, then ending in P (or Q). This is reflected in the face-poset by requiring that a path therein, i.e. a ±-path, cannot perform a first step going against the partial order (going “down”), whereas in its last step it cannot follow strictly the partial order (going “up”).

**Definition 10 (±-path).** Let $\mathcal{M}(\mathcal{X}) = (W, \preceq, \mathcal{V})$ be a finite face-poset model and let $\preceq^{\pm}$ be the relation $\preceq \cup \preceq^{\pm}$. We say that, for $\ell \in \mathbb{N}$, sequence $\pi : [0; \ell] \to W$ is a ±-path (and we indicate it by $\pi : [0; \ell] \stackrel{\pm}{\to} W$) if $\ell \ge 2$ and the following holds: $\pi(0) \preceq^{\pm} \pi(1) \preceq^{\pm} \pi(2) \preceq^{\pm} \dots \preceq^{\pm} \pi(\ell - 1) \succeq^{\pm} \pi(\ell)$. •

The following definition re-interprets SLCS on finite face-posets and is based on ±-paths [12]. In order to avoid confusion, in the sequel, we will call the resulting logic SLCS$_{±}$.

**Definition 11 (SLCS on finite face-posets - SLCS$_{±}$).** The satisfaction relation of SLCS$_{±}$ with respect to a given finite face-poset model $\mathcal{M}(\mathcal{X}) = (W, \preceq, \mathcal{V})$, SLCS$_{±}$ formula $\Phi$, and $w \in W$ is defined recursively on the structure of $\Phi$:

$$ 
\begin{align*}
\mathcal{M}(\mathcal{X}), w \models p &\Leftrightarrow w \in \mathcal{V}(p); \\
\mathcal{M}(\mathcal{X}), w \models \neg \Phi &\Leftrightarrow \mathcal{M}(\mathcal{X}), w \models \Phi \text{ does not hold;} \\
\mathcal{M}(\mathcal{X}), w \models \Phi_1 \wedge \Phi_2 &\Leftrightarrow \mathcal{M}(\mathcal{X}), w \models \Phi_1 \text{ and } \mathcal{M}(\mathcal{X}), w \models \Phi_2; \\
\mathcal{M}(\mathcal{X}), w \models \gamma(\Phi_1, \Phi_2) &\Leftrightarrow 
\begin{aligned}[t]
& a \text{ ±-path } \pi : [0; \ell] \stackrel{\pm}{\to} W \text{ exists such that } \pi(0) = w, \\
& \mathcal{M}(\mathcal{X}), \pi(\ell) \models \Phi_2, \text{ and} \\
& \mathcal{M}(\mathcal{X}), \pi(i) \models \Phi_1 \text{ for all } i \in (0; \ell).
\end{aligned}
\end{align*}
$$

**Definition 12 (Logical Equivalence).** Given finite face-poset model $\mathcal{M}(\mathcal{X}) = (W, \preceq, \mathcal{V})$ and $w_1, w_2 \in W$ we say that $w_1$ and $w_2$ are logically equivalent with respect to SLCS$_{±}$, written $w_1 \simeq_{SLCS_{±}} w_2$ if and only if, for all SLCS$_{±}$ formulas $\Phi$ the following holds: $\mathcal{M}(\mathcal{X}), w_1 \models \Phi$ if and only if $\mathcal{M}(\mathcal{X}), w_2 \models \Phi$. •

A fundamental result, see [12], follows, where with slight overloading, for $x \in |K|$, we let $\mathcal{M}(x)$ denote the unique cell $\tilde{\sigma} \in \tilde{K}$ such that $x \in \tilde{\sigma}$ (see Fig. 4 for an illustration).

*Example.* With reference to the face-poset model $\mathcal{M}(\mathcal{X})$ of Fig. 4b for polyhedral model $\mathcal{X}$ of Fig. 3a, it is easy to see that cells C and CD satisfy $\gamma(\text{green}, \text{true})$, and also $\gamma(\text{green}, \text{red})$ and $\text{red} \wedge \gamma(\text{green}, \text{red})$.

**Theorem 2 (Theorem 4.4 of [12]).** Let $\mathcal{X} = (|K|, \mathcal{V})$ a polyhedral model and $\mathcal{M}(\mathcal{X})$ the associated face-poset model as by Definition 9. For all $x \in |K|$ and formula $\Phi$ the following holds: $\mathcal{X}, x \models \Phi$ if and only if $\mathcal{M}(\mathcal{X}), \mathcal{M}(x) \models \Phi$. □
<figure><img src="image_6.png" /></figure>

<figure><img src="image_7.png" /><figcaption>**Fig. 4.** (a) A polyhedral model $\mathcal{X}$ with atomic propositions red, green and gray, and a path from a point $x$ to vertex $D$. (b) Hasse diagram of face-poset model $\mathcal{M}(\mathcal{X})$ and a path (in blue) corresponding to the path in $\mathcal{X}$. (Color figure online)</figcaption></figure>

We close this section with the definition of some notation for sequences, which $\pm$-paths are a particular case of, and that will be useful in the rest of the paper.

**Definition 13 (Sequences).** Given a set $X$, a sequence over $X$ from $x$, of length $\ell \in \mathbb{N}$, is a total function $s: [0; \ell] \to X$ such that $s(0) = x$. For sequence $s$ of length $\ell$, we often use the notation $(x_i)_{i=0}^{\ell}$ where $x_i = s(i)$ for $i \in [0; \ell]$. Given sequences $s' = (x'_i)_{i=0}^{\ell'}$ and $s'' = (x''_i)_{i=0}^{\ell''}$, with $x'_{\ell'} = x''_0$, the sequentialisation $s' \cdot s'' : [0; \ell' + \ell''] \to X$ of $s'$ with $s''$ is the sequence from $x'_0$ defined as follows:

$$ (s' \cdot s'')(i) = \begin{cases} s'(i), & \text{if } i \in [0; \ell'], \\ s''(i - \ell'), & \text{if } i \in [\ell'; \ell' + \ell''] \end{cases} $$

For sequence $s = (x_i)_{i=0}^n$ and $k \in [0; n]$ we define the $k$-shift operator $\uparrow^k$ as follows: $s\uparrow^k = (x_{j+k})_{j=0}^{n-k}$ and, for $0 < m \le n$, we let $s \leftarrow m$ denote the sequence obtained from $s$ by inserting a copy of $s(m)$ immediately before $s(m)$ itself, i.e. $s \leftarrow m = (s[0; m]) \cdot ((s(m), s(m)), (s\uparrow^m))$. Finally, a (non-empty) prefix of $s$ is a sequence $s[0; k]$, for some $k \in [0; n]$. •

For example, for sequence $(a, b, c)$ of length 2 and sequence $(c, d)$ of length 1, we have $(a, b, c) \cdot (c, d) = (a, b, c, d)$, of length 3, $(a) \cdot (a, b) = (a, b)$, $(a) \cdot (a) = (a)$. Note the difference between sequentialisation and concatenation ‘++’: for instance, $(a, b)++(c) = (a, b, c)$ whereas $(a, b) \cdot (c)$ is undefined since $b \ne c$, $(a)++(a)$ is $(a, a)$ whereas $(a) \cdot (a) = (a)$. We have $(a, b, c)\uparrow 1 = (b, c)$ and $(a, b, c)\uparrow 2 = (c)$ while $(a, b, c)\leftarrow 1 = (a, b, b, c)$. Sequences $(a), (a, b), (a, b, c)$ are all the (non-empty) prefixes of $(a, b, c)$.

## 3 $\pm$-Bisimilarity and the Coincidence Result

In this section, we present the novel notion of $\pm$-bisimulation, that is based on the notion of $\pm$-path compatibility, inspired by compatibility of paths in quasi-discrete closure models introduced in [27]. We additionally show that $\pm$-bisimilarity coincides with logical equivalence for SLCS$\pm$.

**Definition 14 ($\pm$-path compatibility).** Given face-poset model $\mathcal{M}(\mathcal{X}) = (W, \leq, \mathcal{V})$ and binary relation $B \subseteq W \times W$, two $\pm$-paths $\pi_1 = (w'_i)_{i=0}^{k_1}$, $\pi_2 = (w''_i)_{i=0}^{k_2}$
$(w_j'')^{k_2}_{j=0}$ are called compatible with respect to $B$ in $\mathcal{M}(\mathcal{X})$ if, for some $N > 0$, two total monotone non-decreasing surjections $z_1 : [0; k_1] \to [1; N]$ and $z_2 : [0; k_2] \to [1; N]$ exist such that $z_1(1) = z_2(1)$, $z_1(k_1 - 1) = z_2(k_2 - 1)$ and $B(w'_i, w''_j)$ for all indices $i \in [0; k_1]$ and $j \in [0; k_2]$ satisfying $z_1(i) = z_2(j)$. •

The functions $z_1$ and $z_2$ are referred to as matching functions. Note that both the number $N$ and functions $z_1$ and $z_2$ need not be unique. The minimal number $N > 0$ for which matching functions exist is defined to be the number of zones of the two $\pm$-paths $\pi_1$ and $\pi_2$. It is easy to see that, whenever two $\pm$-paths are compatible, for any pair of matching function $z_1$ and $z_2$ the following holds, by virtue of monotonicity and surjectivity: $z_1(0) = z_2(0) = 1$ and $z_1(k_1) = z_2(k_2) = N$. Hence $B(w'_0, w''_0)$ and $B(w'_{k_1}, w''_{k_2})$, and of course $B(w'_1, w''_1)$ and $B(w'_{k_1-1}, w''_{k_2-1})$.

Given binary relation $B \subseteq W \times W$, compatibility of $\pm$-paths with respect to $B$ is a binary relation over $\pm$-paths. We write $\pi_1 \text{ comp}^B \pi_2$ whenever $\pm$-paths $\pi_1$ and $\pi_2$ are compatible with respect to $B$. Lemma 1 below, proved in [21], states some properties of $\pm$-paths compatibility that turn useful in the sequel.

**Lemma 1.** Let $\mathcal{M}(\mathcal{X}) = (W, \leq, \mathcal{V})$ be a face-poset, $B \subseteq W \times W$ a relation, $\pi, \pi_1, \pi_2$ $\pm$-paths with $\pi$ of length $\ell > 0$, $s_1 : [0; \ell_1] \to W$, $s_2 : [0; \ell_2] \to W$ sequences of length $\ell_1, \ell_2 \in \mathbb{N}$ respectively, $m \in (0; \ell)$. The following holds:

1. $\pi \text{ comp}^B(\pi \leftarrow m)$.

2. If $B$ is an equivalence relation, then:

(a) so is $\text{comp}^B$, and

(b) the sequentialisation of two sequences of equivalent elements, and non-decreasing first step, with two compatible $\pm$-paths results in compatible $\pm$-paths. Formally: if $\pi_1 \text{ comp}^B \pi_2$, $s_h(0) \leq s_h(1)$ and $s_h(\ell_h) = \pi_h(0)$ for $h \in [1; 2]$, with $B(s_1(i), s_2(j))$ for all $i \in [0; \ell_1)$ and $j \in [0; \ell_2)$, then $s_1 \cdot \pi_1$ and $s_2 \cdot \pi_2$ are $\pm$-paths that are compatible with respect to $B$.

**Definition 15.** ($\pm$-bisimulation). Let $\mathcal{M}(\mathcal{X}) = (W, R, \mathcal{V})$ be a finite face-poset model. A symmetric binary relation $B \subseteq W \times W$ is a poset $\pm$-bisimulation if, for all $w_1, w_2 \in W$, if $B(w_1, w_2)$ then the following holds:

1. $\mathcal{V}^{-1}(\{w_1\}) = \mathcal{V}^{-1}(\{w_2\})$;

2. for each $\pm$-path $\pi_1$ from $w_1$ there is a $\pm$-path $\pi_2$ from $w_2$ such that $\pi_1 \text{ comp}^B \pi_2$.

We say that $w_1$ and $w_2$ are $\pm$-bisimilar, written $w_1 \rightleftharpoons_{\pm} w_2$, if there is a $\pm$-bisimulation $B$ such that $B(w_1, w_2)$. •

*Example.* With reference to the polyhedral model $\mathcal{X}$ of Fig. 3a, in Fig. 5b the $\pm$-bisimilarity equivalence classes are shown in different colours for $\mathcal{M}(\mathcal{X})$. In Fig. 5a we recall the simplicial bisimilarity quotient of model $\mathcal{X}$. There is no $\pm$-path starting from any of the cells in the cyan class that is compatible with $\pm$-path $\pi_{CD} = (CD, CDE, CDE)$ from cell $CD$ in the yellow class as it is easy to see in Fig. 4b. The same applies for $\pm$-path $\pi_C = (C, CDE, CDE)$ from cell
$C.^4$ Similarly, let us consider cell $D$. We have already seen that there is no other point in the polyhedral model that is simplicial bisimilar to point $D$. Let us consider $\pm$-path $\pi_D = (D, CD, CD)$. In the sequel we show there cannot be any $\pm$-path from any other cell satisfying **gray** that is compatible with $\pi_D$. In fact, any other such a $\pm$-path $\pi$ should be such that $\pi(1)$ satisfies **red** (this is required by the fact that $z_D(1) = z(1)$ for any pair of matching functions for $\pi_D$ and $\pi$) and $\pi(j)$ should not satisfy **green** for any $j$ (since no element of $\pi_D$ satisfies **green**). On the other hand, any $\pm$-path $\pi'$ starting from any other cell satisfying **gray** and reaching a cell satisfying **red** is such that $\pi'(1)$ does not satisfy **red**. Furthermore, many such $\pm$-paths have an element that satisfies **green**. Thus, there is no $\pm$-path starting from any other **gray** cell that is compatible with $(D, CD, CD)$ and $D$ is in fact in a different class than any other **gray** cell.

<figure><img src="image_8.png" /></figure>

<figure><img src="image_9.png" /><figcaption>**Fig. 5.** Equivalence classes of the polyhedral model of Fig. 3a w.r.t. simplicial bisimilarity (a) and those of its face-poset model w.r.t. $\pm$-bisimilarity (b).</figcaption></figure>

We are now in a position to state and prove the two main technical results of this paper, viz. soundness of $\pm$-bisimilarity—Theorem 3—and the fact that logical equivalence is a $\pm$-bisimulation—Theorem 4.

**Theorem 3.** For $w_1, w_2$ in finite face-poset model $\mathcal{M}(\mathcal{X})$, the following holds: if $w_1 \stackrel{\pm}{\Rightarrow} w_2$ then $w_1 \simeq_{\text{SLCS}_{\pm}} w_2$.

*Proof.* Let $\mathcal{M}(\mathcal{X}) = (W, \leq, \mathcal{V})$ be a face-poset model. We proceed by induction on the structure of $\Phi$ in $\text{SLCS}_{\pm}$. We only cover the case $\gamma(\Phi_1, \Phi_2)$ since the others are straightforward. Let $w_1$ and $w_2$ be two points of $\mathcal{M}(\mathcal{X})$ such that $w_1 \stackrel{\pm}{=} w_2$. Suppose $w_1 \models \gamma(\Phi_1, \Phi_2)$. Let $\pi_1 = (w'_i)_{i=0}^{k_1}$ be a $\pm$-path from $w_1$ satisfying $\pi_1(k_1) \models \Phi_2$ and $\pi_1(i) \models \Phi_1$ for all $i \in (0; k_1)$. Since $w_1 \stackrel{\pm}{=} w_2$, a $\pm$-path $\pi_2 = (w''_i)_{i=0}^{k_2}$ from $w_2$ exists that is compatible with $\pi_1$ with respect to $\stackrel{\pm}{=}$. Let, for appropriate $N > 0$, $z_1 : [0; k_1] \to [1; N]$ and $z_2 : [0; k_2] \to [1; N]$ be matching functions for $\pi_1$ and $\pi_2$. Without loss of generality, $z_2^{-1}(\{N\}) = \{k_2\}$.

Since $z_1(k_1) = z_2(k_2) = N$, we have $\pi_1(k_1) \stackrel{\pm}{=} \pi_2(k_2)$. Thus $\pi_2(k_2) \models \Phi_2$ by Induction Hypothesis. Moreover, if $j \in (0; k_2)$, then $z_2(j) < N$ by assumption and there is $i \in (0; k_1)$ such that $z_1(i) = z_2(j)$, that is $\pi_1(i) \stackrel{\pm}{=} \pi_2(j)$.

<footnote n="4">⁴ Recall that partial orders are transitive and reflexive.</footnote>
Since $\pi_1(i) \models \Phi_1$, it follows that $\pi_2(j) \models \Phi_1$ by Induction Hypothesis. Therefore $\pm$-path $\pi_2$ witnesses $w_2 \models \gamma(\Phi_1, \Phi_2)$. $\square$

**Theorem 4.** For finite face-poset model $\mathcal{M}(\mathcal{X})$, $\simeq_{\text{SLCS}_\pm}$ is a $\pm$-bisimulation.

*Proof.* Let $\mathcal{M}(\mathcal{X}) = (W, \leq, \mathcal{V})$ be a finite face-poset model. We check that $\simeq_{\text{SLCS}_\pm}$ satisfies requirement (2) of Definition 15. Requirement (1) is immediate. Let, for points $x, y \in W$, the $\text{SLCS}_\pm$-formula $\delta_{x,y}$ be such that $\delta_{x,y}$ is true if $x \simeq_{\text{SLCS}_\pm} y$, and $x \models \delta_{x,y}$ and $y \models \neg\delta_{x,y}$ if $x \not\simeq_{\text{SLCS}_\pm} y$. Put $\chi(x) = \bigwedge_{y \in W} \delta_{x,y}$. It is easy to see that, for $x, y \in W$, it holds that

$$y \models \chi(x) \text{ if and only if } x \simeq_{\text{SLCS}_\pm} y. \qquad (1)$$

Let $\mathcal{H}$ be the set of all finite sequences $(x_i)_{i=0}^n$ over $\mathcal{M}(\mathcal{X})$. Note that such sequences might not be $\pm$-paths. Furthermore, let function $\text{zones}: \mathcal{H} \to \mathbb{N}$ be such that, for sequence $s = (x_i)_{i=0}^n$,

$$\begin{array}{ll} \text{zones}(s) = 1 & \text{if } n = 0 \\ \text{zones}(s) = \text{zones}(s \uparrow 1) & \text{if } n > 0 \text{ and } x_0 \simeq_{\text{SLCS}_\pm} x_1 \\ \text{zones}(s) = \text{zones}(s \uparrow 1) + 1 & \text{if } n > 0 \text{ and } x_0 \not\simeq_{\text{SLCS}_\pm} x_1 \end{array}$$

A sequence $s$ is said to have $k$ zones, if $\text{zones}(s) = k$.

*Claim.* For all $k \geq 1$, for all $x_1, x_2 \in W$, if $x_1 \simeq_{\text{SLCS}_\pm} x_2$ and $\pi_1$ is a $\pm$-path from $x_1$ and $\pi_1$ has $k$ zones, then a $\pm$-path $\pi_2$ from $x_2$ exists such that $\pi_2$ is compatible with $\pi_1$ with respect to $\simeq_{\text{SLCS}_\pm}$. The claim is proven by induction on $k$.

Base case, $k=1$: If $x_1 \simeq_{\text{SLCS}_\pm} x_2$ and $\pi_1 = (x'_i)_{i=0}^n$ is a $\pm$-path from $x_1$ that has 1 zone only, then $x_1 \simeq_{\text{SLCS}_\pm} x'_i$ for all $i \in [0; n]$. Let $\pi_2$ be the $\pm$-path $(x_2, x_2, x_2)$. Since $x_1 \simeq_{\text{SLCS}_\pm} x_2$, also $x_2 \simeq_{\text{SLCS}_\pm} x'_i$ for all $i \in [0; n]$. Hence, $\pi_2$ is compatible with $\pi_1$ with respect to $\simeq_{\text{SLCS}_\pm}$ with matching functions $z_1(i) = 1$ for all $i \in [0; n]$ and $z_2(j) = 1$ for all $j \in [0; 2]$.

Induction step, $k+1$: Suppose $x_1 \simeq_{\text{SLCS}_\pm} x_2$ and $\pi_1 = (x'_i)_{i=0}^n$ is a $\pm$-path from $x_1$ of $k+1$ zones. Let $m > 0$ be such that $x_1 \simeq_{\text{SLCS}_\pm} x'_i$ for all $i \in [0; m)$ and $x_1 \not\simeq_{\text{SLCS}_\pm} x'_m$. We distinguish two cases:

**Case A:** $m=1$ (Fig. 6 shows an example for $m=1$ and length $n=3$). In this case, it holds that $x_1 \models \gamma(\chi(x'_1), \text{true})$. Since $x_2 \simeq_{\text{SLCS}_\pm} x_1$, we also have $x_2 \models \gamma(\chi(x'_1), \text{true})$. Therefore, a $\pm$-path $\pi'$ exists from $x_2$ such that $\pi'(1) \models \chi(x'_1)$, i.e. $\pi'(1) \simeq_{\text{SLCS}_\pm} x'_1$ by Eq. 1 (Fig. 6a). Let us, first of all, consider the sequence $\pi'_1 = (x'_1, x'_1) \cdot (\pi_1 \uparrow 1)$, obtained by inserting a copy of $x'_1$ before $(\pi_1 \uparrow 1)$ (Fig. 6b and Fig. 6c). Note that $\pi'_1$ is a $\pm$-path of length $n$. In fact, $\pi'_1(0) \preceq \pi'_1(1)$, since $\pi'_1(0) = \pi'_1(1)$ by construction. Furthermore, $\pi'_1(n-1) = \pi_1(n-1) \succeq \pi_1(n) = \pi'_1(n)$, where $\pi_1(n-1) \succeq \pi_1(n)$ because $\pi_1$ is a $\pm$-path. Finally, all the subsequent intermediate elements of $\pi'_1$ are in the $\preceq^\pm$ relation by construction. Moreover, note that $\pi'_1$ has the same number of zones as $\pi_1 \uparrow 1$, that is $k$. So, by the Induction Hypothesis, since $\pi'(1) \simeq_{\text{SLCS}_\pm} x'_1$, there is a $\pm$-path $\pi''$ from $\pi'(1)$ such that $\pi'' \text{comp} \simeq_{\text{SLCS}_\pm} \pi'_1$ (see Fig. 6c). Now, using Lemma 1.2b,
<figure><img src="image_10.png" /><figcaption>**Fig. 6.** Example illustrating the proof of Theorem 4, for $n = 3$, **Case A:** $m = 1$. In the figure, different zones are shown by using different colours, and we assume zones($\pi_1$) = 4. Dotted lines in magenta indicate pairs belonging to $\simeq_{SLCS_{\pm}}$. (Color figure online)</figcaption></figure>

for sequences $\pi'|[0; 1]$ and $\pi_1|[0; 1]$ and $\pm$-paths $\pi''$ and $\pi'_1$ respectively, we get $(\pi'|[0; 1] \cdot \pi'') \mathrm{comp}^{\simeq_{SLCS_{\pm}}} (\pi_1|[0; 1]) \cdot \pi'_1$. Finally, noting that $(\pi_1|[0; 1]) \cdot \pi'_1$ is exactly $\pi_1 \leftarrow 1$ and using Lemma 1.1, we get $(\pi_1|[0; 1]) \cdot \pi'_1 \mathrm{comp}^{\simeq_{SLCS_{\pm}}} \pi_1$. Since $\simeq_{SLCS_{\pm}}$ is an equivalence relation, we finally get, using Lemma 1.2a, $(\pi'|[0; 1] \cdot \pi'') \mathrm{comp}^{\simeq_{SLCS_{\pm}}} \pi_1$ and we choose $\pi_2 = \pi'|[0; 1] \cdot \pi''$ (see Fig. 6d)).

**Case B:** $m > 1$. If $m > 1$ then it holds that $x_1 \models \gamma(\chi(x_1), \chi(x'_m))$. Since, by hypothesis, $x_2 \simeq_{SLCS_{\pm}} x_1$ also $x_2 \models \gamma(\chi(x_1), \chi(x'_m))$. Thus, a $\pm$-path $\pi'$, of some length $\ell \ge 2$, from $x_2$ exists, such that $\pi'(\ell) \models \chi(x'_m)$ and $\pi'(j) \models \chi(x_1)$ for all $j \in (0; \ell)$. We have that $x'_m \simeq_{SLCS_{\pm}} \pi'(\ell)$ and $x_1 \simeq_{SLCS_{\pm}} \pi'(j)$ for all $j \in (0; \ell)$, by Eq. 1. In the sequel, we focus on the case $1 < m < n$. The proof for the case $1 < m = n$ is straightforward and is shown in [21].

Suppose $m > 1$ and $m < n$ (Fig. 7 shows an example for $m = 2$ and $n = 3$).

In a similar way as before, we first consider the sequence $\pi'_1 = (x'_m, x'_m) \cdot (\pi_1 \uparrow m)$ and let $h$ be the length of $\pi'_1$. Note that $\pi'_1$ is a $\pm$-path. In fact $(\pi_1 \uparrow m) = (\dots x'_{n-1}, x'_n)$ has length at least 1—it has at least two elements, because $m < n$ and the length of $(x'_m, x'_m)$ is 1. So, by definition of sequentialisation $\pi'_1$ has length at least 2—it has at least three elements. Moreover $\pi'_1(0) = \pi'_1(1)$ by construction, so $\pi'_1(0) \le \pi'_1(1)$ and $\pi'_1(h-1) = \pi_1(n-1) \ge \pi_1(n) = \pi'_1(h)$, since $\pi_1$ is a $\pm$-path. Finally, all the subsequent intermediate elements of $\pi'_1$ are in the $\leq^{\pm}$ relation by construction. Note, furthermore, that $\pi'_1$ has the same number of zones as $(\pi_1 \uparrow m)$, namely $k$. So, by the Induction Hypothesis, since $\pi'(\ell) \simeq_{SLCS_{\pm}} x'_m$ we know that there is a $\pm$-path $\pi''$ from $\pi'(\ell)$ such that $\pi'' \mathrm{comp}^{\simeq_{SLCS_{\pm}}} \pi'_1$ (see
<figure><img src="image_11.png" /><figcaption>(a)</figcaption></figure>

<figure><img src="image_12.png" /></figure>

<figure><img src="image_13.png" /><figcaption>(c)</figcaption></figure>

<figure><img src="image_14.png" /><figcaption>(d)</figcaption></figure>

**Fig. 7.** Example illustrating the proof of Theorem 4, for $n = 3$, **Case B** and $1 < m < n$. In the figure, different zones are shown by using different colours, and we assume **zones**($\pi_1$) = 3. Dotted lines in magenta indicate pairs that belong to $\simeq_{\text{SLCS}_\pm}$. (Color figure online)

Fig. 7c). Now, using Lemma 1.2b, for sequences $\pi'$ and $\pi_1$|[0; m] and $\pm$-paths $\pi''$ and $\pi'_1$ respectively, we get $(\pi' \cdot \pi'') \text{comp}^{\simeq_{\text{SLCS}_\pm}} (\pi_1|[0; m]) \cdot \pi'_1$. Finally, noting that $(\pi_1|[0; m]) \cdot \pi'_1$ is exactly $\pi_1 \leftarrow m$ and using Lemma 1.1, we get $(\pi_1|[0; m]) \cdot \pi'_1 \text{comp}^{\simeq_{\text{SLCS}_\pm}} \pi_1$. Since $\simeq_{\text{SLCS}_\pm}$ is an equivalence relation, we finally get, using Lemma 1.2a, $\pi' \cdot \pi'' \text{comp}^{\simeq_{\text{SLCS}_\pm}} \pi_1$ and we choose $\pi_2 = \pi' \cdot \pi''$ (see Fig. 7d).

This proves the claim. From the claim it follows immediately that $\simeq_{\text{SLCS}_\pm}$ satisfies the second condition of Definition 15. $\square$

On the basis of Theorem 3 and Theorem 4, we have that the largest $\pm$-bisimulation exists, it is a $\pm$-bisimilarity, it is an equivalence relation, and it coincides with logical equivalence in the face-poset induced by $\text{SLCS}_\pm$:

**Corollary 1.** For every finite face-poset $\mathcal{M}(\mathcal{X}) = (W, \leq, \mathcal{V})$, $w_1, w_2 \in W$, the following holds: $w_1 \iff_{\pm} w_2$ if and only if $w_1 \simeq_{\text{SLCS}_\pm} w_2$. $\square$

In conclusion, recalling that for all $x \in \mathcal{X}$ and $\text{SLCS}_\gamma$ formula $\Phi$, we have that $\mathcal{X}, x \models \Phi$ if and only if $\mathcal{M}(\mathcal{X}), \mathcal{M}(x) \models \Phi$, we get the following final result:

**Corollary 2.** For all polyhedral models $\mathcal{X}, x_1, x_2 \in \mathcal{X}: x_1 \sim x_2$ if and only if $x_1 \simeq_{\text{SLCS}_\gamma} x_2$ if and only if $\mathcal{M}(x_1) \iff_{\pm} \mathcal{M}(x_2)$ if and only if $\mathcal{M}(x_1) \simeq_{\text{SLCS}_\pm} \mathcal{M}(x_2)$. $\square$

*Example.* Figure 8 shows the minimal model $\min(\mathcal{M}(\mathcal{X}))$, modulo $\pm$-bisimilarity, of $\mathcal{M}(\mathcal{X})$ (see Fig. 4b). Model $\min(\mathcal{M}(\mathcal{X}))$ has been obtained in a similar way
<figure><img src="image_15.png" /><figcaption>**Fig. 8.** Hasse diagram of the minimal model, modulo ±-bisimilarity, of the model of Fig. 4b.</figcaption></figure>

as described in Proposition 1 of [23]. Note that the model is transitive and reflexive, because of Corollary 1 above, and the reflexivity and idempotency axioms of topological modal logic. Thus, in Fig. 8 the model is represented by its Hasse diagram. Each element of $min(M(X))$ is coloured according to the atomic proposition satisfied by the members of the corresponding ±-bisimilarity class and its border has the colour of the class (see Fig. 5b). The ±-path (1, 1, 1, 1, 3) in the minimal model corresponds to (AB, ABC, BC, BCD, D) shown in Fig. 4b and (2, 5, 2) witnesses formula red ∧ γ(green, red) in the minimal model.

# 4 Conclusions and Future Work

We have introduced a novel notion of spatial bisimilarity, namely ±-bisimilarity on face-poset models representing polyhedral models. We have shown that it coincides with logical equivalence based on the variant of SLCS proposed in [12]. Consequently, two points in a polyhedral model are simplicial bisimilar if and only if their corresponding cells in the face-poset are ±-bisimilar.

Part of future work will be to investigate the relationship between bisimilarity notions developed for face-poset models, and those developed in the context of closure models, e.g. those studied in [19,27]. Furthermore, we plan to develop slightly weaker notions of ±-bisimilarity, together with their associated spatial logics. Such coarser equivalences are of interest for further model reduction. We will investigate approaches along the lines of the work in [23] for CMs. Finally, the issue of the impact of adding a “converse” operator for $γ$ to the logic— in a similar vein as for other reachability operators, in e.g. [8,19,27]—on the associated bisimilarity and its geometrical interpretation is another subject for future study.

**Acknowledgements.** We thank Nick Bezhanishvili, Gianluca Grilletti and Jan Friso Groote for interesting discussions concerning various aspects of polyhedral model-checking, bisimulations and model reduction techniques.
References

1. Aiello, M.: Spatial reasoning: theory and practice. Ph.D. thesis, Institute of Logic, Language and Computation, University of Amsterdam (2002)

2. Aiello, M.: The topo-approach to spatial representation and reasoning. AIIA NOTIZIE (4) (2003)

3. Alur, R.: Formal verification of hybrid systems. In: Proceedings of the 11th International Conference on Embedded Software, EMSOFT 2011, part of the Seventh Embedded Systems Week, ESWeek 2011, Taipei, Taiwan, 9–14 October 2011, pp. 273–278. ACM (2011). https://doi.org/10.1145/2038642.2038685

4. Alur, R., Giacobbe, M., Henzinger, T.A., Larsen, K.G., Mikučionis, M.: Continuous-time models for system design and analysis. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 452–477. Springer, Cham (2019). https://doi.org/10.1007/978-3-319-91908-9_22

5. Audrito, G., Casadei, R., Damiani, F., Stolz, V., Viroli, M.: Adaptive distributed monitors of spatial properties for cyber-physical systems. J. Syst. Softw. **175**, 110908 (2021). https://doi.org/10.1016/j.jss.2021.110908

6. Balovnev, O.T., et al.: The story of the GeoToolKit - an object-oriented geodatabase kernel system. GeoInformatica **8**(1), 5–47 (2004). https://doi.org/10.1023/B:GEIN.0000007723.77851.8f

7. Banci Buonamici, F., Belmonte, G., Ciancia, V., Latella, D., Massink, M.: Spatial logics and model checking for medical imaging. Int. J. Softw. Tools Technol. Transfer **22**(2), 195–217 (2019). https://doi.org/10.1007/s10009-019-00511-9

8. Belmonte, G., Broccia, G., Ciancia, V., Latella, D., Massink, M.: Feasibility of spatial model checking for nevus segmentation. In: Bliudze, S., Gnesi, S., Plat, N., Semini, L. (eds.) 9th IEEE/ACM International Conference on Formal Methods in Software Engineering, FormalISE@ICSE 2021, Madrid, Spain, 17–21 May 2021, pp. 1–12. IEEE (2021). https://doi.org/10.1109/FormaliSE52586.2021.00007

9. Belmonte, G., Ciancia, V., Latella, D., Massink, M.: Innovating medical image analysis via spatial logics. In: ter Beek, M.H., Fantechi, A., Semini, L. (eds.) From Software Engineering to Formal Methods and Tools, and Back. LNCS, vol. 11865, pp. 85–109. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30985-5_7

10. Belmonte, G., Ciancia, V., Latella, D., Massink, M.: VoxLogicA: a spatial model checker for declarative image analysis. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 281–298. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17462-0_16

11. van Benthem, J., Bezhanishvili, G.: Modal logics of space. In: Aiello, M., Pratt-Hartmann, I., Benthem, J.V. (eds.) Handbook of Spatial Logics, pp. 217–298. Springer, Dordrecht (2007). https://doi.org/10.1007/978-1-4020-5587-4_5

12. Bezhanishvili, N., Ciancia, V., Gabelaia, D., Grilletti, G., Latella, D., Massink, M.: Geometric Model checking of continuous space. Log. Methods Comput. Sci. **18**(4), 7:1–7:38 (2022). https://lmcs.episciences.org/10348. https://doi.org/10.46298/LMCS-18(4:7)2022. ISSN 1860-5974

13. Bogomolov, S., Frehse, G., Giacobbe, M., Henzinger, T.A.: Counterexample-guided refinement of template polyhedra. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 589–606. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54577-5_34

14. Breunig, M., et al.: Geospatial data management research: Progress and future directions. ISPRS Int. J. Geo Inf. **9**(2), 95 (2020). https://doi.org/10.3390/ijgi9020095
15. Browne, M.C., Clarke, E.M., Grumberg, O.: Characterizing finite Kripke structures in propositional temporal logic. Theor. Comput. Sci. 59, 115–131 (1988). https://doi.org/10.1016/0304-3975(88)90098-9

16. Caires, L., Cardelli, L.: A spatial logic for concurrency (part I). Inf. Comput. 186(2), 194–235 (2003). https://doi.org/10.1016/S0890-5401(03)00137-8

17. Cardelli, L., Gordon, A.D.: Anytime, anywhere: modal logics for mobile ambients. In: Wegman, M.N., Reps, T.W. (eds.) POPL 2000, Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Boston, Massachusetts, USA, 19–21 January 2000, pp. 365–377. ACM (2000). https://doi.org/10.1145/325694.325742

18. Chrschn: A triangle mesh of dolphin (2007). https://en.wikipedia.org/wiki/File:Dolphin triangle mesh.png. Accessed 7 Feb 2023

19. Ciancia, V., Latella, D., Massink, M., de Vink, E.P.: Back-and-forth in space: on logics and bisimilarity in closure spaces. In: Jansen, N., Stoelinga, M., van den Bos, P. (eds.) A Journey From Process Algebra via Timed Automata to Model Learning. LNCS, vol. 13560, pp. 98–115. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-15629-8_6

20. Ciancia, V., Latella, D., Massink, M., Paškauskas, R., Vandin, A.: A tool-chain for statistical spatio-temporal model checking of bike sharing systems. In: Margaria, T., Steffen, B. (eds.) ISOLA 2016. LNCS, vol. 9952, pp. 657–673. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47166-2_46

21. Ciancia, V., Gabelaia, D., Latella, D., Massink, M., de Vink, E.P.: On bisimilarity for polyhedral models and SLCS - preliminary version. Technical report. ISTI-TR-2022/018, CNR-ISTI (2023). https://doi.org/10.32079/ISTI-TR-2023/003

22. Ciancia, V., Gilmore, S., Grilletti, G., Latella, D., Loreti, M., Massink, M.: Spatio-temporal model checking of vehicular movement in public transport systems. Int. J. Softw. Tools Technol. Transfer 20(3), 289–311 (2018). https://doi.org/10.1007/s10009-018-0483-8

23. Ciancia, V., Groote, J., Latella, D., Massink, M., de Vink, E.: Minimisation of spatial models using branching bisimilarity. In: Chechik, M., Katoen, J.P., Leucker, M. (eds.) FM 2023. LNCS, vol. 14000, pp. 263–281. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-27481-7_16

24. Ciancia, V., Latella, D., Loreti, M., Massink, M.: Specifying and verifying properties of space. In: Diaz, J., Lanese, I., Sangiorgi, D. (eds.) TCS 2014. LNCS, vol. 8705, pp. 222–235. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44602-7_18

25. Ciancia, V., Latella, D., Loreti, M., Massink, M.: Model checking spatial logics for closure spaces. Log. Methods Comput. Sci. 12(4) (2016). https://doi.org/10.2168/LMCS-12(4:2)2016

26. Ciancia, V., Latella, D., Massink, M., Paškauskas, R.: Exploring spatio-temporal properties of bike-sharing systems. In: 2015 IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, SASO Workshops 2015, Cambridge, MA, USA, 21–25 September 2015, pp. 74–79. IEEE Computer Society (2015). https://doi.org/10.1109/SASOW.2015.17

27. Ciancia, V., Latella, D., Massink, M., de Vink, E.P.: On bisimilarity for quasi-discrete closure spaces (2023). https://arxiv.org/abs/2301.11634

28. De Nicola, R., Vaandrager, F.W.: Three logics for branching bisimulation. J. ACM 42(2), 458–487 (1995). https://doi.org/10.1145/201019.201032

29. Galton, A.: The mereotopology of discrete space. In: Freksa, C., Mark, D.M. (eds.) COSIT 1999. LNCS, vol. 1661, pp. 251–266. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48384-5_17
30. Galton, A.: Discrete mereotopology. In: Calosi, C., Graziani, P. (eds.) Mereology and the Sciences. SL, vol. 371, pp. 293–321. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-05356-1_11

31. Girard, A., Le Guernic, C.: Zonotope/hyperplane intersection for hybrid systems reachability analysis. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 215–228. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78929-1_16

32. van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. J. ACM 43(3), 555–600 (1996). https://doi.org/10.1145/233551.233556

33. Groote, J.F., Jansen, D.N., Keiren, J.J.A., Wijs, A.: An O(mlogn) algorithm for computing stuttering equivalence and branching bisimulation. ACM Trans. Comput. Log. 18(2), 13:1–13:34 (2017). https://doi.org/10.1145/3060140

34. Hansen, H., Kupke, C., Pacuit, E.: Neighbourhood structures: bisimilarity and basic model theory. Log. Methods Comput. Sci. 5(2) (2009). https://lmcs.episciences.org/1167

35. Henzinger, T.A.: The theory of hybrid automata. In: Inan, M.K., Kurshan, R.P. (eds.) Verification of Digital and Hybrid Systems, pp. 265–292. Springer, Heidelberg (2000). https://doi.org/10.1007/978-3-642-59615-5_13

36. Henzinger, T.A., Ho, P.-H.: HyTech: the cornell hybrid technology tool. In: Antsaklis, P., Kohn, W., Nerode, A., Sastry, S. (eds.) HS 1994. LNCS, vol. 999, pp. 265–293. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-60472-3_14

37. Levine, J.A., Paulsen, R.R., Zhang, Y.: Mesh processing in medical-image analysis - a tutorial. IEEE Comput. Graphics Appl. 32(5), 22–28 (2012). https://doi.org/10.1109/MCG.2012.91

38. Linker, S., Papacchini, F., Sevegnani, M.: Analysing spatial properties on neighbourhood spaces. In: Esparza, J., Král', D. (eds.) 45th International Symposium on Mathematical Foundations of Computer Science, MFCS 2020, 24–28 August 2020, Prague, Czech Republic. LIPIcs, vol. 170, pp. 66:1–66:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020). https://doi.org/10.4230/LIPIcs.MFCS.2020.66

39. Linker, S., Papacchini, F., Sevegnani, M.: Finite models for a spatial logic with discrete and topological path operators. In: Bonchi, F., Puglisi, S.J. (eds.) 46th International Symposium on Mathematical Foundations of Computer Science, MFCS 2021, 23–27 August 2021, Tallinn, Estonia. LIPIcs, vol. 202, pp. 72:1–72:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021). https://doi.org/10.4230/LIPIcs.MFCS.2021.72

40. Loreti, M., Quadrini, M.: A spatial logic for a simplicial complex model. CoRR (2021). https://arxiv.org/abs/2105.08708

41. Massink, M., Paškauskas, R.: Model-based assessment of aspects of user-satisfaction in bicycle sharing systems. In: IEEE 18th International Conference on Intelligent Transportation Systems, ITSC 2015, Gran Canaria, Spain, 15–18 September 2015, pp. 1363–1370. IEEE (2015). https://doi.org/10.1109/ITSC.2015.224

42. McKinsey, J., Tarski, A.: The algebra of topology. Ann. Math. 45, 141–191 (1944). https://doi.org/10.2307/1969080

43. Milner, R.: Communication and Concurrency. PHI Series in Computer Science. Prentice Hall (1989)

44. Milner, R.: The Space and Motion of Communicating Agents. Cambridge University Press, Cambridge (2009)
45. Nenzi, L., Bortolussi, L., Ciancia, V., Loreti, M., Massink, M.: Qualitative and quantitative monitoring of spatio-temporal properties with SSTL. Log. Methods Comput. Sci. 14(4) (2018). https://doi.org/10.23638/LMCS-14(4:2)2018

46. Sankaranarayanan, S., Dang, T., Ivančić, F.: Symbolic model checking of hybrid systems using template polyhedra. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 188–202. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_14

47. Smyth, M.B., Webster, J.: Discrete spatial models. In: Aiello, M., Pratt-Hartmann, I., van Benthem, J. (eds.) Handbook of Spatial Logics, pp. 713–798. Springer, Dordrecht (2007). https://doi.org/10.1007/978-1-4020-5587-4_12

48. Tsigkanos, C., Nenzi, L., Loreti, M., Garriga, M., Dustdar, S., Ghezzi, C.: Inferring analyzable models from trajectories of spatially-distributed internet of things. In: 2019 IEEE/ACM 14th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS), pp. 100–106 (2019). https://doi.org/10.1109/SEAMS.2019.00021

49. Tsigkanos, C., Pasquale, L., Ghezzi, C., Nuseibeh, B.: Ariadne: topology aware adaptive security for cyber-physical systems. In: Bertolino, A., Canfora, G., Elbaum, S.G. (eds.) 37th IEEE/ACM International Conference on Software Engineering, ICSE 2015, Florence, Italy, 16–24 May 2015, vol. 2, pp. 729–732. IEEE Computer Society (2015). https://doi.org/10.1109/ICSE.2015.234

50. Čech, E.: Topological spaces. In: Pták, V. (ed.) Topological Spaces, chap. III, pp. 233–394. Publishing House of the Czechoslovak Academy of Sciences/Interscience Publishers, John Wiley & Sons, Prague/London-New York-Sydney (1966). Revised edition by Zdeněk Frolíc and Miroslav Katětov. Scientific editor, Vlastimil Pták. Editor of the English translation, Charles O. Junge. MR0211373