Research partially supported by the MIUR Project PRIN 2017FTXR7S “IT-
MaTTerS”. The authors are listed in alphabetical order, as they equally
contributed to this work.

# Geometric Model Checking of
Continuous Space

Nick Bezhanishvili  Institute for Logic, Language and Computation, University
of Amsterdam, The Netherlands  ,  Vincenzo Ciancia  Istituto di Scienza e
Tecnologie dell’Informazione “A. Faedo”, Consiglio Nazionale delle Ricerche,
Pisa, Italy  ,  David Gabelaia  TSU Razmadze Mathematical Institute, Tbilisi,
Georgia  ,  Gianluca Grilletti  Munich Center for Mathematical Philosophy,
Ludwig-Maximilians-Universität München, Germany  ,  Diego Latella  Istituto di
Scienza e Tecnologie dell’Informazione “A. Faedo”, Consiglio Nazionale delle
Ricerche, Pisa, Italy  and  Mieke Massink  Istituto di Scienza e Tecnologie
dell’Informazione “A. Faedo”, Consiglio Nazionale delle Ricerche, Pisa, Italy

###### Abstract.

Topological Spatial Model Checking is a recent paradigm where model checking
techniques are developed for the topological interpretation of Modal Logic.
The Spatial Logic of Closure Spaces, SLCS, extends Modal Logic with
reachability connectives that, in turn, can be used for expressing interesting
spatial properties, such as “being near to” or “being surrounded by”. SLCS
constitutes the kernel of a solid logical framework for reasoning about
discrete space, such as graphs and digital images, interpreted as quasi
discrete closure spaces. Following a recently developed _geometric_ semantics
of Modal Logic, we propose an interpretation of SLCS in _continuous space_ ,
admitting a geometric spatial model checking procedure, by resorting to models
based on polyhedra. Such representations of space are increasingly relevant in
many domains of application, due to recent developments of 3D scanning and
visualisation techniques that exploit mesh processing. We introduce
PolyLogicA, a geometric spatial model checker for SLCS formulas on polyhedra
and demonstrate feasibility of our approach on two 3D polyhedral models of
realistic size. Finally, we introduce a geometric definition of bisimilarity,
proving that it characterises logical equivalence.

###### Key words and phrases:

Simplicial complexes, Spatial Logic, Model Checking, Geometric Logic

##  1\. Introduction and Related Work

Spatial reasoning and spatial properties are of interest in a vast number of
domains, ranging from collective adaptive systems, concerned with the
emergence of spatial patterns, and the mobility and distribution of devices in
cyber-physical systems to medical imaging and interactive visualisation.
Recently, novel variants of model checking have been developed, moving the
focus from checking temporal properties to spatial properties, see for example
[GSC+09, CLLM14, CLLM16a, CLLM16b, NBC+18, HJK+15], and, in fact, also to the
combination of reasoning on time and space in spatio-temporal model checking
[CGL+14, CLMP15, CGL+15, CGG+18, CLM+16, Gri16, TKG17].

This so-called _topological_ approach to spatial logic and spatial model
checking has its origin in the ideas by McKinsey and Tarski [MT44], who
recognised the possibility of reasoning about space using topology as a
mathematical framework for the interpretation of modal logic (see [BB07] for a
thorough introduction). The work by Ciancia et al. (see e.g. [CLLM14,
CLLM16a]) builds on these theoretical developments using Closure Spaces, a
generalisation of topological spaces encompassing also general discrete
spatial structures such as graphs [Gal99, Gal14], as underlying model for the
Spatial Logic for Closure Spaces SLCS. The original version of this spatial
logic included two spatial operators, the near operator and the surrounded
operator. The points in space satisfying ‘near $\phi$’ are all those points
close to any point satisfying $\phi$. In other words, the near operator is
interpreted as a closure operator on space. The points satisfying ‘$\phi$
surrounded by $\psi$’, instead, are all those points satisfying $\phi$ from
which no path can be found that passes by a point not satisfying $\phi$
without first passing by a point satisfying $\psi$. In other words, these are
those points, satisfying $\phi$, that are surrounded by points satisfying
$\psi$.

Two different spatial model-checkers for finite (quasi-discrete) closure
spaces were developed based on this foundational work: Topochecker
111Topochecker: a topological model checker, see
http://topochecker.isti.cnr.it, https://github.com/ vincenzoml/topochecker and
VoxLogicA 222VoxLogicA: See https://github.com/vincenzoml/VoxLogicA.. These
tools have been used successfully in several applications. For example, for
the analysis of the spatial and spatio-temporal aspects of excessive delays in
returning bikes in the London bike sharing system [CLM+16] and the spatio-
temporal aspects of the emergence of Turing patterns [CLLM16b, NBC+18] and the
robustness of their formation in the presence of noise. Also in the field of
medical imaging these spatial model checking techniques have shown to be very
promising as a novel approach to the segmentation of malignant brain lesions
[BCLM19b, BBC+20] in 3D MRI scans as well as for the segmentation of normal
brain tissue, such as white and grey matter [BCLM19a]. A similar approach has
also been used for the segmentation of nevi333Benign and malignant lesions of
the skin. in 2D dermoscopic images [BBC+21]. The application of spatial model
checking techniques on publicly available datasets, consisting of hundreds of
such medical images, showed that an accuracy and computational efficiency can
be obtained that is in line with the state-of-the-art in such fields.

So far, spatial model checking approaches focused on discrete spatial
structures, i.e. discrete sets of points related by an adjacency relation,
namely graphs. However, in several domains, e.g. medical imaging and
visualisation in virtual reality, reasoning on continuous space is required.
For example, computerised 3D visualisation of medical images can help
physicians to make better diagnoses or treatment plans. Images used for
visualisation often consist of continuous spatial structures that are divided
into suitable areas of different size using mesh techniques such as
_triangular surface meshes_ or _tetrahedral volume meshes_ (see for example
[LPZ12]).

In the present work we therefore focus on the development of the foundations
to reason about and model-check properties of continuous space. Interestingly,
we will also show how our earlier results on discrete space are, in part, also
relevant to model-checking continuous space. Unlike the topological semantics,
where formulas are interpreted in the powerset algebra of a topological space,
in the polyhedral semantics formulas are assigned polyhedral subsets of an
$m$-dimensional Euclidean space. Polyhedral subsets can be thought of as
finite unions of simplexes (i.e. $n$-dimensional triangles). Using piecewise
linear geometry (triangulations, nerves), the work in [BMMP18] gives a full
characterization of the intuitionistic and modal logics of the class of all
compact polyhedra and [ABGM21, AD19] provide an infinite family of
polyhedrally complete modal and intermediate logics.

The version of SLCS we use in this paper is obtained by extending the
polyhedral modal logic with a _spatial reachability_ modality $\gamma$, which
is a variant of the $\rho$ operator originally proposed in [BCLM19b] that, in
turn, can be seen as a spatial version of the Existential Until operator of
temporal logics. Roughly speaking, $\gamma(\phi,\psi)$ (pronounced as $\psi$
is reachable through $\phi$) means that a point satisfying $\psi$ is reachable
by a path satisfying $\phi$ along the way. The reachability modality is quite
expressive and other operators, relevant for the intended applications (such
as “surrounded”, or “grow”, discussed in more detail throughout the paper),
can be defined based on it. We show that the reachability modality can be
defined for polyhedral models.

One of the main conceptual results of the present paper is that, starting from
a polyhedral model $\mathcal{X}$, we can build a relational (Kripke) model
$\mathcal{M}(\mathcal{X})$ satisfying the same formulas of the logic. In
particular, $\mathcal{M}(\mathcal{X})$ is isomorphic to the face poset of an
underlying triangulation of $\mathcal{X}$. Triangulation is a standard
technique of piecewise linear geometry in which each polyhedron is decomposed
in simplexes. That triangulations play an important role in the logical
analysis of polyhedra has already been observed in [BMMP18, AD19, ABGM21].
However, here we show this also for the language enriched with the
reachability modality $\gamma$. In particular, $\mathcal{M}(\mathcal{X})$
captures all the properties expressible in this extended language.

The finite state, Kripke-style semantics that we define preserves all the
information that can be discerned by SLCS formulas. This is the key for
introducing a novel _geometric model checking_ technique to analyse continuous
space. We prove that the continuous model of the extended language can be
turned into a finite relational model for the same language without losing any
of the logical information. A model checking algorithm, along the lines of
[BCLM19b], has been implemented in the free and open source geometric model
checker PolyLogicA, which brings the core features of VoxLogicA (global model
checking, concurrent multi-core execution, “memoization” at the syntactic
level) to the continuous space domain.

Finally, we define a notion of _bisimilarity_ between two polyhedral models,
and we prove that bisimilarity preserves and reflects logical equivalence.

Summarizing, the original contributions in this paper are:

  * •

The development of a (continuous space) polyhedral semantics for the logic
SLCS building upon recent developments in polyhedral semantics for modal and
intuitionistic logic [BMMP18, ABGM21, AD19];

  * •

The introduction of a finite state relational Kripke model
$\mathcal{M}(\mathcal{X})$ for any given (continuous space) polyhedral model
$\mathcal{X}$, such that $\mathcal{M}(\mathcal{X})$ provides a full logical
invariant for $\mathcal{X}$ with respect to SLCS;

  * •

A novel geometric spatial model checking algorithm for the verification of
SLCS properties on polyhedral models;

  * •

First proof-of-concept model checking of two realistic-size polyhedral models
using PolyLogicA, the first-in-its-kind prototype implementation of the
geometric model checking algorithm;

  * •

A novel notion of simplicial bisimilarity characterising logical equivalence
for SLCS formulas.

##### Further related work.

The theoretical framework for spatial model checking of continuous space in
the present paper is based on spatial models involving polyhedra (see also the
work in [CM21], generalising the semantics of SLCS to a categorical setting
based on hyperdoctrines). Polyhedra also play an important role in development
of model checking algorithms for the verification of behavioural properties of
real-time and hybrid systems (see for example [HH94, Alu11, BFGH17, Hen00,
AGH+19] and references therein). In that context polyhedra, and their related
notions such as template polyhedra [SDI08, BFGH17] and zonotopes [GG08], 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. In the present paper we focus on spatial properties of continuous
space rather than behavioural properties.

Topology and simplicial complexes also play an important role in the domain of
geographic information systems (GIS). In that domain of application simplicial
complexes are used as an efficient data structure to store large geospatial
data sets [BBJ+20] in 2D or 3D. They also form the core of several important
tools in this domain such as the GeoToolKit [BBB+04]. This could therefore be
in principle another interesting domain of application for spatial model
checking techniques, enriching the spatial query languages that are currently
used in this database oriented domain.

Model Checking of simplicial complexes is also the topic of recent work by
Loreti and Quadrini [LQ21], developed independently from our work444See
[BCG+21a] for an earlier version of the present paper. Therein, a logic is
defined, sharing similar syntax, but not its semantics, with the logic SLCS
used in the present paper. More precisely, the domain upon which formulas are
interpreted, are not (sets of) points in polyhedra, but rather (sets of)
simplices. This is reflected by the choice of the adjacency relation between
objects555Actually, the paper proposes three different relations, see
Definition 1–3 therein. giving rise to _nearness_ and _reachability_. In
contrast, the domain of interpretation of our spatial logic SLCS are points of
topological spaces, with polyhedral atomic valuations, and reachability is the
classical topological notion, defined via paths.

Looking at tools, perhaps closest to our work is the python library pymeshlab
[MC21], which is able to programmatically modify 3D meshes based on pre-built
operators (mostly traditional 3D imaging filters). Since also the selection of
connected components is an operator of the library, we envisage that it could
be possible, given an SLCS formula, to encode it as a python program
containing pymeshlab functions, effectively using the library as a backend for
VoxLogicA. Indeed, using such a library within the context of a traditional
programming language does not lay at the same level of abstraction of using a
simple declarative language such as SLCS, with automatic parallelisation, and
automatic memoization (caching) of intermediate results, so a direct
comparison of the library and our tool would be misleading.

##### Outline.

Section 2 introduces the basic geometrical notions and notation. Section 3
recalls SLCS and provides its semantics on polyhedral models. Section 4 and
Section 5 present the foundations for geometric model checking and the related
model checker PolyLogicA, respectively, including two proof-of-concept
examples on realistic size polyhedra. In Section 6 the concept of simplicial
bisimilarity is introduced and it is shown that it characterises logic
equivalence for SLCS formulas. Section 7 concludes the paper with an outlook
for future work.

Proofs of the most relevant theoretical results are reported in Appendix A.

##  2\. Background

In this section, we establish the basic geometric notions that we use in this
work. See [Mau80, Chapter 2] for more details on these matters.

[Simplex] A _$d$ -simplex_ $\sigma$ is the convex hull of a finite set
$V=\\{v_{0},v_{1},\dots,v_{d}\\}$ $\subseteq$ $\mathbb{R}^{m}$ of $d+1$
affinely independent points666 $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\leq m$. , that is the set

$\sigma=\left\\{\lambda_{0}v_{0}+\dots+\lambda_{d}v_{d}\;\middle|\;\forall
i.\lambda_{i}\in[0,1]\;\text{and}\;\sum_{i=0}^{d}\lambda_{i}=1\right\\}.$

The number $d$ is called the _dimension_ of $\sigma$ and $v_{0},\dots,v_{d}$
are called its _vertices_.

In Definition 2, any subset of $\\{v_{0},\dots,v_{d}\\}$ is also a set of
affinely independent points, and thus it spans a simplex $\tau$: we call
$\tau$ a _face_ of $\sigma$ (in symbols $\tau\preceq\sigma$), and we call it a
_proper face_ if $\tau\neq\emptyset$ and $\tau\neq\sigma$. Next, we identify
the “internal part” of a simplex. [Relative interior] In terms of the notation
of Definition 2, let the _relative interior_ of $\sigma$ be the set
$\widetilde{\sigma}:=\left\\{\sum_{i=0}^{d}\lambda_{i}v_{i}\;\middle|\;\forall
i.\lambda_{i}\in(0,1]\;\text{and}\;\sum_{i=0}^{d}\lambda_{i}=1\right\\}$. Note
that if $\sigma$ is non-empty then also $\widetilde{\sigma}$ is non-empty. For
instance, $b_{\sigma}:=\sum_{i=0}^{d}\frac{1}{d+1}v_{i}$ (i.e., the
_barycentre_ of $\sigma$) is an element of $\widetilde{\sigma}$. In
particular, the relative interior of a point $p$ is $p$ itself. Each simplex
$\sigma$ is partitioned by the relative interiors of its faces, that is,
$\sigma=\bigcup\\{\widetilde{\tau}\;|\;\tau\preceq\sigma\\}$.

In this paper we adopt the Kuratowski axiomatic characterisation of
topological spaces, based on the closure operator. We denote the latter by
$\mathcal{C}$. Given topological space $(X,\mathcal{C})$ we let $\mathcal{I}$
denote the interior operator, i.e. the dual of $\mathcal{C}$ defined as
$\mathcal{I}(A)=X\setminus\mathcal{C}(X\setminus A)$ for all $A\subseteq X$.
Finally, for $X^{\prime}\subseteq X$, the topological sub-space of
$(X,\mathcal{C})$ generated by $X^{\prime}$ is the pair
$(X^{\prime},\mathcal{C}^{\prime})$, where
$\mathcal{C}^{\prime}(A)=\mathcal{C}(A)\cap X^{\prime}$ for all $A\subseteq
X^{\prime}$. For ease of notation, we will indicate the topological space
$(X,\mathcal{C})$ simply as $X$ when no confusion arises.

Simplexes are bounded, convex, compact subspaces of $\mathbb{R}^{m}$ [Mau80,
Proposition 2.3.3]. Being subsets of an Euclidean space $\mathbb{R}^{m}$, a
simplex $\sigma$ inherits the topological structure of the sub-space from
$\mathbb{R}^{m}$. Let us indicate by $\mathcal{C}_{m}$ the closure operator of
$\mathbb{R}^{m}$ and by $\mathcal{C}_{\sigma}$ the induced closure operator on
$\sigma$. Notice that, since $\sigma$ is a closed subset of $\mathbb{R}^{m}$,
the closure of any subset $A\subseteq\sigma$ is the same computed in both
topologies, that is, $\mathcal{C}_{m}(A)=\mathcal{C}_{\sigma}(A)$. An
emblematic example is the closure of $\widetilde{\sigma}$:
$\mathcal{C}_{\sigma}(\widetilde{\sigma})=\mathcal{C}_{m}(\widetilde{\sigma})=\sigma$.
However, the interior of a set may depend on the topology considered: for
example, $\mathcal{I}_{m}(\sigma)$ is either $\widetilde{\sigma}$ if the
dimension of $\sigma$ is $m$, or the empty set otherwise. On the other hand,
$\mathcal{I}_{\sigma}(\sigma)=\sigma$, independently from the dimension.

More complex spaces are obtained by “gluing” simplexes together.

[Simplicial complex] A _simplicial complex_ $\mathrm{K}$ is a finite set of
simplexes of $\mathbb{R}^{m}$ such that:

  1. (1)

If $\sigma\in\mathrm{K}$ and $\tau$ is a face of $\sigma$, then
$\tau\in\mathrm{K}$;

  2. (2)

