On Bisimilarity for Polyhedral Models and SLCS
V. Ciancia, D. Gabelaia, D. Latella, M. Massink, E.~P.~de Vink

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