Weak Simplicial Bisimilarity for Polyhedral Models and SLCS_eta -- Extended Version
Nick Bezhanishvili, Vincenzo Ciancia, David Gabelaia, Mamuka Jibladze, Diego Latella, Mieke Massink, Erik P. de Vink
TL;DR
This work introduces SLCS$_{\eta}$, a weaker variant of SLCS$_{\gamma}$ for polyhedral models, and two corresponding weak bisimulation notions—weak simplicial bisimilarity on polyhedral models and weak $\pm$-bisimilarity on their cell-poset representations. It proves that SLCS$_{\eta}$ characterises these weak bisimilarities, establishing the Hennessy–Milner property in both continuous and discrete settings, and shows how the discrete poset interpretation preserves and reflects the continuous semantics via the map $\mathbb{F}$. A key contribution is the encoding $\mathcal{E}$ that embeds SLCS$_{\eta}$ into SLCS$_{\gamma}$, demonstrating that SLCS$_{\eta}$ is strictly weaker and thereby enabling substantial model reductions, which are illustrated by large reductions in representative polyhedral structures. The results enable more scalable spatial model checking with PolyLogicA, offering principled reduction of mesh-based models while preserving relevant reachability properties, and setting the stage for automated minimisation procedures and back-mapping to original polyhedral geometries. Overall, the paper provides a rigorous foundation for using weaker, yet expressive, spatial logics to achieve efficient verification on large polyhedral meshes.
Abstract
In the context of spatial logics and spatial model checking for polyhedral models -- mathematical basis for visualisations in continuous space -- we propose a weakening of simplicial bisimilarity. We additionally propose a corresponding weak notion of $\pm$-bisimilarity on cell-poset models, a discrete representation of polyhedral models. We show that two points are weakly simplicial bisimilar iff their repesentations are weakly $\pm$-bisimilar. The advantage of this weaker notion is that it leads to a stronger reduction of models than its counterpart that was introduced in our previous work. This is important, since real-world polyhedral models, such as those found in domains exploiting mesh processing, typically consist of large numbers of cells. We also propose SLCS_eta, a weaker version of the Spatial Logic for Closure Spaces (SLCS) on polyhedral models, and we show that the proposed bisimilarities enjoy the Hennessy-Milner property: two points are weakly simplicial bisimilar iff they are logically equivalent for SLCS_eta. Similarly, two cells are weakly $\pm$-bisimilar iff they are logically equivalent in the poset-model interpretation of SLCS_eta. This work is performed in the context of the geometric spatial model checker PolyLogicA and the polyhedral semantics of SLCS.