If $\sigma,\tau\in\mathrm{K}$, then $\sigma\cap\tau$ is a face of $\sigma$ and
$\tau$ (possibly the empty simplex).

Figure 1. On the left, a graphical representation of a simplicial complex is
shown in grey and black. On the right, we highlight some of the faces of the
simplicial complex, of dimension 2, 1 and 0 (the green triangle, blue segment
and red point, respectively).

Figure 1 illustrates an example of a simplicial complex $\mathrm{K}$ and
highlights some of the simplexes comprising it. The _dimension_ of
$\mathrm{K}$ is the maximum of the dimensions of its simplexes, i.e. $2$ in
Figure 1. The face relation on simplexes is inherited by simplicial complexes
in the expected way: the face relation $\preceq$ on simplicial complex
$\mathrm{K}$ is the union of the face relations on the simplexes composing
$\mathrm{K}$.

We call the set of points that lie in at least one of the simplexes of
$\mathrm{K}$ the _polyhedron_ of $\mathrm{K}$, formally defined as
$\left|\mathrm{K}\right|:=\bigcup\mathrm{K}$. As for simplexes,
$\left|\mathrm{K}\right|$ is a subset of the ambient space $\mathbb{R}^{m}$
and so inherits the topological structure of sub-space of $\mathbb{R}^{m}$.
Let us indicate with $\mathcal{C}_{\mathrm{K}}$ the corresponding closure
operator—notice that this operator only depends on the set
$\left|\mathrm{K}\right|$. A point of $\left|\mathrm{K}\right|$ may belong to
several of the simplexes in $\mathrm{K}$. However, there is a natural way to
associate to each point of $\left|\mathrm{K}\right|$ the “smallest” simplex it
belongs to.

######  Lemma 1.

Each point of $\left|\mathrm{K}\right|$ belongs to the relative interior of
exactly one non-empty simplex in $\mathrm{K}$. That is,
$\widetilde{\mathrm{K}}:=\\{\widetilde{\sigma}\,|\,\sigma\in\mathrm{K}\setminus\\{\emptyset\\}\\}$
is a partition of $\left|\mathrm{K}\right|$.

We call $\widetilde{\mathrm{K}}$ a _simplicial partition_ of $|\mathrm{K}|$,
and we call its elements the _cells_ of the partition.777 We use the
terminology _cells_ in this way for the purposes of this paper; there is no
relation between such cells and the so-called _cell complexes_ of algebraic
topology.  Note that distinct simplicial complexes induce distinct partitions,
even when they are associated to the same polyhedron. From now on, to ease
readability, we fix a simplicial complex $\mathrm{K}$, with the associated
$\left|\mathrm{K}\right|$ and $\widetilde{\mathrm{K}}$.

Finally, we recall the topological notion of _path_. A topological _path_ in a
topological space $P$ is a total, continuous function $\pi:[0,1]\to P$, where
$[0,1]$ is equipped with the subspace topology of $\mathbb{R}$. With a mild
abuse of notation, for $S$ a subset of $[0,1]$ and $\pi$ a path, we write
$\pi(S)$ to denote $\\{\pi(x)\mid x\in S\\}$.

##  3\. Interpreting SLCS on Polyhedra

In this section we introduce the main theory driving our model checking
approach to polyhedra. In the classical topological tradition, valuations of
atomic propositions can be arbitrary subsets of the space. In this work,
instead, we restrict our attention to a specific class of spatial regions,
namely unions of cells of a fixed simplicial partition. This simple change
makes it possible to define the spatial logic SLCS on continuous space, while
retaining decidability of the model checking problem. First of all, we
introduce the syntax of the variant of SLCS that we use in this paper, that is
based on the binary modality $\gamma$ instead of $\rho$ of [BCLM19b]; the
relationship between $\rho$ and $\gamma$ will be shown in Proposition 13.

[Syntax] The syntax of the logic SLCS is:

$\phi\;::=\;\top\;|\;p\;|\;\neg\phi\;|\;\phi\land\phi\;|\;\Box\phi\;|\;\gamma(\phi,\phi)$

where $p$ is an atomic proposition, taken from a fixed finite set
$\mathrm{AP}$.

Thus, we enhance the basic modal logic with a _spatial reachability_ operator
$\gamma$. As in the standard topological semantics for modal logic, we
interpret formulas as sets of points. Boolean operators are given their
standard set-theoretical interpretation; disjunction $\lor$ is derived via the
De Morgan laws. The $\Box$ modality corresponds to _topological_ interior
$\mathcal{I}$.

The formula $\gamma(\phi,\psi)$ (“reach $\psi$ through $\phi$”) is satisfied
by a point if there is a path rooted in that point, leading to a point
satisfying $\psi$ and whose intermediate points all satisfy $\phi$. We provide
a number of examples of the operators after presenting the models and formal
semantics of the logic. In the following, we let $\mathcal{P}(P)$ denote the
powerset of $P$.

[Model] A _Polyhedral Model_ is a triplet $\mathcal{X}=\left\langle
P,\mathrm{K},V\right\rangle$, where $P\subseteq\mathbb{R}^{d}$ is a
polyhedron, $\mathrm{K}$ is a simplicial complex such that $P=|\mathrm{K}|$,
and $V:\mathrm{AP}\to\mathcal{P}(P)$ is a valuation such that $V(p)$ is a
union of cells of $\widetilde{\mathrm{K}}$.

Polyhedral models are essentially topological models with some extra
restrictions on the valuation: $P$ plays the role of the topological space and
$V$ is used to interpret atomic propositions as specific subsets of this
space, namely those that are the union of a finite number of simplicial cells.
From now on, fix a polyhedral model $\mathcal{X}=\left\langle
P,\mathrm{K},V\right\rangle$.

[Semantics] Given $x\in P$, satisfaction $\mathcal{X},x\vDash\phi$ over
formulas $\phi$ is given by the following inductive clauses, where we let
$\left\llbracket\phi\right\rrbracket^{\mathcal{X}}$ denote the set $\\{x\in
P\,|\,\mathcal{X},x\vDash\phi\\}$:

$\begin{array}[]{lcl}\mathcal{X},x\vDash\top&\lx@intercol\text{always
holds}\hfil\lx@intercol\\\ \mathcal{X},x\vDash p&\iff&x\in V(p)\;\,\text{for
}p\in\mathrm{AP}\\\
\mathcal{X},x\vDash\neg\phi&\iff&\mathcal{X},x\nvDash\phi\\\
\mathcal{X},x\vDash\phi\land\psi&\iff&\mathcal{X},x\vDash\phi\;\text{and}\;\mathcal{X},x\vDash\psi\\\
\mathcal{X},x\vDash\Box\phi&\iff&x\in\mathcal{I}_{P}(\left\llbracket\phi\right\rrbracket^{\mathcal{X}})\\\
\mathcal{X},x\vDash\gamma(\phi,\psi)&\iff&\text{there exists a path $\pi$ such
that}\\\
&&\pi(0)=x,\,\pi(1)\in\left\llbracket\psi\right\rrbracket^{\mathcal{X}}\text{and
}\pi((0,1))\subseteq\left\llbracket\phi\right\rrbracket^{\mathcal{X}}\end{array}$

The definition of the satisfaction relation for the standard operators of
modal logic is the usual one for the classical topological interpretation. In
particular, note the interpretation of $\Box\phi$ as the _topological
interior_ with respect to the topology of $P=\left|\mathrm{K}\right|$,
intuitively expressing that point $x$ is in the “internal” part of the set of
points satisfying $\phi$. Notice that the closure operator $\mathcal{C}_{P}$
can be obtained as the dual of topological interior
$\Diamond\phi=\neg(\Box\neg\phi)$. Figure 2 illustrates these operators and
their combination applied on a simple polyhedral model.

Regarding spatial reachability, a point $x$ satisfies $\gamma(\phi,\psi)$ in
model $\mathcal{X}$ if there is a path $\pi$ rooted in $x$ leading to a point
$y$ satisfying $\psi$; in addition, all the points that lay in $\pi$, except
$x$ and $y$, are required to satisfy $\phi$. Indeed, several different
variants of reachability could be defined using this operator.

As a prominent example, the reachability modality $\rho\,\psi\,[\phi]$
introduced in [BCLM19b], that we also employ to introduce some derived
operators, can be defined as $\rho\,\psi[\phi]:=\psi\lor\gamma(\phi,\psi)$.
Actually, the two operators are inter-definable, by letting
$\gamma(\phi,\psi):=\rho\,(\phi\land\rho\,\psi[\phi])[\phi]$ (see Proposition
13). In this work we opt to use $\gamma$ since, in the context of polyhedral
models, its definition is more concise.

Another relevant spatial modality is the surrounded operator ${\mathcal{S}}$
(e.g., [CLLM16a, LPS20, TKG17, NBC+18] use it as a primitive of the language).
A point $x$ satisfies $\phi\,{\mathcal{S}}\,\psi$ if it lays in an area whose
points satisfy $\phi$, and that is limited (i.e., surrounded) by points that
satisfy $\psi$. In other words, it is not possible to exit this area without
passing by a point satisfying $\psi$. Following [BCLM19b], we can define the
operator ${\mathcal{S}}$ on polyhedral models in terms of $\rho$ through the
following expression: $\phi\,\land\,\neg\rho\,(\neg(\phi\vee\psi))[\neg\psi]$.

Some examples involving the reachability operator are shown in Figure 3. We
refer to the caption of that figure for more detailed explanation. Notably, we
illustrate the derived operator $grow(a,b)$, that also played an important
role in the brain tumour segmentation procedure presented in [BCLM19b]. The
operator $grow$ is reminiscent of the technique of _region growing_ in Medical
Imaging, and it is used to characterise those areas of space satisfying $b$
that are in contact with areas of space satisfying $a$, or, in other words,
the operator lets $a$ “grow” inside $b$ (and no further). The formal
definition is
$grow(\phi_{1},\phi_{2}):=\phi_{1}\lor(\phi_{2}\land\rho\,\phi_{1}[\phi_{2}])$.

(a)  Model A

(b)  $\Box g$

(c)  $\Diamond g=\neg(\Box\neg g)$

(d)  $\Diamond(\Box g)$

Figure 2. Examples of basic topological operators on Polyhedra. 2a) Polyhedral
model A. Circles denote 0-dimensional simplexes. The valuation of atomic
propositions $r,g,b$ in model A is given by the colours _red_ , _green_ , and
_blue_ , respectively. The points in model A that satisfy the following
example formulas are shown in orange in: 2b) $\Box g$, i.e. points satisfying
the topological interior of the part in _green_ in model A; 2c) $\Diamond g$,
i.e. points satisfying the topological closure of the part in _green_ in model
A; 2d) $\Diamond(\Box g)$, i.e. points satisfying the closure of the interior
of the part in _green_ in model A.

(a)  Model C

(b)  $\gamma(g,b)$

(c)  $grow(r,g)$

(d)  $g\land\gamma(g,\gamma(b,r))$

Figure 3. Examples illustrating the reachability operator on Polyhedra. 3a)
Polyhedral model C. Circles and colours have the same meaning as in Figure 2.
Dashed segments and white points and triangles do not satisfy any atomic
proposition. 3b) In orange: Points satisfying $\gamma(g,b)$ applied to the
model in 3a. Note that these include points in the closure of the green area
since the first point of the paths passing by green and reaching blue do not
need to be green themselves. 3c) In orange: Points satisfying $grow(r,g)$.
Note that only the points corresponding to the red area and one green triangle
in the model in 3a satisfy this formula. 3d) In orange: Points satisfying
$g\land\gamma(g,\gamma(b,r))$; by nesting reachability, quite complex spatial
formulas may be defined.

Note that the same polyhedron $P$ can be associated with different simplicial
complexes: our semantics is not sensitive to such presentational ambiguity in
the description of $P$.888Such ambiguity can be thought of as being similar,
in spirit, to the infinitely many different programs that may result in
equivalent Kripke frames, in a specification language for classical model
checking applications. This is because, although we need to specify
$\mathrm{K}$ to spell out the restriction on the range of $V$, $\mathrm{K}$
itself does not play a role in the semantics, as shown in the following
proposition.

######  Lemma 2.

Let $\mathcal{X}=\left\langle P,\mathrm{K},V\right\rangle$ and
$\mathcal{X}^{\prime}=\left\langle P,\mathrm{K}^{\prime},V\right\rangle$ be
two models sharing the same $P$ and $V$. For each $x\in P$ and $\phi$ we have:
$\mathcal{X},x\vDash\phi\iff\mathcal{X}^{\prime},x\vDash\phi$.

Therefore, for the sake of readability, we will sometimes indicate a
polyhedral model with the notation $\mathcal{X}=\left\langle
P,V\right\rangle$, abstracting from the particular choice of $\mathrm{K}$.
Nevertheless, we require $V$ to range over unions of cells of _some_
polyhedral partition, thus restricting the semantics to spatial regions
definable in terms of polyhedra. We will call a simplicial complex
$\mathrm{K}$ as in Definition 3 _coherent_ with the model
$\mathcal{X}=\left\langle P,V\right\rangle$.

We mentioned that employing polyhedra allows for a _finitary treatment_ of the
semantics. The following results are essential to formalize this intuition,
which will be further investigated in Section 4.

Let $\mathcal{X}=\left\langle P,V\right\rangle$ be a polyhedral model.
_Logical equivalence_ $\equiv$ is the binary relation on $P$ such that
$x\equiv y$ if and only if, for every formula $\phi$:
$\mathcal{X},x\vDash\phi\iff\mathcal{X},y\vDash\phi$.

######  Lemma 3.

Let $\mathcal{X}$ be a polyhedral model and $\mathrm{K}$ a simplicial complex
coherent with $\mathcal{X}$. Then for each cell
$\widetilde{\sigma}\in\widetilde{\mathrm{K}}$ and $x,y\in\widetilde{\sigma}$
we have $x\equiv y$.

In particular, for every formula $\phi$,
$\left\llbracket\phi\right\rrbracket^{\mathcal{X}}$ is a (finite) union of
cells of $\widetilde{\mathrm{K}}$.

######  Proposition 4.

Given a polyhedral model $\mathcal{X}$, the relation $\equiv$ has only
finitely many equivalence classes. Furthermore, each equivalence class $C$ has
a _characteristic formula_ $\phi^{C}$ such that
$\mathcal{X},x\vDash\phi^{C}\iff x\in C$.

The above facts are also useful to prove an interesting feature of polyhedral
models, namely that the $\Box$ modality can be considered a derived operator,
since it is expressible using $\gamma$. This considerably simplifies proofs.

######  Theorem 5.

For each formula $\phi$, we have
$\mathcal{X},x\vDash\Box\phi\iff\mathcal{X},x\vDash\lnot\gamma(\lnot\phi,\top)$.

Another property of polyhedral models which turns out to be fundamental in
this work is that we can restrict our attention to a special class of
paths—rather than arbitrary paths—to study the reachability operator $\gamma$:
_piecewise linear paths_.

[PL-path] We call a path $\pi:[0,1]\to P$ _piecewise linear_ (or simply PL-
path) if there exist values $r_{0}=0,r_{1},\dots,r_{k}=1$ such that for every
$i=0,\dots,k-1$ and $t\in[0,1]$:
$\pi\big{(}tr_{i}+(1-t)r_{i+1}\big{)}=t\pi(r_{i})+(1-t)\pi(r_{i+1})$.

x (a)  Path 1

y (b)  Path 2

Figure 4.  Two examples of piecewise linear paths, one starting in point $x$
and the other in point $y$.

Figure 4 shows two examples of piecewise linear paths. We indicate that a path
is piecewise linear with the notation $\pi:[0,1]\stackrel{{\scriptstyle
PL}}{{\to}}P$. Intuitively, a PL-path is obtained by connecting a finite
number of segments and parametrizing them in a suitable way. Even if PL-paths
are much simpler than arbitrary paths, when it comes to connectivity in
polyhedral models the two classes are interchangeable, as shown in the
following lemma.

######  Lemma 6.

Let $\mathrm{K}$ be a simplicial complex and $x,y\in\left|\mathrm{K}\right|$.
Then there exists a path in $\left|\mathrm{K}\right|$ from $x$ to $y$ if and
only if there is a PL-path in $\left|\mathrm{K}\right|$ from $x$ to $y$.

Using the previous result, we can give an alternative semantic
characterization of the reachability operator, which is relevant for the
proofs of decidability of model checking (Section 4) and the characterisation
of logical equivalence via bisimilarity (Section 6).

######  Lemma 7.

We have: $\mathcal{X},x\vDash\gamma(\phi,\psi)$ if and only if there is a PL-
path $\pi:[0,1]\stackrel{{\scriptstyle PL}}{{\to}}P$ such that $\pi(0)=x$ and
$\pi((0,1))\subseteq\left\llbracket\phi\right\rrbracket^{\mathcal{X}}$ and
$\pi(1)\in\left\llbracket\psi\right\rrbracket^{\mathcal{X}}$.

We conclude this section by pointing out an interesting property of PL-paths
in connection to simplicial complexes. By definition, PL-paths are obtained by
concatenating a finite number of line segments, but in general each segment
might traverse different cells of the simplicial complex $\mathrm{K}$. However
we can give an alternative decomposition of these paths so that each portion
is fully contained in a unique cell; paths that admit such a decomposition are
called _simplicial paths_.

A path $\pi:[0,1]\to P$ is _simplicial_ if and only if there is a finite
sequence $s_{0}=0<\ldots<s_{k}=1$ of values in $[0,1]$ and cells
$\widetilde{\sigma}_{1},\dots,\widetilde{\sigma}_{k}\in\widetilde{\mathrm{K}}$
such that, for all $i=1,\dots,k$, we have
$\pi((s_{i-1},s_{i}))\subseteq\widetilde{\sigma_{i}}$.

Notice that the property of being _simplicial_ depends on the simplicial
complex $\mathrm{K}$, since a path might be simplicial with respect to a
certain triangulation of $P$, but not with respect to another. For PL-paths,
this property holds independently from the simplicial complex considered.

######  Lemma 8.

Any piecewise linear path is simplicial.

##  4\. Geometric Model Checking

Given a polyhedral model $\mathcal{X}$, this section is devoted to identifying
a corresponding Kripke-style, finite model $\mathcal{M}(\mathcal{X})$.
Notably, $\mathcal{M}(\mathcal{X})$ is also a topological model in the sense
of [BB07] when equipped with the Alexandrov topology, and it is a quotient of
$\mathcal{X}$ that preserves and reflects the semantics of each formula. The
goal of this section is to extend the standard Kripkean semantics of modal
logic to the language of SLCS, by defining a suitable semantics for $\gamma$
and by showing that $\mathcal{X}$ and $\mathcal{M}(\mathcal{X})$ are logically
equivalent, in the sense that, for all $x\in\mathcal{X}$ and for all formulas
$\Phi$, letting $\widetilde{\sigma}$ be the only cell such that
$x\in\widetilde{\sigma}$, we have: $\mathcal{X},x\models\Phi$ if and only if
$\mathcal{M}(\mathcal{X}),\widetilde{\sigma}\models\Phi$. To do so, we
introduce a suitable notion of path in $\mathcal{M}(\mathcal{X})$
corresponding to a simplicial path in $\mathcal{X}$. Model checking on
$\mathcal{X}$ can then be carried out using $\mathcal{M}(\mathcal{X})$.

Given a polyhedral model $\mathcal{X}=\left\langle
P,\mathrm{K},V\right\rangle$, we define the Kripke model
$\mathcal{M}(\mathcal{X})=\left\langle\widetilde{\mathrm{K}},\widetilde{\preceq},\widetilde{V}\right\rangle$,
where

  * •

$\widetilde{\mathrm{K}}$ is the simplicial partition of $|\mathrm{K}|$
generated by $\mathrm{K}$, as Defined in Lemma 1,

  * •

$\widetilde{\preceq}\subseteq\widetilde{\mathrm{K}}\times\widetilde{\mathrm{K}}$
with $\widetilde{\sigma}_{1}\;\widetilde{\preceq}\;\widetilde{\sigma}_{2}$ iff
$\sigma_{1}\;\preceq\;\sigma_{2}$, and

  * •

$\widetilde{\sigma}\in\widetilde{V}(p)$ iff $\widetilde{\sigma}\subseteq V(p)$

where $\preceq$ is the face relation of the simplicial complex $\mathrm{K}$.

$B$$A$$D$$C$$F$$E$ (a)  Polyhedral model $\mathcal{X}$

$B$$A$$D$$C$$F$$E$$AB$$BD$$BC$$AC$$CD$$DF$$DE$$CE$$EF$$BCD$$ABC$$DEF$$CDE$ (b)
Kripke model $\mathcal{M}(\mathcal{X})$

Figure 5.  The polyhedral model $\mathcal{X}$ of Figure 14 (5a) and its
corresponding Kripke model $\mathcal{M}(\mathcal{X})$ (5b). We indicate a cell
by the set of the vertices of the corresponding simplex. The accessibility
relation $\widetilde{\preceq}$ is represented via its Hasse diagram (reflexive
and transitive edges are omitted). The atomic propositions $g$ and $r$ are
indicated in green and red respectively.

Notice that, since $\preceq$ is reflexive, anti-symmetric and transitive, then
so is $\widetilde{\preceq}$. An example of a 2D polyhedral model together with
its corresponding Kripke model $\mathcal{M}(\mathcal{X})$ is depicted in
Figure 5 (where reflexive and transitive relations are omitted). Each cell is
identified by the vertices of the corresponding simplexes indicated in the
polyhedron on the left in Figure 5.

Such Kripke models can be depicted as a number of rows. The nodes in the
bottom row represent the zero-dimensional cells (i.e. the vertices), the
middle row the one-dimensional ones (i.e. the line segments) and the top-row
the two-dimensional cells (i.e. the triangles). To represent 3D polyhedral
models we would have one more row representing the three-dimensional cells
(i.e. tetrahedrons), and so on for higher dimensions. We emphasize that
$\mathcal{M}(\mathcal{X})$, although disregarding much of the information
about a polyhedral model (e.g., the position and size of the simplexes)
encodes all the information which is expressible using SLCS, while being a
finite—thus computationally tractable—representation of $\mathcal{X}$.

By definition of the relation $\widetilde{\preceq}$, we have that for two
different cells $\widetilde{\sigma}_{1}$ and $\widetilde{\sigma}_{2}$,
$\widetilde{\sigma}_{1}\,\widetilde{\preceq}\,\widetilde{\sigma}_{2}$ entails
that the two cells are spatially adjacent—more precisely, $\sigma_{1}$ is part
of the _boundary_ of $\sigma_{2}$. This becomes particularly relevant when
studying PL-paths in $P$. In fact, a PL-path can transit between two different
cells $\widetilde{\sigma}_{1}$ and $\widetilde{\sigma}_{2}$ only if either
$\widetilde{\sigma}_{1}\widetilde{\preceq}\widetilde{\sigma}_{2}$ or
$\widetilde{\sigma}_{1}\widetilde{\succeq}\widetilde{\sigma}_{2}$ holds. Based
on this intuition, the next definition introduces special paths on these
Kripke models corresponding to PL-paths on the polyhedron.

[$\pm$-path] Given a polyhedral model $\mathcal{X}$, with
$\mathcal{M}(\mathcal{X})=\left\langle\widetilde{\mathrm{K}},\widetilde{\preceq},\widetilde{V}\right\rangle$
as in Definition 4, let $\preceq^{\pm}$ be the relation
$\widetilde{\preceq}\cup\widetilde{\succeq}$. We say that
$\pi:\\{0,\dots,k\\}\to\widetilde{\mathrm{K}}$ is a _$\pm$ -path_ (and we
indicate it with
$\pi:\\{0,\dots,k\\}\stackrel{{\scriptstyle\pm}}{{\to}}\widetilde{\mathrm{K}}$)
if $k\geq 2$ and
$\pi(0)\;\widetilde{\preceq}\;\pi(1)\;\preceq^{\pm}\;\pi(2)\;\preceq^{\pm}\;\dots\;\preceq^{\pm}\;\pi(k-1)\;\widetilde{\succeq}\;\pi(k)$.

Intuitively, a $\pm$-path $\pi$ represents the cells traversed by a PL-path
$\pi^{\prime}$ in $P$; $\pi(0)$ is the cell containing the first point
$\pi^{\prime}(0)$ of the PL-path $\pi^{\prime}$; $\pi(1)$ is the cell
containing the the next portion of PL-path $\pi^{\prime}$, i.e. the image via
the PL-path $\pi^{\prime}$ of an interval of the form $(0,s)$ or $(0,s]$, for
some $s$, and so on, up to cell $\pi(k)$ that contains the end-point
$\pi^{\prime}(1)$ of the PL-path $\pi^{\prime}$. An example of a PL-path and
its corresponding $\pm$-path is shown in Figure 6. Notice that the first step
$\pi(0)\pi(1)$ in the $\pm$-path $\pi$ reflects the move from the starting
point in the PL-path to the subsequent segment on the PL-path in polyhedron
$P$. The starting point must obviously be ‘connected’ to this subsequent path
segment. This is only possible if the starting point is in the closure of the
cell that contains the interval, in other words,
$\pi(0)\,\widetilde{\preceq}\,\pi(1)$, that is $\pi(0)$ must be on the
boundary of $\mathcal{C}_{P}(\pi(1))$. Moreover, if $\pi(0)=\pi(1)$, then,
depending on the dimension of the cell containing the starting point, the
subsequent portion of the path can be in the same cell as the starting point.
This is for example the case in path $y$ in Figure 4. Obviously, the path
segment following the starting point cannot be part of a cell that, in the
poset, is strictly below the cell containing the starting point, because then
the point and the segment cannot be connected to each other. A similar
situation holds for the end-point of the PL-path and the last segment of the
path leading to it. In that case the end-point should be in a cell that is in
the closure of the cell containing the last segment of the PL-path before
reaching the end-point, in other words,
$\pi(k-1)\,\widetilde{\succeq}\,\pi(k)$. Figure 4 illustrates this situation
in both path $x$ and path $y$ for different situations.

$B$$A$$D$$C$$F$$E$$x$ (a)  PL-path $\pi^{\prime}$

$B$$A$$D$$C$$F$$E$$AB$$BD$$BC$$AC$$CD$$DF$$DE$$CE$$EF$$BCD$$ABC$$DEF$$CDE$ (b)
Kripke Model $\mathcal{M}(\mathcal{X})$

Figure 6. On the left, a PL-path $\pi^{\prime}$ (in blue); on the right, the
corresponding $\pm$-path $\pi$ (again in blue). Only $\pi^{\prime}(0)$ belongs
to the simplex $AB$ and the path enters immediately into the cell
$\widetilde{ABC}$: this is possible since
$\widetilde{AB}\,\widetilde{\preceq}\,\widetilde{ABC}$. Likewise, the path
ends with a transition from the cell $\widetilde{BCD}$ to $\widetilde{D}$,
which is possible since $\widetilde{BCD}\,\widetilde{\succeq}\,\widetilde{D}$.
These are exactly the requirements on the first and last steps of a
$\pm$-path.

We are now ready to define the formal semantics of SLCS on
$\mathcal{M}(\mathcal{X})$.

[SLCS semantics on $\mathcal{M}(\mathcal{X})$] Consider
$\mathcal{M}(\mathcal{X})=\left\langle\widetilde{\mathrm{K}},\widetilde{\preceq},\widetilde{V}\right\rangle$.
Given $\widetilde{\sigma}\in\widetilde{\mathrm{K}}$, satisfaction
$\mathcal{M}(\mathcal{X}),\widetilde{\sigma}\vDash\phi$ over formulas $\phi$
is given by the following inductive clauses, where we let
$\left\llbracket\phi\right\rrbracket^{\mathcal{M}}$ denote the set
$\\{\widetilde{\sigma}\in\widetilde{\mathrm{K}}\,|\,\mathcal{M}(\mathcal{X}),\widetilde{\sigma}\vDash\phi\\}$:

$\begin{array}[]{lcl}\mathcal{M}(\mathcal{X}),\widetilde{\sigma}\vDash\top&\lx@intercol\text{always
holds}\hfil\lx@intercol\\\ \mathcal{M}(\mathcal{X}),\widetilde{\sigma}\vDash
p&\iff&\widetilde{\sigma}\in\widetilde{V}(p)\;\,\text{for }p\in\mathrm{AP}\\\
\mathcal{M}(\mathcal{X}),\widetilde{\sigma}\vDash\neg\phi&\iff&\mathcal{M}(\mathcal{X}),\widetilde{\sigma}\nvDash\phi\\\
\mathcal{M}(\mathcal{X}),\widetilde{\sigma}\vDash\phi\land\psi&\iff&\mathcal{M}(\mathcal{X}),\widetilde{\sigma}\vDash\phi\;\text{and}\;\mathcal{M}(\mathcal{X}),\widetilde{\sigma}\vDash\psi\\\
\mathcal{M}(\mathcal{X}),\widetilde{\sigma}\vDash\Box\phi&\iff&\forall\widetilde{\tau}\in\widetilde{\mathrm{K}}.\;\text{if}\;\widetilde{\sigma}\,\widetilde{\preceq}\,\widetilde{\tau}\;\text{then}\;\mathcal{M}(\mathcal{X}),\widetilde{\tau}\vDash\phi\\\
\mathcal{M}(\mathcal{X}),\widetilde{\sigma}\vDash\gamma(\phi,\psi)&\iff&\text{there
exists a $\pm$-path
$\pi:\\{0,\dots,k\\}\stackrel{{\scriptstyle\pm}}{{\to}}\widetilde{\mathrm{K}}$
such that}\\\
&&\pi(0)=\widetilde{\sigma},\,\pi(k)\in\left\llbracket\psi\right\rrbracket^{\mathcal{M}}\text{and
}\pi(\\{1,\dots,k-1\\})\subseteq\left\llbracket\phi\right\rrbracket^{\mathcal{M}}\end{array}$

The clauses for the Boolean operators and for $\Box$ are the standard
interpretation of modal formulas on Kripke models (and on topological spaces,
via the Alexandrov topology, see [BB07]). In the semantic clause for $\gamma$
we use $\pm$-paths since, as previously pointed out, these paths naturally
correspond to PL-paths and Lemma 7 allows us to restrict our attention to this
class of topological paths. We can give an example of this correspondence
based on Figure 6: the PL-path $\pi^{\prime}$ (on the left) witnesses that
$x\in\left\llbracket\gamma(r,\neg(r\vee g))\right\rrbracket^{\mathcal{X}}$,
and the corresponding $\pm$-path $\pi$ (on the right) witnesses that
$\widetilde{AB}\in\left\llbracket\gamma(r,\neg(r\vee
g))\right\rrbracket^{\mathcal{M}}$.

The following theorem shows that this correspondence holds for every formula
of the logic.

######  Theorem 9.

Let $\mathcal{X}=\left\langle P,\mathrm{K},V\right\rangle$ be a polyhedral
model and $x$ a point of $P$. Let $\sigma\in\mathrm{K}$ be the unique simplex
such that $x\in\widetilde{\sigma}$. For every formula $\phi$ of SLCS we have
$\mathcal{X},x\vDash\phi\iff\mathcal{M}(\mathcal{X}),\widetilde{\sigma}\vDash\phi$.

###  4.1. Geometric Model-checking Algorithm

We briefly present the main aspects of the geometric model checking algorithm
for SLCS over polyhedra. The model checking algorithm takes as inputs a Kripke
model $\mathcal{M}(\mathcal{X})$ of polyhedron $\mathcal{X}$ and an SLCS
formula $\phi$. The output is the satisfaction set
$\mbox{Sat}(\phi)=\\{\widetilde{\sigma}\in\widetilde{\mathrm{K}}\,|\,\mathcal{M}(\mathcal{X}),\widetilde{\sigma}\vDash\phi\\}=\left\llbracket\phi\right\rrbracket^{\mathcal{M}}$
of nodes in the model $\mathcal{M}(\mathcal{X})$ that correspond to the set of
cells in $\mathcal{X}$ that satisfy formula $\phi$, i.e. the algorithm is a
global model checking algorithm. The satisfaction set Sat is defined
recursively on the structure of SLCS formulas in the usual way (see for
example [BK08]). The algorithms for the Boolean operators are straightforward,
and thus omitted. The algorithm for the $\Box$ operator takes a set
$\mbox{Sat}(\phi)=\left\llbracket\phi\right\rrbracket^{\mathcal{M}}$ and
computes the corresponding satisfaction set
$\mbox{Sat}(\Box\phi)=\left\llbracket\Box\phi\right\rrbracket^{\mathcal{M}}=\\{\widetilde{\sigma}\in\mbox{Sat}(\phi)\,|\,\texttt{out}(\widetilde{\sigma})\subseteq\mbox{Sat}(\phi)\\}$,
where $\texttt{out}(\widetilde{\sigma})$ is the out-neighborhood of
$\widetilde{\sigma}$, i.e.
$\texttt{out}(\widetilde{\sigma})=\\{\widetilde{\tau}\,|\,\widetilde{\sigma}\,\widetilde{\preceq}\,\widetilde{\tau}\\}$.
We omit a detailed description of the algorithm, since it only involves basic
set-theoretic operations. We give a more detailed description of the algorithm
for the spatial reachability operator $\gamma$ that, given
$\mbox{Sat}(\phi)=\left\llbracket\phi\right\rrbracket^{\mathcal{M}}$ and
$\mbox{Sat}(\psi)=\left\llbracket\psi\right\rrbracket^{\mathcal{M}}$, computes
the satisfaction set
$\mbox{Sat}(\gamma(\phi,\psi))=\left\llbracket\gamma(\phi,\psi)\right\rrbracket^{\mathcal{M}}$.

The semantics of $\gamma$, as of Definition 6, is computed via a variant of
the flooding procedure that was already successfully employed in our previous
work on point-based spatial model checking algorithms [CLLM16a, CGL+15,
Gri16], retaining its asymptotic complexity (in the geometric case linear in
the number of nodes in $\mathcal{M}(\mathcal{X})$).

The pseudo-code with comments is reported in Algorithm 4.1. In the code, we
make use of the additional operators on cells out (previously introduced) and
in, the in-neighbourhood, defined as
$\texttt{in}(\widetilde{\sigma})=\\{\widetilde{\tau}\,|\,\widetilde{\sigma}\,\widetilde{\succeq}\,\widetilde{\tau}\\}$.
Both operators are lifted to sets in the obvious way. Therein, for brevity, we
call a $\pm$-path $\pi$ a “good” path if it is witnessing the formula
$\gamma(\phi,\psi)$, i.e. the path must map (0,1) to
$\left\llbracket\phi\right\rrbracket^{\mathcal{M}}$ and $\\{1\\}$ to
$\left\llbracket\psi\right\rrbracket^{\mathcal{M}}$. Figure 7 shows a step-by-
step example of an execution of the flooding algorithm described in Algorithm
4.1 for the property $\gamma(r,g)$, where $r$ denoted red and $g$ denotes
green, in the polyhedral model and corresponding Kripke model shown in Figure
7a. Recall that the definition of the reachability operator $\gamma$ states
that the first point of the paths passing by red and reaching green does not
need to be red itself, which explains why also point $B$ is included in the
results.

Pseudo-code for model checking the spatial reachability operator.

⬇

1 Input:
$\left\llbracket\phi\right\rrbracket^{\mathcal{M}},\left\llbracket\psi\right\rrbracket^{\mathcal{M}}$
sets of nodes of $\mathcal{M}(\mathcal{X})$ satisfying $\phi$ resp. $\psi$

2 Output: $\left\llbracket\gamma(\phi,\psi)\right\rrbracket^{\mathcal{M}}$
satisfaction set of nodes in $\mathcal{M}(\mathcal{X})$

3

4 // frontier: the points queued for the next iteration. Initialized with the
next to last points of a good path.

5 let frontier =
$\left\llbracket\phi\right\rrbracket^{\mathcal{M}}\cap\texttt{out}(\left\llbracket\psi\right\rrbracket^{\mathcal{M}})$

6

7 // flooded: all the points that are in the middle of a good path.

8 let flooded = frontier

9

10 while frontier$\neq\emptyset$:

11 let $\sigma$ = frontier.pop()

12 for every $\tau\in\texttt{in}(\sigma)\cup\texttt{out}(\sigma)$:

13 if $\tau\notin$flooded and
$\tau\in\left\llbracket\phi\right\rrbracket^{\mathcal{M}}$:

14 frontier.add($\tau$)

15 flooded.add($\tau$)

16

17 // result: the starting points of a good path.

18 let result = $\texttt{in}($flooded$)$

19

20 return result

$B$$A$$D$$C$

$B$$A$$D$$C$$AB$$BD$$BC$$AC$$CD$$BCD$$ABC$

(a) A polyhedral model $\mathcal{X}$ and its corresponding Kripke model
$\mathcal{M}(\mathcal{X})$.

$B$$A$$D$$C$

$B$$A$$D$$C$$AB$$BD$$BC$$AC$$CD$$BCD$$ABC$

$\begin{array}[]{ll}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{frontier}}&=\\{AC,BC,ABC\\}\phantom{A,AB}\end{array}$

(b) Initialization of frontier (lines 4-5).

$B$$A$$D$$C$

$B$$A$$D$$C$$AB$$BD$$BC$$AC$$CD$$BCD$$ABC$

$\begin{array}[]{ll}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{frontier}}&=\\{A,AB\\}\\\
{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{flooded}}&=\\{AC,BC,ABC\\}\phantom{A,AB}\end{array}$

(c) Initialization of flooded and first flooding iteration (lines 7-15).

$B$$A$$D$$C$

$B$$A$$D$$C$$AB$$BD$$BC$$AC$$CD$$BCD$$ABC$

$\begin{array}[]{ll}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{frontier}}&=\emptyset\\\
{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{flooded}}&=\\{A,AB,AC,BC,ABC\\}\end{array}$

(d) Second flooding iteration (lines 10-15).

$B$$A$$D$$C$

$B$$A$$D$$C$$AB$$BD$$BC$$AC$$CD$$BCD$$ABC$

$\begin{array}[]{ll}\mathtt{flooded}&=\\{A,AB,AC,BC,ABC\\}\\\
{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{result}}&=\\{A,B,C,AB,\\\
&\hskip 50.00008ptAC,BC,ABC\\}\end{array}$

(e) Computation of result (lines 17-18).

Figure 7. An example of application of the algorithm described in Algorithm
4.1. Subfigure 7a depicts a polyhedral model $\mathcal{X}$ (on the left) and
its corresponding Kripke model $\mathcal{M}(\mathcal{X})$. Subfigures from 7b
to 7e depict the steps performed on $\mathcal{M}(\mathcal{X})$ to compute the
satisfaction set $\mbox{Sat}(\gamma(r,g))$, with reference to the pseudo-code
in Algorithm 4.1. For each subfigure the value of the relevant variables at
the end of the computation step are indicated and illustrated in corresponding
colours in both models (blue for frontier, orange for flooded and purple for
result).

We include a concise proof of the correctness of the algorithm.

######  Proof 4.1 (Correctness, sketch).

To be consistent with the comments in the pseudo-code, we keep calling a
$\pm$-path $\pi:\\{0,\dots,k\\}\to\widetilde{\mathrm{K}}$ witnessing the
satisfaction of $\gamma(\phi,\psi)$ a “good” path.

First, notice that we can divide a good path into three parts: the initial
point $\pi(0)$, the points on the central segment $\pi(\\{1,\dots,k-1\\})$ all
satisfying $\phi$ and the final point $\pi(k)$ satisfying $\psi$. To compute
the set $\left\llbracket\gamma(\phi,\psi)\right\rrbracket^{\mathcal{M}}$ we
work “backwards” from an initial set of nodes that satisfy $\phi$ and that
have an outgoing edge to a node satisfying $\psi$. So, first, we compute the
set
$C:=\left\llbracket\phi\right\rrbracket^{\mathcal{M}}\cap\texttt{out}(\left\llbracket\psi\right\rrbracket^{\mathcal{M}})$
(the cells corresponding to nodes with index $\pi(k-1)$ on some good path
$\pi$). Then we use a standard flooding procedure to build the set $D$ of the
nodes of the graph that are connected to $C$ via a non-directed path, i.e.
abstracting from the direction of the edges, passing only through nodes
satisfying $\left\llbracket\phi\right\rrbracket^{\mathcal{M}}$ (these
correspond to the cells of the form $\pi(j)$, with $j=1,\ldots,k-1$, for any
good path $\pi$ in the polyhedron). Finally we compute the set
$\left\llbracket\gamma(\phi,\psi)\right\rrbracket^{\mathcal{M}}=\mbox{${\texttt{in}}(D)$}$
(the cells corresponding to the initial nodes of good paths, i.e. $\pi(0)$ for
any good path $\pi$).

###  4.2. Computational Complexity

In what follows, we indicate by $n$ the number of cells of
$\widetilde{\mathrm{K}}$ and by $d$ the dimension of $\mathrm{K}$, that is,
the maximum dimension of a simplex $\sigma$ in $\mathrm{K}$. Therefore, the
number of nodes of the encoding $\mathcal{M}(\mathcal{X})$ is $n$. Each
simplex $\sigma$ having dimension $d_{\sigma}\leq d$ has $d_{\sigma}+1$
vertices. Furthermore, in the graph encoding $\widetilde{\mathrm{K}}$, the in-
neighbourhood of each $\widetilde{\sigma}\in\widetilde{K}$ is precisely the
set of the proper faces of $\sigma$, having cardinality $2^{d_{\sigma}+1}-1$.
By this, the total number of edges of $\mathcal{M}(\mathcal{X})$ is at most
$n\cdot(2^{d+1}-1)$. We let $N$ to be the size of this encoding, that is, the
sum of the number of nodes and edges, which is at most equal to
$n+n\cdot(2^{d+1}-1)=n\cdot 2^{d+1}$.

Note that the complexity of our encoding grows exponentially in $d$ if $d$ is
not fixed. The design space for algorithms that scale better with $d$,
possibly exploiting specialised data structures (see, e.g., the recent work
[BM14]) will be explored in future research, depending on the considered use
case. In the case under consideration (i.e., 3D meshes) we have the fixed
dimension $d=3$. Therefore the “exponential” contribution of $d$ to the
computational complexity becomes a constant. In other words, when the
dimension $d$ is fixed, as in 3D meshes, the size of
$\mathcal{M}(\mathcal{X})$ is of order $\mathcal{O}(n)$.

Note that the flooding procedure (Algorithm 4.1) has linear computational
complexity in the number of nodes and edges of $\mathcal{M}(\mathcal{X})$,
that is, $N$. The computation of the Boolean operators and of the
$\Box$-operator are also linear in $N$. As in [CLLM16a], since each subformula
is checked independently from the others, the asymptotic computational
complexity of the model checking algorithm is of order $\mathcal{O}(N\cdot
h)$, where $h$ is the cardinality of the set of subformulas of the SLCS
formula to be checked.

As remarked before, once the dimension $d$ of the image is fixed the
exponential contribution of $d$ to the computational complexity is negligible
and therefore the total complexity of the spatial model checking algorithm is
of order $\mathcal{O}(n\cdot h)$.

Finally, we briefly address the complexity of the encoding. In the current
prototype implementation of the model-checking algorithm (see Sect. 5 for
further details), the input polyhedron is described by a list of $n$ simplexes
with maximum dimension $d$, each one being represented by a list of vertices.
To compute the Kripke frame of Definition 4 from this description, an explicit
enumeration is performed of the subsets of each simplex, incrementally
building the arrays of out- and in-neighborhoods. This results in a time
complexity in $\mathcal{O}(N)$, which becomes $\mathcal{O}(n)$ once the
dimension $d$ is fixed. Therefore, for $d$ fixed, the total complexity
(encoding plus model checking) is in $\mathcal{O}(n\cdot h)$.

##  5\. PolyLogicA: a Model Checker for Polyhedra

Based on the theory and the model checking algorithm presented in Section 4,
we developed the prototype model checker PolyLogicA: a _Polyhedral Logic-based
Analysis tool_. The model checker is implemented in the functional language
FSharp.999See https://www.fsharp.org PolyLogicA is Free and Open Source
Software, distributed under the Apache 2.0 license.101010The tool is currently
available in a branch of the main VoxLogicA repository, see
https://github.com/vincenzoml/VoxLogicA.

Currently PolyLogicA represents a polyhedral model $\mathcal{X}$ through an
explicit encoding of the Kripke model $\mathcal{M}(\mathcal{X})$ according to
Definition 4. The encoding is stored as a graph having the cells as nodes and
with the covering relation of $\widetilde{\preceq}$ as the edge relation. The
current implementation stores the out-neighborhood and the in-neighborhood of
each node $\sigma$ in two separate arrays, allowing access in constant time to
these sets.

###  5.1. Functional description

A PolyLogicA specification consists of a text file that can make use of four
commands: let, for declaring functions and constants; import, for importing
libraries of such declarations; load, to specify the file to be loaded as a
model; save, to specify the logic formulas that need to be computed, and
saved, possibly making use of previous let declarations.

Models are required to be based on a fixed simplicial complex. The given
simplicial complex constitutes the subspace of $\mathbb{R}^{d}$ that is
explored by the tool. Thus, one needs to explicitly include, in the input
model, the “environment” in which the objects live. As an example, consider
the simplicial complex depicted in Figure 2. The semantics of the formula
$\phi=g\lor r\lor b$ is indeed the set of points $S$ that belong to the whole
coloured triangle (made up of four smaller ones).

The file describing the input model uses a custom json-based111111See
https://www.json.org/. format. The information contained in the file consists
of: a list $p$ of $d$-dimensional vectors, denoting the coordinates of the
0-cells of the polyhedron; a list of atomic proposition identifiers; a list of
simplexes. Each simplex is specified by the list of the indexes of its
vertices in $p$, and its specification also contains the list of atomic
propositions holding at the cell corresponding to the simplex.

Logic formulas are just a concrete syntax for SLCS as presented in Section 3.
Currently, PolyLogicA does not implement additional extra-logical operators
(contrary to VoxLogicA, which also implements imaging primitives). PolyLogicA
is in spirit a _global, explicit-state_ model checker, that is, the set of
simplexes satisfying a given formula is computed and returned at once. The
output of the model checker is a list, in json format, containing an element
for each formula $\phi$ that the specification requires to be checked. Each
element of such list contains in turn a list representing the truth values of
$\phi$ at each point (cell) of the input model. Finally, a simple 3D, web-
based visualizer has been implemented along with the prototype (see the
screenshot in Figure 13e), which will be refined in future work.

###  5.2. Implementation Details

The current version of PolyLogicA has been implemented sharing part of the
code base for point-based spatial model checking with VoxLogicA. PolyLogicA
inherits from its parent tool the multithreaded, memoizing computation engine,
and the parser for the input language of the tool. Basically, after expanding
let bindings, each formula is converted into a _directed acyclic graph_ where
nodes are _tasks_ , and arcs are _dependencies_. Each task is a basic logical
primitive, to be applied to specific arguments. Task $A$ depends upon task $B$
if and only if the result of $B$ is an argument of $A$. The implementation
guarantees that, while being constructed, such data structure is kept
_minimal_ in the sense that the same primitive on the same arguments will
never be added twice to the graph, thus implementing _memoization_ at a
syntactic level, without the need to hash possibly large sets of states at
run-time. After having been constructed, the task graph is executed in
parallel as much as possible, exploiting the available CPU cores.

###  5.3. A Visualiser for PolyLogicA

In addition to the polyhedra model checker we developed PolyVisualiser, a
prototype polyhedra visualiser. The user interface of the visualiser is shown
in the screenshots in Figure 8. The visualiser is an interactive tool with
which polyhedra can be explored from different perspectives by means of the
mouse or an other pointing device. The tool allows to zoom in and out on the
visualised model, to translate it rigidly and to turn it around a fixed point.
The main purpose of the visualiser is to inspect the result of spatial
properties that were checked using PolyLogicA. From a pop-up menu, shown on
the right of the screenshot, a property can be selected and from further menu
items one can select the way in which the results of the evaluation of the
property will be visualised. For example, in the screenshot in Figure 8 the
cells that satisfy the selected property are shown in green and the cells that
do not satisfy the property are shown in red. Also the degree of transparency
of the colours can be set, thus facilitating the inspection of the interior of
3D objects. Cells that are points or line segments or triangles are coloured
in a direct way. To facilitate inspection of the solid components, being them
covered by triangles, tetrahedra are reduced in size and coloured without
transparency. Moreover, the relative size of tetrahedra can be manipulated
real-time through the appropriate control panel.

In the following sections PolyVisualiser is used to illustrate two examples of
realistic size. In those examples, rather than using the colour green for
cells in the polyhedron that satisfy the selected formula and the colour red
for those cells that do not satisfy the formula, we will use different levels
of transparency while retaining the original colour of the cells. Cells that
satisfy the selected property are shown in their original colour but made less
transparent (i.e. more opaque) than cells that do not satisfy the property.
This way the contours of the complete model are preserved and may serve as a
visual reference framework for the interpretation of the 3D spatial model
checking results which pop-out as opaque objects as shown in Figure 11.

(a)

(b)

(c)

Figure 8.  Visualiser for PolyLogicA: Model of a simple cube showing cells
satisfying the atomic propositions “p” and “q” in green ((8a) and (8b),
respectively) and model checking result (in green) of cells satisfying “grow p
with q” (8c).

###  5.4. Proof of Concept Experiments

In order to obtain a first impression of the actual feasibility of our (first-
in-its-kind) geometric model checking approach we present two examples: one
involving the analysis of a 3D maze (generated by the authors) and one
involving the analysis of an existing mesh model of the anatomy of the human
body. Both examples are analysed with PolyLogicA and we show screenshots of
the PolyVisualiser to illustrate the results. The results are also made
available
online121212http://ggrilletti2.scienceontheweb.net/polyVisualizer/polyVisualizer_static_maze.html
for inspection in an interactive way.

####  5.4.1. A 3D Maze

The first example concerns a 3D maze131313The maze has been generated by the
authors.. The maze, shown in Figure 10a, consists of “rooms” that are
connected by “corridors”. The rooms come in four colours: white, black, green
and one room in red. The green rooms are all situated at the outer boundary of
the maze and represent the surroundings of the maze that can be reached via an
exit. The white, black and red rooms, and related corridors, are situated
inside the cube and form the maze itself. Figure 10b shows all the white and
black rooms. Figure 10c shows the red room situated at the centre of the maze.
All corridors between rooms are dark grey. The valid paths through the maze
should only pass by white rooms (and related corridors) to reach a green room
without passing by black rooms or corridors that connect to black rooms.

Typical spatial queries or properties that are of interest for such a maze
are:

  1. Q1:

Which are the white rooms and connecting corridors from which one can reach a
green room (i.e. an exit) without having to pass by a black room? Show those
white rooms, the related corridors and the green exit.

  2. Q2:

Which are the white rooms and connecting corridors from which both a green
room (exit) and a red room can be reached, without having to pass by black
rooms (and related corridors)? Show those white rooms, the related corridors,
the green exit and the red room.

  3. Q3:

Which are the white rooms (and related corridors) from which it is not
possible to reach a green room without having to pass by a black room?

Figure 9 shows the specification of the above properties in a syntax close to the spatial logic introduced in Section 3. This syntax is shared with that of VoxLogicA (see [CBLM21] for a tutorial) and is mostly self-explanatory. The boolean operators are | (or), & (and), ! (not). The spatial reachability operator $\gamma$ is denoted by the keyword through. The surround operator sur is implicitly defined in terms of the operator through according to its definition provided in Section 3. In the first line of Figure 9 the model file is loaded. In lines 4 to 7 atomic propositions are defined for the simplicial cells of the various coloured rooms. In line 8 the atomic proposition of cells belonging to corridors is defined. These definitions make direct reference to the information stored in the elements of the model file, in json format, representing the cells of the polyhedron model. In particular, ap denotes an atomic proposition associated with such elements.

In line 11 a simple application of these atomic propositions is defined. The
property blackOrWhite is satisfied by all cells of black rooms and those of
white rooms. The result of this property can be saved (as shown in line 44)
and used by PolyVisualiser to visualise the outcome. The saved file
essentially consists of a list of booleans indicating for each cell whether it
satisfies the property. The result is shown in a screenshot of the visualiser
in Figure 10b where the cells that satisfy the property are opaque and all the
others almost transparent. Similarly, in Figure 10c the cells that satisfy the
atomic proposition red are shown.

Lines 14 to 20 define properties to distinguish different kinds of corridors.
In particular, corridors that connect white rooms (corridorWW), those between
white and green rooms (corridorWG), those between white and red rooms
(corridorWR) and those between white and black rooms (corridorWB). These will
turn useful in the specification of the three properties Q1, Q2 and Q3. A
point satisfies corridorWW if it (lays in a cell that) belongs to a corridor
(i.e. a cell satisfying corridor) and from which only white rooms can be
reached via the corridor itself (i.e. only cells satisfying white but neither
green, nor black, nor red can be reached from cells of the corridor).

In lines 24 and 27 property Q1 is specified as whiteToGreen. It is expressed in terms of the through-operator ($\gamma$). It says that we want all (cells of) white rooms, corridors between white rooms and corridors between white and green rooms by which one can reach a green room, i.e. without passing by black rooms or corridors connected to black rooms. If we also want to include the green room that is being reached in the set of results we have to add it, as is done in line 27 in connWG, leading to all cells satisfying whiteToGreen and the (cells of) green rooms from which cells satisfying whiteToGreen can be reached. Cells satisfying connWG are shown in their original opaque colour in Figure 11a. Cells that do not satisfy the property are shown in a transparent manner. Note that, in general, the through(x,y)-operator would also admit satisfaction by cells that are adjacent to those satisfying x in that case, as shown in the example of Figure 3b. In the model of the maze rooms and corridors do not have such adjacent cells. However, in general one could consider the use of (x | y) & through(x,y) to make sure that only cells satisfying at least x or y are part of the result. The choice for the particular definition of through (and $\gamma$) has been motivated by the fact that it poses minimal restrictions. More restricted variants can be easily defined based on through. This would not be the case if one opts for a less basic definition of through.

In line 30 property Q2 is specified as connRWG. In this case we are looking
for white rooms and related corridors from which both a green room and a red
one can be reached, and we also want to include in the result such red and
green rooms. The specification makes use of connWG and allows passing by
corridors connecting white rooms to red rooms corridorWR. The result is shown
in Figure 11b.

In line 34 property Q3 is specified as whiteNoGreen. In this case we are
looking for white rooms and related corridors from which it is not possible to
reach a green room without passing by a black room. This can be specified as
white rooms and corridors between white rooms that are not satisfying
whiteToGreen (i.e. property Q1 above). The same property could also be
specified in an alternative way making use of the surround operator sur
defined in lines 37-38. In that case these cells are characterised as those
belonging to white rooms and corridors between white rooms that are completely
surrounded by corridors leading only to black rooms in specification
whiteSblack in line 41. The result is shown in Figure 11c.

Finally, in line 44 an example is shown of saving a particular result, in this
case that of property blackOrWhite. Saving the other results can be performed
in a similar manner and is not shown in the specification.

⬇

1load model = "mazeModel.json"

2

3// Atomic propositions for rooms and corridors

4let green = ap("G")

5let white = ap("W")

6let black = ap("B")

7let red = ap("R")

8let corridor = ap("corridor")

9

10// Black or White rooms

11let blackOrWhite = black | white

12

13// Corridors: white-to-white, white-to-green, white-to-red, white-to-black:

14let corridorWW = through( corridor, white ) &

15 !through( corridor, green | black | red )

16let corridorWG = through( corridor, white ) &

17 through( corridor, green )

18let corridorWR = through( corridor, white ) &

19 through( corridor, red )

20let corridorWB = through( corridor, white ) &

21 through( corridor, black )

22

23// Q1: White rooms from which a green room can be reached not passing by
black rooms

24let whiteToGreen = through((white | corridorWW | corridorWG), green)

25

26// as Q1 but including the green room that is reached

27let connWG = whiteToGreen | through(green,whiteToGreen)

28

29// Q2: White rooms from which both a red and a green room can be reached not
passing by black rooms

30let connRWG = through((connWG | corridorWR), red) |

31 through((red | corridorWR), connWG)

32

33// Q3: White rooms with no path to green rooms and their connecting
corridors

34let whiteNoGreen = (white | corridorWW) & !whiteToGreen

35

36// Surround operator in terms of reach in the polyhedra setting

37let reach(x,y) = x | through(y,x)

38let sur(x,y) = x & !reach(!(x | y),!y)

39

40// Q3(alternative): White rooms and their connecting corridors surrounded
only by corridors to black rooms

41let whiteSblack = sur((white | corridorWW), corridorWB)

42

43// Save the result for property blackOrWhite

44save "blackOrWhite" blackOrWhite

Figure 9.  PolyLogicA specification of some spatial properties for the 3D maze
model.

(a)

(b)

(c)

Figure 10.  3Dmaze (10a), black and white (10b) and red rooms (10c) in the 3D
maze.

(a) Q1

(b) Q2

(c) Q3

Figure 11.  Spatial model checking results of the properties in Figure 9 for the 3D maze of Figure 10. Q1: White rooms and their connecting corridors from which a green room can be reached not passing by black rooms, including the green room that is reached (connWG); Q2: White rooms and their connecting corridors from which both a red and a green room can be reached not passing by black rooms (connRWG); Q3: White rooms and their connecting corridors with no path to green rooms (whiteNoGreen or equivalently whiteSblack). | Number of tasks |  Check (millisecs.) |  Total time (millisecs.)
---|---|---|---
Property Q1 connWG | 24 | 200 | 5,450
Property Q2 connRWG | 31 | 250 | 5,500
Property Q3 whiteNoGreen | 25 | 100 | 5,350
All properties in one run | 34 | 300 | 5,550
Table 1.  PolyLogicA performance results (rounded to the nearest multiple of
50ms) of the evaluation of the specification in Figure 9 on three properties
of the 3D mesh of the maze shown in Figure 10. The size of the model is
147,245 cells. The time spent in parsing the input file (circa 12 megabytes)
is about 4 seconds, whereas building the Kripke structure takes about 1
second. If all properties are evaluated in the same specification, the
execution time is just slightly above the maximum one, since the machine has 8
physical cores, and PolyLogicA evaluates independent properties in parallel
needing less than 8 cores for the maze example.

Table 1 shows information on the model checking time for the properties Q1-Q3
individually and when evaluated all together. Also the total time is shown
that includes the parsing of the model, the generation of the Kripke model and
the actual model checking time. It is easy to see that most of the time goes
in preparing the model (4 seconds for parsing and 1 second for building the
Kripke model) rather than the actual model checking which only takes a few
hundred milliseconds. This is very encouraging, because it means that the
actual model checking procedure is not the bottleneck and we are confident
that more efficient parsing and Kripke model generating procedures can be
found than the non-optimised ones we used for this first proof-of-concept set-
up. Work on such optimisations is planned as part of future work. Note also
that it is possible to verify several properties at once in which case the
Kripke structure needs to be generated only one time. In future work an option
could be to enable saving and loading such Kripke structures once they have
been generated in order to reduce the total time needed for analysis. The
evaluation was performed on a desktop machine equipped with an Intel core i9
9900k cpu and 32Gb of RAM.

Even though the 3D maze example seems simple, the fact that examples like this
can be generated in various forms makes it a promising example for a future
benchmark. The example lends itself for endless variations in size and shape
of the maze, introducing “holes” or forms of “rings”. Setting up a suitable
benchmark for geometric model checking of polyhedra is planned as part of
future work.

####  5.4.2. Digital Anatomy

In the second example we apply PolyLogicA on an existing 3D mesh from the
medical domain with the aim to assess the feasibility of the geometric model
checking approach on existing meshes of realistic size. The mesh visualised in
Figure 13LABEL:sub@subfig:3dimage consists of about 1.5 milion simplicial
cells. A custom converter has been implemented to obtain a model file in json
format from the input obj mesh141414 _Wavefront obj_ is a widely used file
format for 3D meshes. See https://en.wikipedia.org/wiki/Wavefront_.obj_file ;
the atomic propositions used are strings of the form "Ci" for C in
$\\{r,g,b\\}$ (standing for _red_ , _green_ , _blue_) and i an integer between
$0$ and $3$. Each such atomic proposition denotes the intensity level at each
point of the red, green or blue component of the colour vector associated to
the simplicial cell, with intensities quantised to four discrete target levels
indicated by the integers.

Based on such atomic propositions, it is possible to encode spatial properties
involving approximations of the colour gradients151515This type of mesh has
colours associated to vertices, and no textures. In future versions of the
tool we plan to encode colour intervals in the logic, in a similar way as has
been done in the parent tool VoxLogicA. However, this is ongoing work, as the
presence or colours, textures, materials, and so on, may depend upon the
chosen file format of the mesh and will require further investigation. that
are visible in the rendered mesh. Using the specification of spatial
properties shown in Figure 12, we have checked the properties heart (Figure
13LABEL:sub@subfig:hearth), spleen (Figure 13LABEL:sub@subfig:spleen), vein
(Figure 13LABEL:sub@subfig:someVeins), and selectedVein (Figure
13LABEL:sub@subfig:selectedVein). The syntax of the specification is the same
as the one explained in the 3D maze example. Some definitions (e.g.
spleenWithError) need to handle errors in the segmentations due to the usage
of quantised colours leading to somewhat loose approximations; this is no
problem for our purposes, as in this example we merely want to illustrate a
first feasibility test and performance of the tool on existing meshes. After
loading the model file (line 1), in the specification first some areas are
identified based on their approximative colour (lines 3–8). In particular, a
blueish colour is defined as a combination of the blue and red intensity
levels. The core of the spleen can be found in a similar way, as well as an
over-approximation of the spleen by a relaxation of the constraint on the
level of red. Heart, spleen or kidneys are identified by a particular
combination of the levels of red and green.

This simple first approximation is then used to identify the individual organs
exploiting, for example, the knowledge that veins are blueish and leading to
the core of the spleen (line 10, definition vein). The spleen itself is first
approximated by spleenOver, an over-approximation of the spleen that touches
the veins, but may have some overlap with the heart. Recall here that the
through-operator may be satisfied by some points (cells) that do not satisfy
spleenOver (see the example in Figure 3b).

The heart is specified as that part of heartOrSpleenOrKidneys that is not part
of the over-approximated spleen that can reach a vein spleenWithError, but can
reach a vein by itself. Subsequently, the spleen can be characterised more
precisely by excluding the points belonging to the heart (line 12). Finally,
the reachability operator through is used (line 14) to identify the veins that
reach the spleen but not the heart.

We have tested the specification using PolyLogicA on a desktop machine
equipped with an Intel core i9 9900k cpu and 32Gb of RAM161616The memory limit
is actually never hit, even with lower amounts of available RAM on other
machines.. Three models have been used: the original one, and two versions
that have been obtained by simplifying the original mesh, using a built-in
algorithm in MeshLab [CCC+08]. The number of tasks executed (the nodes of the
directed acyclic graph described in Section 5.2, that is, the cardinality of
the set of subformulas) is $33$. Table 2 reports the model size and the
execution time, broken down into parsing of the json model file, computing the
Kripke structure, and actual model checking. Note that parsing a terse textual
format for such large objects is time consuming, and ought to be replaced in
future work by functions to load and save more specific mesh-based file
formats. However, in the meantime, we find these results particularly
encouraging, as the model checking times are quite small, and would permit to
check many more formulas in a single run, thus compensating for the time
needed to generate the Kripke structure.

|  Size (cells) |  Parse (secs.) |  Kripke (secs.) |  Check (secs.) |  Total (secs.)
---|---|---|---|---|---
Small | 91,771 | 2.5 | 0.5 | 0.3 | 3.3
Medium | 591,269 | 15 | 7 | 1.6 | 23.6
Full-size | 1,587,430 | 44 | 32 | 5 | 81
Table 2.  PolyLogicA performance results of the evaluation of the
specification in Figure 12 on three variants of the 3D Medical mesh shown in
Figure 13a.

⬇

1load model = "RAJA2.json"

2

3let blueish = (ap("b3")|ap("b2")) & (ap("r0")| ap("r1"))

4let cyan = ap("r2") & (ap("g0"))

5

6let spleenCore = ap("b3") & (ap("r1")) & ap("g1")

7let spleenOver = ap("b3") & (ap("r2")|ap("r1")) & ap("g1")

8let heartOrSpleenOrKidneys = ap("r2") & (ap("g1"))

9

10let vein = through(blueish,spleenCore)

11let spleenWithError = (spleenOver | through(spleenOver,vein))

12let heart = through(heartOrSpleenOrKidneys & (not(spleenWithError)),vein)

13let spleen = spleenWithError & (!heart)

14let selectedVein = vein & (!through(vein,heart))

Figure 12.  Specification of the spatial properties to produce the results
shown in Figure 13.

Future work will include the implementation of a fast loader for 3D meshes, in
order to eliminate the parsing of (very large) model files in json format, and
the optimisation of the translation from simplicial complexes to Kripke
models, which currently exploits purely-functional data structures for ease of
prototyping. We note in passing that the intermediate Kripke model may be
cached, for speeding up the execution of multiple analyses on the same model.

Future work will also include further experiments with more complex spatial
formulas and different kinds of meshes with the aim to generate a basic
benchmark suitable for future comparisons of performance.

(a)  3D medical image

(b)  Heart (red)

(c)  Spleen (brown)

(d)  Veins (violet)

(e)  Selected vein (violet)

Figure 13.  (13a) A 3D medical illustration, courtesy of www.sketchfab.com
(copyright: COEUR et vaissaaux by Chair_Digital_Anatomy – The Unesco Chair of
digital anatomy (Paris University) – is licensed under Creative Commons
Attribution, see https://creativecommons.org/licenses/by/4.0/legalcode),
visualized using MeshLab [CCC+08]. PolyLogicA is used to segment the heart
(13b) shown in red, spleen (13c) shown in brown, and some veins (13d) shown in
violet, and then to segment a specific vein (the one that reaches the spleen)
using a reachability predicate (13e), also shown in violet. In each image, the
non segmented parts are shown as mostly transparent cells.

##  6\. Simplicial Bisimilarity

A further, more theoretically inspired, direction of research aiming at
increasing the performance of geometric spatial model checking is to exploit
suitable spatial bisimilarity to reduce the models. The main idea is to
identify areas that satisfy the same spatial properties, before applying model
checking. Similar approaches have been exploited in traditional model checking
techniques, based on bisimilarity for modal logics (see e.g. [VB84]).

As a first step into this direction, in this section we characterise logical
SLCS equivalence via _simplicial bisimilarity_. Recall the results summarised
in [APvB07], defining bisimilarity for topological spatial logics, so that any
two points are bisimilar if and only if they are logically equivalent.

To account for the addition of the reachability operator in the logical
language, the definition of bisimilarity makes use of the point-wise lifting
of a relation to a path, defined in a formal way below. In the following, fix
a model $\mathcal{X}:=\left\langle P,\mathrm{K},V\right\rangle$.

Given a relation $R\subseteq P\times P$, let the _extension of $R$ to paths_
be the binary relation between paths $\hat{R}$, such that
$\pi_{1}\hat{R}\pi_{2}$ if and only for all $t\in[0,1]$ we have
$\pi_{1}(t)R\pi_{2}(t)$.

[Simplicial bisimilarity] A binary relation $\sim\,\subseteq P\times P$ is a
_simplicial bisimulation_ if and only if for all $x,y$ with $x\sim y$:

  1. (1)

for all $p\in\mathrm{AP}$, $x\in V(p)\iff y\in V(p)$;

  2. (2)

for each _simplicial_ path $\pi_{x}$, with $\pi_{x}(0)=x$, there is a
simplicial path $\pi_{y}$ with $\pi_{y}(0)=y$, and $\pi_{x}\hat{\sim}\pi_{y}$;

  3. (3)

for each _simplicial_ path $\pi_{y}$, with $\pi_{y}(0)=y$, there is a
simplicial path $\pi_{x}$ with $\pi_{x}(0)=x$, and $\pi_{x}\hat{\sim}\pi_{y}$.

The largest simplicial bisimulation, if it exists, is called _simplicial
bisimilarity_.

The notion of simplicial bisimulation resembles that of stuttering equivalence
for process calculi [BCG88, DV95, GJKW17] but it should be noted that it is
defined for continuous structures. In the following, we state the three main
facts that conclude this section. Detailed proofs can be found in Appendix A.

######  Theorem 10.

Logical equivalence is a simplicial bisimulation.

######  Theorem 11.

Each simplicial bisimulation is included in logical equivalence.

######  Corollary 12 (of Theorem 10 and 11).

In a polyhedral model, the largest simplicial bisimulation always exists, and
it coincides with logical equivalence.

Consider the polyhedral, $1$-dimensional model with cells the points $x=-1$,
$y=0$, $z=1$, and the open segments $s=(-1,0)$ and $t=(0,1)$. Consider the set
of atomic propositions $\\{a,b\\}$. Let $V(a)=\\{y\\}$ and $V(b)=z$. According
to topo-bisimilarity [BB07], which characterises the modal fragment of our
language, all the points in $s\cup t$ are equivalent, as there is no modal
formula telling $s$ and $t$ apart. However, if $\gamma$ is added to the
picture, let $\phi=\gamma(\lnot a,b)$. The points of $s$ do not satisfy
$\phi$, but the points of $t$ do. No point of $s$ is bisimilar to a point of
$t$. In Figure 14, we propose a simple illustration of the concept of
simplicial bisimilarity. Note how the two presented paths pass through a
different number of equivalent cells (in a way akin to classical “stuttering”
forms of bisimilarities for process calculi [BK08]).

(a)  Model

(b)  Bisimulation

x (c)  Path 1

y (d)  Path 2

Figure 14.  An example of bisimilarity. 14a) Model with atomic propositions in
green and red. 14b) bisimilarity, encoded via colours (points of the same
colour are bisimilar). 14c) A point $x$ and a simplicial path starting from
$x$. 14d) Another point $y$, bisimilar to $x$, and a simplicial path starting
from $y$. The two paths are, in turn, bisimilar; note that these paths are
also piecewise linear. The two paths cross a different set of cells, and have
a different number of segments.

##  7\. Conclusions and Future Work

We proposed an interpretation of the spatial logic SLCS in continuous space
using models based on polyhedra. SLCS is a spatial logic stemming from
topological modal logics enhanced with reachability. We developed a polyhedral
semantics for SLCS introducing a finite state relational Kripke model for any
given polyhedral model. Such Kripke models represent the face-relation between
the simplicial complexes of a polyhedron. We showed that such Kripke models
provide a full logical invariant for the polyhedral model with respect to
SLCS. Based on these theoretical results we presented a novel spatial model
checking algorithm for the verification of SLCS properties of polyhedral
spaces, and in particular for the reachability operator of SLCS. First
applications of the prototype polyhedral model checker PolyLogicA on examples
of realistic size showed very encouraging results for the feasibility of this
novel type of spatial model checking requiring only about 5 seconds for the
actual model checking task of a full-size model consisting of circa 1.5
million of simplicial cells.

Future work will span several theoretical and applied directions. Regarding
bisimilarity, by looking at the _simplicial_ paths that are used in Definition
6, one may wonder what logical operators (alternative to $\gamma$), and in
what classes of models, can be characterised by lifting the restrictions or
completely changing the kind of paths that are used therein. Furthermore,
bisimilarity hints at _minimization_ in order to reduce the complexity of the
analysis. The preliminary results presented in [CLMdV20], including the tool
_MiniLogicA_ could be useful in this research direction. Note that the
quotient mapping each simplex in $P$ to a point in $\widetilde{\mathrm{K}}$ in
Definition 4 is an _open map_ , thus it preserves and reflects logical
equivalence of the modal fragment of our language; additionally, as shown in
Section 6, it preserves and reflects logical equivalence of the full language,
thus simplicial bisimilarity. Not all open maps do so (just consider, e.g. the
quotient with respect to classical modal logical equivalence). In future work,
we plan to formalise the conditions on an arbitrary open map that make it
preserve and reflect simplicial bisimilarity. The relationship between spatial
logics and temporal logics, and related bisimilarities [KdR97] is also of
interest, and in particular, comparing path-based spatial notions such as
simplicial bisimilarity, to the so-called _stuttering_ equivalences, and their
associated minimisation algorithms (see e.g. [BCG88, GJKW17]).

Spatio-temporal model checking in the style of [Gri16, CGL+15] is a planned
future development, the simplest case being the one where the underlying
polyhedron does not change over time, and only the valuation of atomic
propositions depends upon the temporal state of a system. More complex forms
of dynamic spatial structures where the underlying polyhedron evolves over
time are also of interest.

A promising application of PolyLogicA is fully automated, declarative analysis
of 3D _meshes_. Clearly, we foresee 3D medical imaging to be a promising
landscape for future applications. Furthermore, note that 3D meshes play a
central role in several other fields, including architecture and computer-
aided design (CAD), geographic information systems (GIS), see e.g. [BBJ+20],
or the entertainment industry (consider 3D games or 3D animation movies), in
education and in scientific visualisation.

Implementation-wise, _GPU computing_ could provide a computational boost to
PolyLogicA. See [BCG21b] for a GPU implementation of the parent tool
VoxLogicA. Finally, a user interface could be useful to explore large
datasets, and to better visualise the interpretation of logic formulas,
possibly exploiting results in [BMÖ19] for validation.

## References

  * [ABGM21] Sam Adam-Day, Nick Bezhanishvili, David Gabelaia, and Vincenzo Marra.  Polyhedral completeness of intermediate logics: the nerve criterion.  CoRR, abs/2112.07518, 2021.
  * [AD19] S. Adam-Day.  Polyhedral completeness in intermediate and modal logics.  Master’s Thesis, Available as ILLC report: MoL-2019-08, 2019.
  * [AGH+19] Rajeev Alur, Mirco Giacobbe, Thomas A. Henzinger, Kim G. Larsen, and Marius Mikucionis.  Continuous-time models for system design and analysis.  In Computing and Software Science - State of the Art and Perspectives, volume 10000 of Lecture Notes in Computer Science, pages 452–477. Springer, 2019.
  * [Alu11] Rajeev Alur.  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, October 9-14, 2011, pages 273–278. ACM, 2011.
  * [APB07] M. Aiello, I. Pratt-Hartmann, and J. Benthem, van.  Handbook of Spatial Logics.  Springer, 2007.
  * [APvB07] Marco Aiello, Ian Pratt-Hartmann, and Johan van Benthem.  What is spatial logic?  In Handbook of Spatial Logics [APB07], pages 1–11.
  * [BB07] J. Benthem, van and G. Bezhanishvili.  Modal logics of space.  In Handbook of Spatial Logics [APB07], pages 217–298.
  * [BBB+04] Oleg T. Balovnev, Thomas Bode, Martin Breunig, Armin B. Cremers, Wolfgang Müller, Gleb Pogodaev, Serge S. Shumilov, Jörg Siebeck, Agemar Siehl, and Andreas Thomsen.  The story of the geotoolkit - an object-oriented geodatabase kernel system.  GeoInformatica, 8(1):5–47, 2004.
  * [BBC+20] Fabrizio Banci Buonamici, Gina Belmonte, Vincenzo Ciancia, Diego Latella, and Mieke Massink.  Spatial logics and model checking for medical imaging.  Int. J. Softw. Tools Technol. Transf., 22(2):195–217, 2020.
  * [BBC+21] Gina Belmonte, Giovanna Broccia, Vincenzo Ciancia, Diego Latella, and Mieke Massink.  Feasibility of spatial model checking for nevus segmentation.  In 9th IEEE/ACM International Conference on Formal Methods in Software Engineering, FormaliSE@ICSE 2021, Madrid, Spain, May 17-21, 2021, pages 1–12. IEEE, 2021.
  * [BBJ+20] Martin Breunig, Patrick Erik Bradley, Markus Jahn, Paul Kuper, Nima Mazroob, Norbert Rösch, Mulhim Al-Doori, Emmanuel Stefanakis, and Mojgan Jadidi.  Geospatial data management research: Progress and future directions.  ISPRS Int. J. Geo Inf., 9(2):95, 2020.
  * [BCG88] Michael C. Browne, Edmund M. Clarke, and Orna Grumberg.  Characterizing finite kripke structures in propositional temporal logic.  Theor. Comput. Sci., 59:115–131, 1988.
  * [BCG+21a] Nick Bezhanishvili, Vincenzo Ciancia, David Gabelaia, Gianluca Grilletti, Diego Latella, and Mieke Massink.  Geometric model checking of continuous space.  CoRR, abs/2105.06194, 2021.
  * [BCG21b] Laura Bussi, Vincenzo Ciancia, and Fabio Gadducci.  Towards a spatial model checker on GPU.  In Kirstin Peters and Tim A. C. Willemse, editors, Formal Techniques for Distributed Objects, Components, and Systems - 41st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14-18, 2021, Proceedings, volume 12719 of Lecture Notes in Computer Science, pages 188–196. Springer, 2021.
  * [BCLM19a] Gina Belmonte, Vincenzo Ciancia, Diego Latella, and Mieke Massink.  Innovating medical image analysis via spatial logics.  In From Software Engineering to Formal Methods and Tools, and Back - Essays Dedicated to Stefania Gnesi on the Occasion of Her 65th Birthday, volume 11865 of Lecture Notes in Computer Science, pages 85–109. Springer, 2019.
  * [BCLM19b] Gina Belmonte, Vincenzo Ciancia, Diego Latella, and Mieke Massink.  Voxlogica: A spatial model checker for declarative image analysis.  In Tools and Algorithms for the Construction and Analysis of Systems, TACAS, volume 11427 of LNCS, pages 281–298. Springer, 2019\.
  * [BFGH17] Sergiy Bogomolov, Goran Frehse, Mirco Giacobbe, and Thomas A. Henzinger.  Counterexample-guided refinement of template polyhedra.  In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, volume 10205 of Lecture Notes in Computer Science, pages 589–606, 2017.
  * [BK08] C. Baier and J. Katoen.  Principles of model checking.  MIT Press, 2008.
  * [BM14] Jean-Daniel Boissonnat and Clément Maria.  The simplex tree: An efficient data structure for general simplicial complexes.  Algorithmica, 70(3):406–427, Nov 2014.
  * [BMMP18] N. Bezhanishvili, V. Marra, D. McNeill, and A. Pedrini.  Mckin’s theorem on intuitionistic logic, for polyhedra.  Ann. Pure Appl. Log., 169(5):373–391, 2018.
  * [BMÖ19] Giovanna Broccia, Paolo Milazzo, and Peter Csaba Ölveczky.  Formal modeling and analysis of safety-critical human multitasking.  Innov. Syst. Softw. Eng., 15(3-4):169–190, 2019.
  * [CBLM21] Vincenzo Ciancia, Gina Belmonte, Diego Latella, and Mieke Massink.  A hands-on introduction to spatial model checking using voxlogica.  In Alfons Laarman and Ana Sokolova, editors, Model Checking Software, pages 22–41, Cham, 2021. Springer International Publishing.
  * [CCC+08] Paolo Cignoni, Marco Callieri, Massimiliano Corsini, Matteo Dellepiane, Fabio Ganovelli, and Guido Ranzuglia.  MeshLab: an Open-Source Mesh Processing Tool.  In Vittorio Scarano, Rosario De Chiara, and Ugo Erra, editors, Eurographics Italian Chapter Conference. The Eurographics Association, 2008.
  * [CGG+18] Vincenzo Ciancia, Stephen Gilmore, Gianluca Grilletti, Diego Latella, Michele Loreti, and Mieke Massink.  Spatio-temporal model checking of vehicular movement in public transport systems.  STTT, 20(3):289–311, 2018.
  * [CGL+14] V. Ciancia, S. Gilmore, D. Latella, M. Loreti, and M. Massink.  Data verification for collective adaptive systems: Spatial model-checking of vehicle location data.  In Eighth IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, SASOW, pages 32–37. IEEE Computer Society, 2014.
  * [CGL+15] V. Ciancia, G. Grilletti, D. Latella, M. Loreti, and M. Massink.  An experimental spatio-temporal model checker.  In Software Engineering and Formal Methods - SEFM 2015 Collocated Workshops, volume 9509 of Lecture Notes in Computer Science, pages 297–311. Springer, 2015.
  * [CLLM14] V. Ciancia, D. Latella, M. Loreti, and M. Massink.  Specifying and verifying properties of space.  In Theoretical Computer Science - 8th IFIP TC 1/WG 2.2 International Conference, TCS 2014, Rome, Italy, September 1-3, 2014. Proceedings, volume 8705 of Lecture Notes in Computer Science, pages 222–235. Springer, 2014.
  * [CLLM16a] V. Ciancia, D. Latella, M. Loreti, and M. Massink.  Model Checking Spatial Logics for Closure Spaces.  Logical Methods in Computer Science, Volume 12, Issue 4, October 2016.
  * [CLLM16b] Vincenzo Ciancia, Diego Latella, Michele Loreti, and Mieke Massink.  Spatial logic and spatial model checking for closure spaces.  In Formal Methods for the Quantitative Evaluation of Collective Adaptive Systems - 16th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2016, volume 9700 of Lecture Notes in Computer Science, pages 156–201. Springer, 2016.
  * [CLM+16] V. Ciancia, D. Latella, M. Massink, R. Paškauskas, and A. Vandin.  A tool-chain for statistical spatio-temporal model checking of bike sharing systems.  In Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Part I, volume 9952 of Lecture Notes in Computer Science, pages 657–673, 2016.
  * [CLMdV20] Vincenzo Ciancia, Diego Latella, Mieke Massink, and Erik P. de Vink.  Towards spatial bisimilarity for closure models: Logical and coalgebraic characterisations.  CoRR, abs/2005.05578, 2020.
  * [CLMP15] Vincenzo Ciancia, Diego Latella, Mieke Massink, and Rytis Paškauskas.  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, September 21-25, 2015, pages 74–79. IEEE Computer Society, 2015.
  * [CM21] Davide Castelnovo and Marino Miculan.  Closure hyperdoctrines.  In Fabio Gadducci and Alexandra Silva, editors, 9th Conference on Algebra and Coalgebra in Computer Science, CALCO 2021, August 31 to September 3, 2021, Salzburg, Austria, volume 211 of LIPIcs, pages 12:1–12:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.
  * [DV95] Rocco De Nicola and Frits W. Vaandrager.  Three logics for branching bisimulation.  J. ACM, 42(2):458–487, 1995.
  * [Gal99] A. Galton.  The mereotopology of discrete space.  In Spatial Information Theory. Cognitive and Computational Foundations of Geographic Information Science, volume 1661 of Lecture Notes in Computer Science, pages 251–266. Springer, 1999.
  * [Gal14] A. Galton.  Discrete mereotopology.  In C. Calosi and P. Graziani, editors, Mereology and the Sciences: Parts and Wholes in the Contemporary Scientific Context, pages 293–321. Springer International Publishing, 2014.
  * [GG08] Antoine Girard and Colas Le Guernic.  Zonotope/hyperplane intersection for hybrid systems reachability analysis.  In Hybrid Systems: Computation and Control, 11th International Workshop, 2008., volume 4981 of Lecture Notes in Computer Science, pages 215–228. Springer, 2008.
  * [GJKW17] Jan Friso Groote, David N. Jansen, Jeroen J. A. Keiren, and Anton Wijs.  An _O_(_m_ log _n_) algorithm for computing stuttering equivalence and branching bisimulation.  ACM Trans. Comput. Log., 18(2):13:1–13:34, 2017.
  * [Gri16] Gianluca Grilletti.  Spatio-temporal model checking: Explicit and abstraction-based methods.  Master’s thesis, University of Pisa, 2016.
  * [GSC+09] R. Grosu, S. Smolka, F. Corradini, A. Wasilewska, E. Entcheva, and E. Bartocci.  Learning and detecting emergent behavior in networks of cardiac myocytes.  Commun. ACM, 52(3):97–105, 2009.
  * [Hen00] Thomas A. Henzinger.  The theory of hybrid automata.  In Verification of Digital and Hybrid Systems, pages 265–292. Springer, 2000.
  * [HH94] Thomas A. Henzinger and Pei-Hsin Ho.  HYTECH: the cornell hybrid technology tool.  In Hybrid Systems II, Proceedings of the Third International Workshop on Hybrid Systems, volume 999 of Lecture Notes in Computer Science, pages 265–293. Springer, 1994.
  * [HJK+15] I. Haghighi, A. Jones, Z. Kong, E. Bartocci, R. Grosu, and C. Belta.  Spatel: A novel spatial-temporal logic and its applications to networked systems.  In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, HSCC ’15, pages 189–198. ACM, 2015.
  * [KdR97] Natasha Kurtonina and Maarten de Rijke.  Bisimulations for temporal logic.  J. Log. Lang. Inf., 6(4):403–425, 1997.
  * [LPS20] Sven Linker, Fabio Papacchini, and Michele Sevegnani.  Analysing spatial properties on neighbourhood spaces.  In Javier Esparza and Daniel Král’, editors, 45th International Symposium on Mathematical Foundations of Computer Science, MFCS 2020, August 24-28, 2020, Prague, Czech Republic, volume 170 of LIPIcs, pages 66:1–66:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.
  * [LPZ12] Joshua A. Levine, Rasmus R. Paulsen, and Yongjie Zhang.  Mesh processing in medical-image analysis?a tutorial.  IEEE Computer Graphics and Applications, 32(5):22–28, 2012.
  * [LQ21] Michele Loreti and Michela Quadrini.  A spatial logic for a simplicial complex model.  CoRR, abs/2105.08708, 2021.
  * [Mau80] C. R. F. Maunder.  Algebraic topology.  Cambridge University Press., 1980.
  * [MC21] Alessandro Muntoni and Paolo Cignoni.  PyMeshLab.  Zenodo, January 2021.
  * [MT44] J. McKinsey and A. Tarski.  The algebra of topology.  Annals of Mathematics, 45:141–191, 1944.
  * [NBC+18] L. Nenzi, L. Bortolussi, V. Ciancia, M. Loreti, and M. Massink.  Qualitative and Quantitative Monitoring of Spatio-Temporal Properties with SSTL.  Logical Methods in Computer Science, 14(4):1–38, 2018.  DOI 10.23638/LMCS-14(4:2)2018. Published on line: 23 Oct. 2018. ISSN: 1860-5974.
  * [SDI08] Sriram Sankaranarayanan, Thao Dang, and Franjo Ivancic.  Symbolic model checking of hybrid systems using template polyhedra.  In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008., volume 4963 of Lecture Notes in Computer Science, pages 188–202. Springer, 2008.
  * [TKG17] Christos Tsigkanos, Timo Kehrer, and Carlo Ghezzi.  Modeling and verification of evolving cyber-physical spaces.  In Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2017, pages 38–48. ACM, 2017.
  * [VB84] Johan Van Benthem.  Correspondence Theory, pages 167–247.  Springer Netherlands, Dordrecht, 1984.

##  Appendix A Additional Lemmas and Proofs

######  Proposition 13.

Consider the operator $\rho$ of [BCLM19b]. We have
$\mathcal{X},x\vDash\rho\,\psi[\phi]\iff\mathcal{X},x\models\psi\lor\gamma(\phi,\psi)$,
and
$\mathcal{X},x\vDash\gamma(\phi,\psi)\iff\mathcal{X},x\vDash\rho\,(\phi\land\rho\,\psi[\phi])[\phi]$.

######  Proof A.1.

We note in passing that the following proof (and the definition of $\rho$ and
$\gamma$) generalise to arbitrary topological models. We first recall the
formal definition of $\rho$, which uses right-open paths (that is, total
continuous functions having $\mathbb{R}_{\geq 0}$ as a domain). Note that in
[BCLM19b], $\rho$ was defined only on discrete spaces. However, following the
direction of [CLLM16a], the definition applies in a natural way to continuous
spaces as follows: $\mathcal{X},x\vDash\rho\,\psi\,[\phi]$ whenever there is a
right-open path $\pi:\mathbb{R}_{\geq 0}\to P$ and an index $r$ such that
$\pi(0)=x$, $\pi(r)\in\left\llbracket\psi\right\rrbracket^{\mathcal{X}}$ and
$\pi((0,r))\subseteq\left\llbracket\phi\right\rrbracket^{\mathcal{X}}$. We
proceed by proving the four implications in the statement separately.

First, we show that ${\mathcal{X}},x\models\rho\,\psi[\phi]$ implies
${\mathcal{X}},x\models\psi\lor\gamma(\phi,\psi)$. If
${\mathcal{X}},x\models\rho\,\psi[\phi]$ then there is right-open path $\pi$
and $\ell\in\mathbb{R}_{\geq 0}$ such that
$\pi(0)=x,\pi((0,\ell))\subseteq\left\llbracket\phi\right\rrbracket^{\mathcal{X}}$
and $\pi(\ell)\in\left\llbracket\psi\right\rrbracket^{\mathcal{X}}$. We
consider two distinct cases:
Case 1: $\ell=0$. In this case
$x\in\left\llbracket\psi\right\rrbracket^{\mathcal{X}}$ and so
${\mathcal{X}},x\models\psi\lor\gamma(\phi,\psi)$.
Case 2: $\ell\neq 0$. In this case, let $\pi^{\prime}$ with
$\pi^{\prime}(r)=\pi(r\ell)$ for all $r\in[0,1]$. We have
$\pi^{\prime}(0)=\pi(0)=x$,
$\pi^{\prime}((0,1))=\pi((0,\ell))\subseteq\left\llbracket\phi\right\rrbracket^{\mathcal{X}}$
and
$\pi^{\prime}(1)=\pi(\ell)\in\left\llbracket\psi\right\rrbracket^{\mathcal{X}}$.
This means that ${\mathcal{X}},x\models\gamma(\phi,\psi)$, and so
${\mathcal{X}},x\models\psi\lor\gamma(\phi,\psi)$.

We now show that ${\mathcal{X}},x\models\psi\lor\gamma(\phi,\psi)$ implies
${\mathcal{X}},x\models\rho\,\psi[\phi]$. Suppose that
${\mathcal{X}},x\models\psi\lor\gamma(\phi,\psi)$. We consider two distinct
cases:
Case 1: ${\mathcal{X}},x\models\psi$. In this case it trivially holds
${\mathcal{X}},x\models\rho\,\psi[\phi]$ (for any right-open path starting at
$x$, just consider $\ell=0$).
Case 2: ${\mathcal{X}},x\models\gamma(\phi,\psi)$. In this case there is a
path $\pi$ such that $\pi(0)=x$,
$\pi((0,1))\subseteq\left\llbracket\phi\right\rrbracket^{\mathcal{X}}$ and
$\pi(1)\in\left\llbracket\psi\right\rrbracket^{\mathcal{X}}$. We obtain
${\mathcal{X}},x\models\rho\,\psi[\phi]$ by taking $\ell=1$ in the definition
of the semantic clause of $\rho$.

We now show that ${\mathcal{X}},x\models\gamma(\phi,\psi)$ implies
${\mathcal{X}},x\models\rho\,(\phi\land\rho\,\psi[\phi])[\phi]$. Suppose
${\mathcal{X}},x\models\gamma(\phi,\psi)$, that is, there is a path $\pi$ such
that $\pi(0)=x$,
$\pi((0,1))\subseteq\left\llbracket\phi\right\rrbracket^{\mathcal{X}}$ and
$\pi(1)\in\left\llbracket\psi\right\rrbracket^{\mathcal{X}}$. Since $\pi$ is a
total continuous function, there is an $\epsilon\in(0,1)$ such that
$\pi(\epsilon)\in\left\llbracket\phi\right\rrbracket^{\mathcal{X}}$. We define
two additional paths $\pi_{1}(t)=\pi(t\epsilon)$ and
$\pi_{2}(t)=\pi((1-\epsilon)t+\epsilon)$. Notice that
$\pi_{2}(0)=\pi(\epsilon)\in\left\llbracket\phi\right\rrbracket^{\mathcal{X}},\pi_{2}((0,1))=\pi((\epsilon,1))\subseteq\left\llbracket\phi\right\rrbracket^{\mathcal{X}}$
and $\pi_{2}(1)=\pi(1)\in\left\llbracket\psi\right\rrbracket^{\mathcal{X}}$:
this shows that ${\mathcal{X}},\pi(\epsilon)\models\phi\land\rho\,\psi[\phi]$.
Moreover, we have
$\pi_{1}(0)=\pi(0)=x,\pi_{1}((0,1))=\pi((0,\epsilon))\subseteq\left\llbracket\phi\right\rrbracket^{\mathcal{X}}$
and
$\pi_{1}(1)=\pi_{2}(0)\in\left\llbracket\phi\land\rho\,\psi[\phi]\right\rrbracket^{\mathcal{X}}$:
this shows that
${\mathcal{X}},x\models\rho\,(\phi\land\rho\,\psi[\phi])[\phi]$.

Finally, we show that
${\mathcal{X}},x\models\rho\,(\phi\land\rho\,\psi[\phi])[\phi]$ implies
${\mathcal{X}},x\models\gamma(\phi,\psi)$. Suppose that
${\mathcal{X}},x\models\rho\,(\phi\land\rho\,\psi[\phi])[\phi]$, that is,
there is a right-open path $\pi_{1}$ and a value $\ell_{1}\in\mathbb{R}_{\geq
0}$ such that
$\pi_{1}(0)=x,\pi_{1}((0,\ell_{1}))\subseteq\left\llbracket\phi\right\rrbracket^{\mathcal{X}}$
and
$\pi_{1}(\ell_{1})\in\left\llbracket\phi\land\rho\,\psi[\phi]\right\rrbracket^{\mathcal{X}}=\left\llbracket\phi\right\rrbracket^{\mathcal{X}}\cap\left\llbracket\rho\,\psi[\phi]\right\rrbracket^{\mathcal{X}}$.
By the last condition, there is a right-open path $\pi_{2}$ and a value
$\ell_{2}\in\mathbb{R}_{\geq 0}$ such that $\pi_{2}(0)=\pi_{1}(\ell_{1})$,
$\pi_{2}((0,\ell_{2}))\subseteq\left\llbracket\phi\right\rrbracket^{\mathcal{X}}$
and $\pi_{2}(\ell_{2})\in\left\llbracket\psi\right\rrbracket^{\mathcal{X}}$.
We consider two distinct cases:
Case 1: $l_{1}=l_{2}=0$. In this case $\pi_{1}(l_{1})=\pi_{2}(l_{2})=x$, and
so
$x\in\left\llbracket\phi\right\rrbracket^{\mathcal{X}}\cap\left\llbracket\psi\right\rrbracket^{\mathcal{X}}$.
In this case $\mathcal{X},x\vDash\gamma(\phi,\psi)$ holds trivially.
Case 2: $l_{1}>0$ or $l_{2}>0$. In this case define the path $\pi^{\prime}$ by
imposing $\pi^{\prime}(t)=\pi_{1}(2tl_{1})$ and
$\pi^{\prime}(\frac{1}{2}+t)=\pi_{2}(2tl_{2})$ for $t\in[0,\frac{1}{2}]$
(notice that the path is well-defined since
$\pi^{\prime}(\frac{1}{2})=\pi_{1}(l_{1})=\pi_{2}(0)$). Clearly
$\pi^{\prime}(0)=x$. Moreover,
$\pi^{\prime}((0,1))=\pi^{\prime}((0,\frac{1}{2}])\cup\pi^{\prime}((\frac{1}{2},1))=\pi_{1}((0,l_{1}))\cup\pi_{2}((0,l_{2}))\subseteq\left\llbracket\phi\right\rrbracket^{\mathcal{X}}$
(under the assumption that $l_{1}>0$ or $l_{2}>0$). And finally
$\pi^{\prime}(1)=\pi_{2}(l_{2})\in\left\llbracket\psi\right\rrbracket^{\mathcal{X}}$.
This shows that $\mathcal{X},x\vDash\gamma(\phi,\psi)$, as desired.

######  Proposition 14.

Let $\sigma$ be a non-empty simplex and consider $x\in\widetilde{\sigma}$ and
$y\in\sigma$. Then there is a _linear_ path (a segment in $\mathbb{R}^{d}$)
$\pi:[0,1]\to\sigma$ with $\pi(0)=x$, $\pi(1)=y$ and
$\pi([0,1))\subseteq\widetilde{\sigma}$; more precisely, $\pi(t)=ty+(1-t)x$.

######  Proof A.2.

Let $V=\\{v_{0},\dots,v_{n}\\}$ be the set of vertices of $\sigma$. By
definition of $\sigma$, $x$ and $y$ are in the convex hull of $V$, that is,
there exist $\lambda_{i}$ and $\delta_{i}$ such that
$x=\sum_{i=0}^{n}\lambda_{i}v_{i}$ and $y=\sum_{i=0}^{n}\delta_{i}v_{i}$.
Since $x\in\widetilde{\sigma}$, every $\lambda_{i}$ is strictly greater than
$0$. For $\pi$ as defined in the statement we have
$\pi(t)=\sum_{i=0}^{n}\left(t\delta_{i}+(1-t)\lambda_{i}\right)v_{i}$. This
function is clearly continuous (thus a path), and we have $\pi(0)=x$ and
$\pi(1)=y$. Moreover, for every $t\in[0,1)$ and every $i\leq n$ we have
$t\delta_{i}+(1-t)\lambda_{i}\geq(1-t)\lambda_{i}>0$, and so
$\pi([0,1))\subseteq\widetilde{\sigma}$.

######  Lemma 15.

Let $\mathrm{K}$ be a simplicial complex and $\sigma,\tau\in\mathrm{K}$. Then
$\sigma\preceq\tau$ iff
$\widetilde{\sigma}\,\widetilde{\preceq}\,\widetilde{\tau}$ iff
$\widetilde{\sigma}\subseteq\mathcal{C}(\widetilde{\tau})$ iff
$\widetilde{\sigma}\cap\mathcal{C}(\widetilde{\tau})\neq\emptyset$.

######  Proof A.3.

The first equivalence is simply the definition of $\widetilde{\preceq}$ (see
Definition 5). As for the other equivalences, firstly we show that
$\sigma\preceq\tau$ implies
$\widetilde{\sigma}\subseteq\mathcal{C}(\widetilde{\tau})$. In fact, if
$\sigma\preceq\tau$ we have $\sigma\subseteq\tau$, and so
$\widetilde{\sigma}\subseteq\sigma\subseteq\tau=\mathcal{C}(\widetilde{\tau})$.
Secondly, note that since cells are nonempty sets we have that
$\widetilde{\sigma}\subseteq\mathcal{C}(\widetilde{\tau})$ implies
$\widetilde{\sigma}\cap\mathcal{C}(\widetilde{\tau})\neq\emptyset$. Finally,
we show that
$\widetilde{\sigma}\cap\mathcal{C}(\widetilde{\tau})\neq\emptyset$ implies
$\sigma\preceq\tau$, concluding the proof. Notice that
$\mathcal{C}(\widetilde{\tau})=\tau=\bigcup\\{\widetilde{\tau}^{\prime}\,|\,\tau^{\prime}\preceq\tau\\}$.
So by Lemma 1 we have that either
$\widetilde{\sigma}\in\\{\widetilde{\tau}^{\prime}\,|\,\tau^{\prime}\preceq\tau\\}$
or $\widetilde{\sigma}\cap\mathcal{C}(\widetilde{\tau})=\emptyset$. Since the
latter is not the case by assumption, we conclude $\sigma\preceq\tau$.

######  Lemma 16.

Let $\pi_{1}$ and $\pi_{2}$ be two paths, with $\pi_{1}(1)=\pi_{2}(0)$; let
$x,y\in[0,1]$, with $x<y$. Define in the obvious way the _concatenation_
$\pi_{1};\pi_{2}$, with $\pi_{1};\pi_{2}(0)=\pi_{1}(0)$ and
$\pi_{1};\pi_{2}(1)=\pi_{2}(1)$ and the sub-path ${\pi_{1}}^{[x,y]}$, with
${\pi_{1}}^{[x,y]}(0)=\pi_{1}(x)$ and ${\pi_{1}}^{[x,y]}(1)=\pi_{1}(y)$. We
have that: whenever $\pi_{1}$ and $\pi_{2}$ are piecewise-linear (simplicial),
also $\pi_{1};\pi_{2}$ is piecewise linear (simplicial); whenever $\pi_{1}$ is
piecewise linear (simplicial), also ${\pi_{1}}^{[x,y]}$ is piecewise linear
(simplicial). Furthermore, for any two (additional) paths $\pi^{\prime}_{1}$,
$\pi^{\prime}_{2}$ with $\pi^{\prime}_{1}(1)=\pi^{\prime}_{2}(0)$, and
relation $R$, if $\pi_{1}\hat{R}\pi^{\prime}_{1}$ and
$\pi_{2}\hat{R}\pi^{\prime}_{2}$, then
$\pi_{1};\pi_{2}\hat{R}\pi^{\prime}_{1};\pi^{\prime}_{2}$.

######  Proof A.4.

We omit the proof, which is straightforward.

Lemma 2. Let $\mathcal{X}=\left\langle P,\mathrm{K},V\right\rangle$ and
$\mathcal{X}^{\prime}=\left\langle P,\mathrm{K}^{\prime},V\right\rangle$ be
two models sharing the same $P$ and $V$. For each $x\in P$ and $\phi$ we have:
$\mathcal{X},x\vDash\phi\iff\mathcal{X}^{\prime},x\vDash\phi$.

######  Proof A.5.

Just note that $\mathrm{K}$ does not appear in Definition 3.

Lemma 3. Let $\mathcal{X}$ be a polyhedral model and $\mathrm{K}$ a simplicial
complex coherent with $\mathcal{X}$. Then for each cell
$\widetilde{\sigma}\in\widetilde{\mathrm{K}}$ and $x,y\in\widetilde{\sigma}$
we have $x\equiv y$.

######  Proof A.6.

We prove the result by induction on the structure of $\phi$. Since most of the
cases follow easily from the semantic clauses of the logic, we show only the
cases for $\phi=\Box\psi$ and $\phi=\gamma(\psi,\chi)$.

Case $\phi=\Box\psi$: By inductive hypothesis,
$\left\llbracket\psi\right\rrbracket^{\mathcal{X}}$ is a union of cells of
$\widetilde{\mathrm{K}}$, and by Lemma 1 also
$P\setminus\left\llbracket\psi\right\rrbracket^{\mathcal{X}}$ is a union of
cells. Since there are only finitely many cells in $\widetilde{\mathrm{K}}$,
we have
$\mathcal{C}(P\setminus\left\llbracket\psi\right\rrbracket^{\mathcal{X}})=\bigcup\\{\mathcal{C}(\widetilde{\sigma})\,|\,\widetilde{\sigma}\subseteq
P\setminus\left\llbracket\psi\right\rrbracket^{\mathcal{X}}\\}$. And since
$\mathcal{C}(\widetilde{\sigma})=\sigma=\bigcup\\{\widetilde{\tau}\,|\,\tau\preceq\sigma\\}$,
it follows that
$\mathcal{C}(P\setminus\left\llbracket\psi\right\rrbracket^{\mathcal{X}})=\bigcup\\{\widetilde{\tau}\,|\,\exists\sigma.\,\tau\preceq\sigma\,\text{and}\,\widetilde{\sigma}\subseteq
P\setminus\left\llbracket\psi\right\rrbracket^{\mathcal{X}}\\}$, that is,
$\mathcal{C}(P\setminus\left\llbracket\psi\right\rrbracket^{\mathcal{X}})$ is
a union of cells. To conclude, by Lemma 1 we have that
$\left\llbracket\phi\right\rrbracket^{\mathcal{X}}=\mathcal{I}(\left\llbracket\psi\right\rrbracket^{\mathcal{X}})=P\setminus\mathcal{C}(P\setminus\left\llbracket\psi\right\rrbracket^{\mathcal{X}})$
is again a union of cells.

Case $\phi=\gamma(\psi,\chi)$: Suppose that
$\mathcal{X},x\vDash\gamma(\phi,\psi)$: we aim to show that
$\mathcal{X},y\vDash\gamma(\phi,\psi)$. The fact that
$\mathcal{X},x\vDash\gamma(\phi,\psi)$ means that there exists a path $\pi$
such that $\pi(0)=x$,
$\pi((0,1))\subseteq\left\llbracket\phi\right\rrbracket^{\mathcal{X}}$ and
$\pi(1)\in\left\llbracket\psi\right\rrbracket^{\mathcal{X}}$. By inductive
hypothesis $\left\llbracket\phi\right\rrbracket^{\mathcal{X}}$ is a union of
cells, and since
$\left\llbracket\phi\right\rrbracket^{\mathcal{X}}\cap\pi((0,1))$ is not empty
also the set $\Pi=\\{\widetilde{\tau}|\exists
r\in(0,1).\pi(r)\in\widetilde{\tau}\subseteq\left\llbracket\phi\right\rrbracket^{\mathcal{X}}\\}$
is not empty.

Since $\pi((0,1))\subseteq\bigcup\Pi$, we have
$x\in\mathcal{C}(\pi((0,1)))\subseteq\bigcup\\{\tau|\exists
r\in(0,1).\pi(r)\in\widetilde{\tau}\subseteq\left\llbracket\phi\right\rrbracket^{\mathcal{X}}\\}$.
Thus there exists a value $r\in(0,1)$ and a cell $\widetilde{\tau}$ such that
$x\in\tau$ and $\pi(r)\in\widetilde{\tau}$. Since
$x\in\widetilde{\sigma}\cap\mathcal{C}(\widetilde{\tau})$, by Lemma 15 we have
$\widetilde{\sigma}\subseteq\mathcal{C}(\widetilde{\tau})=\tau$ and
consequently $y\in\tau$. By Proposition 14 (modulo inverting and
reparametrising the path) there exists a path $\pi^{\prime}:[0,r]\to\tau$ such
that $\pi^{\prime}(0)=y$, $\pi^{\prime}(r)=\pi(r)$ and
$\pi^{\prime}((0,r))\subseteq\widetilde{\tau}\subseteq\left\llbracket\phi\right\rrbracket^{\mathcal{X}}$.
If we extend $\pi^{\prime}$ by imposing $\pi^{\prime}(t)=\pi(t)$ for
$t\in(r,1]$, we obtain a path such that $\pi^{\prime}(0)=y$,
$\pi^{\prime}((0,1))\subseteq\left\llbracket\phi\right\rrbracket^{\mathcal{X}}$
and $\pi^{\prime}(1)\in\left\llbracket\psi\right\rrbracket^{\mathcal{X}}$. In
particular $\pi^{\prime}$ witnesses that
$\mathcal{X},y\vDash\gamma(\phi,\psi)$, as desired.

Proposition 4. Given a polyhedral model $\mathcal{X}$, the relation $\equiv$
has only finitely many equivalence classes. Furthermore, each equivalence
class $C$ has a _characteristic formula_ $\phi^{C}$ such that
$\mathcal{X},x\vDash\phi^{C}\iff x\in C$.

######  Proof A.7.

Fix $\mathrm{K}$ coherent with $\mathcal{X}$. By Lemma 3, each equivalence
class is a union of distinct cells of $\widetilde{\mathrm{K}}$. But since
there are only finitely many cells, there are finitely many equivalence
classes too. For two distinct equivalence classes $C$ and $C^{\prime}$, let
$\phi^{C,C^{\prime}}$ be a formula satisfied by the elements of $C$ but not by
the elements in $C^{\prime}$—such a formula exists by definition of $\equiv$.
Then the formula $\phi^{C}=\bigwedge_{C^{\prime}\neq C}\phi^{C,C^{\prime}}$ is
satisfied only by elements in $C$, as desired.

Theorem 5. For each formula $\phi$, we have
$\mathcal{X},x\vDash\Box\phi\iff\mathcal{X},x\vDash\lnot\gamma(\lnot\phi,\top)$.

######  Proof A.8.

Recall the definition of $\Diamond\phi:=\lnot\Box\lnot\phi$ and that
$\mathcal{X},x\models\Diamond\phi\iff
x\in\mathcal{C}(\left\llbracket\phi\right\rrbracket^{\mathcal{X}})$ (see e.g.
[BB07]), where $\mathcal{C}$ is the topological closure operator. Thus, we
prove the equivalent statement
$\mathcal{X},x\vDash\Diamond\phi\iff\mathcal{X},x\vDash\gamma(\phi,\top)$.

If $\mathcal{X},x\models\gamma(\phi,\top)$, by definition, there is a path
$\pi$ with $\pi(0)=x$ and
$\pi((0,1))\subseteq\left\llbracket\phi\right\rrbracket^{\mathcal{X}}$. In
particular we have $x=\pi(0)\in\mathcal{C}(\,\pi((0,1))\,)$ by continuity of
paths, and
$\mathcal{C}(\,\pi((0,1))\,)\subseteq\mathcal{C}(\left\llbracket\phi\right\rrbracket^{\mathcal{X}})$
by monotonicity of $\mathcal{C}$. Therefore
$x\in\mathcal{C}(\left\llbracket\phi\right\rrbracket^{\mathcal{X}})$, which
amounts to $\mathcal{X},x\vDash\Diamond\phi$.

If $\mathcal{X},x\models\Diamond\phi$, we have
$x\in\mathcal{C}(\left\llbracket\phi\right\rrbracket^{\mathcal{X}})$. Fix
$\mathrm{K}$ a simplicial complex coherent with $\mathcal{X}$. By Lemma 3
$\left\llbracket\phi\right\rrbracket^{\mathcal{X}}$ is a union of cells in
$\widetilde{\mathrm{K}}$, and so
$\mathcal{C}(\left\llbracket\phi\right\rrbracket^{\mathcal{X}})=\bigcup\\{\mathcal{C}(\widetilde{\sigma})\,|\,\widetilde{\sigma}\subseteq\left\llbracket\phi\right\rrbracket^{\mathcal{X}}\\}$.
In particular, $x\in\mathcal{C}(\widetilde{\sigma})=\sigma$ for one of these
cells. Fix an arbitrary element $y\in\widetilde{\sigma}$—recall that
$\widetilde{\sigma}$ is nonempty whenever $\sigma$ is nonempty. By Proposition
14 (note that the names $x$ and $y$ are inverted in the statement of the
proposition) there is a path $\pi$ with $\pi(0)=y$, $\pi(1)=x$, and
$\pi([0,1))\subseteq\widetilde{\sigma}\subseteq\left\llbracket\phi\right\rrbracket^{\mathcal{X}}$.
The “converse” path $\pi^{\prime}(i):=\pi(1-i)$ witnesses that
$\mathcal{X},x\models\gamma(\phi,\top)$.

Lemma 6. Let $\mathrm{K}$ be a simplicial complex and
$x,y\in\left|\mathrm{K}\right|$. Then there exists a path in
$\left|\mathrm{K}\right|$ from $x$ to $y$ if and only if there is a PL-path in
$\left|\mathrm{K}\right|$ from $x$ to $y$.

######  Proof A.9.

The right-to-left direction is trivial, so we focus on the left-to-right
direction. Fix a path in $\left|\mathrm{K}\right|$ starting at $x$ and ending
at $y$, and consider the set $\Pi\subseteq\widetilde{\mathrm{K}}$ of cells
traversed by the path. Clearly $\bigcup\Pi$ is a connected subset of
$\left|\mathrm{K}\right|$. To obtain the desired result it suffices to show
that $\bigcup\Pi$ is also _PL-connected_ , that is, for all $x,y\in\bigcup\Pi$
there exists a PL-path from $x$ to $y$. We are going to prove this by
induction on the cardinality of $\Pi$.

Base case: If $\\#\Pi=1$, then any two points $x,y\in\bigcup\Pi$ belong to the
same cell $\widetilde{\sigma}$, and since cells are convex there is a linear
path (thus piecewise linear) connecting $x$ and $y$.

Inductive step: Suppose that $\\#\Pi=n+1$ and that the result holds for sets
with lower cardinality. Consider two points $x,z\in\bigcup\Pi$ and call
$\widetilde{\sigma}$ the cell containing $x$. If $z\in\widetilde{\sigma}$ too
we can reason as in the base case, so we can assume otherwise. Define $Z$ to
be the connected component of
$\bigcup\left(\Pi\setminus\\{\widetilde{\sigma}\\}\right)$ containing $z$. $Z$
is itself the union of a set of cells $\Pi^{\prime}$—since cells are
connected. As $\\#\Pi^{\prime}<\\#\Pi$, by inductive hypothesis $Z$ is PL-
connected. Notice that $Y:=\widetilde{\sigma}\cup Z$ is connected, for
otherwise $Z$ would be disconnected from $\bigcup\Pi\setminus Z$, against the
initial assumption that $\bigcup\Pi$ is connected.

$\mathcal{C}(\widetilde{\sigma})=\sigma$ and $\mathcal{C}(Z)$ are closed sets
whose union covers $Y$. If the intersection $Y\cap\sigma\cap\mathcal{C}(Z)$
were empty, then $Y\cap\sigma$ and $Y\cap\mathcal{C}(Z)$ would disconnect $Y$.
So there must be a point $y\in Y\cap\sigma\cap\mathcal{C}(Z)$. By Proposition
14 there exists a linear (thus PL) path $\pi_{1}$ connecting
$x\in\widetilde{\sigma}$ and $y\in\sigma$, and with
$\pi_{1}([0,1))\subseteq\widetilde{\sigma}\subseteq Y$. Moreover, since
$y\in\mathcal{C}(Z)=\mathcal{C}(\bigcup\Pi^{\prime})$, there exists a cell
$\widetilde{\tau}\in\Pi^{\prime}$ such that
$y\in\mathcal{C}(\widetilde{\tau})=\tau$. So, again by Proposition 14 (with
$w$ playing the role of $x$ in the statement of the proposition), there exists
a linear path $\pi_{2}$ from $y\in\tau$ to an arbitrary point
$w\in\widetilde{\tau}$, fully contained in $Y$. Finally, since $Z$ is PL-
connected, there exists a PL-path $\pi_{3}$ from $w$ to $z$ in $Z\subseteq Y$.
By concatenating $\pi_{1}$, $\pi_{2}$ and $\pi_{3}$ we obtain a PL-path
connecting $x$ and $z$ contained in $Y\subseteq\bigcup\Pi$, as desired.

Lemma 7. We have: $\mathcal{X},x\vDash\gamma(\phi,\psi)$ if and only if there
is a PL-path $\pi:[0,1]\stackrel{{\scriptstyle PL}}{{\to}}P$ such that
$\pi(0)=x$ and
$\pi((0,1))\subseteq\left\llbracket\phi\right\rrbracket^{\mathcal{X}}$ and
$\pi(1)\in\left\llbracket\psi\right\rrbracket^{\mathcal{X}}$.

######  Proof A.10.

The right-to-left implication follows trivially from the semantics clauses of
the reachability operators, so we focus on the left-to-right implications. Fix
a simplicial complex $\mathrm{K}$ coherent with $\mathcal{X}$. Suppose that
there exists a path $\pi:[0,1]\to P$ such that $\pi(0)=x$,
$\pi((0,1))\subseteq\left\llbracket\phi\right\rrbracket^{\mathcal{X}}$ and
$\pi(1)\in\left\llbracket\psi\right\rrbracket^{\mathcal{X}}$. Consider the set
of cells
$\Pi:=\\{\widetilde{\sigma}\in\widetilde{\mathrm{K}}\,|\,\pi((0,1))\cap\widetilde{\sigma}\neq\emptyset\\}$.
Clearly $\bigcup\Pi$ is connected, and so by Lemma 6 it is also PL-connected
(i.e., for every two points in $\bigcup\Pi$ there is a PL-path in $\bigcup\Pi$
connecting them). Moreover $x,\pi(1)\in\mathcal{C}(\bigcup\Pi)$.

Since $x\in\mathcal{C}(\bigcup\Pi)$, there exists a cell
$\widetilde{\sigma}\in\Pi$ such that
$x\in\mathcal{C}(\widetilde{\sigma})=\sigma$. So by Proposition 14 there
exists a linear path $\pi_{1}$ from $x$ to a point (arbitrarily chosen)
$y\in\widetilde{\sigma}\subseteq\bigcup\Pi$ such that
$\pi_{1}((0,1))\subseteq\widetilde{\sigma}$ (note that the names $x$ and $y$
are inverted in the statement of the proposition). By a similar argument,
there exists a linear path $\pi_{3}$ from a point $z\in\bigcup\Pi$ to
$\pi(1)\in\left\llbracket\psi\right\rrbracket^{\mathcal{X}}$, such that
$\pi_{3}((0,1))\subseteq\bigcup\Pi$. Finally, since $\bigcup\Pi$ is PL-
connected, there exists a PL-path $\pi_{2}$ from $y$ to $z$ completely
contained in $\bigcup\Pi$. By concatenating $\pi_{1}$, $\pi_{2}$ and $\pi_{3}$
we obtain a PL-path $\pi^{\prime}$ such that $\pi^{\prime}(0)=x$,
$\pi^{\prime}((0,1))\subseteq\bigcup\Pi\subseteq\left\llbracket\phi\right\rrbracket^{\mathcal{X}}$
and $\pi^{\prime}(1)\in\left\llbracket\psi\right\rrbracket^{\mathcal{X}}$, as
desired.

Lemma 8. Any piecewise linear path is simplicial.

######  Proof A.11.

As cells are convex sets, the intersection between a cell and a segment is a
segment. So any segment crosses each cell at most once. Observing that there
are finitely many segments in a PL-path, one obtains the proof.

Theorem 9. Let $\mathcal{X}=\left\langle P,\mathrm{K},V\right\rangle$ be a
polyhedral model and $x$ a point of $P$. Let $\sigma\in\mathrm{K}$ be the
unique simplex such that $x\in\widetilde{\sigma}$. For every formula $\phi$ of
SLCS we have
$\mathcal{X},x\vDash\phi\iff\mathcal{M}(\mathcal{X}),\widetilde{\sigma}\vDash\phi$.

######  Proof A.12.

Notice that by Lemma 3 the left side of the bi-implication is equivalent to
$\widetilde{\sigma}\subseteq\left\llbracket\phi\right\rrbracket^{\mathcal{X}}$.
We proceed by induction on the structure of the formula; the only non trivial
cases are when the formula is of the form $\Box\psi$ and when the formula is
of the form $\gamma(\phi,\psi)$.

Case $\Box\psi$: We have that $\mathcal{X},x\vDash\Box\psi$ iff
$x\notin\mathcal{C}(\left\llbracket\neg\psi\right\rrbracket^{\mathcal{X}})$.
By Lemma 3, $\left\llbracket\neg\psi\right\rrbracket^{\mathcal{X}}$ is a
finite union of cells, so, by Lemma 15, the condition is equivalent to
$x\notin\bigcup\\{\tau\,|\,\widetilde{\tau}\subseteq\left\llbracket\neg\psi\right\rrbracket^{\mathcal{X}}\\}$;
and again, by Lemma 15, it is equivalent to
$\widetilde{\sigma}\,\widetilde{\not\preceq}\,\widetilde{\tau}$ for every
$\widetilde{\tau}\subseteq\left\llbracket\neg\psi\right\rrbracket^{\mathcal{X}}$.
Again by Lemma 3, for every $\widetilde{\tau}\in\widetilde{\mathrm{K}}$ we
have that if $\widetilde{\sigma}\,\widetilde{\preceq}\,\widetilde{\tau}$ then