Weak simplicial bisimilarity for polyhedral models and SLCSη

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 addition- ally propose a corresponding weak notion of ±-bisimilarity on cell-poset models, discrete representation of polyhedral models. We show that two points are weakly simplicial bisimilar iff their representations are weakly ±-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 mod- els, such as those found in domains exploiting mesh processing, typically consist of large numbers of cells. We also propose SLCSη, a weaker ver- sion 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η. Similarly, two cells are weakly ±-bisimilar iff they are logically equivalent in the poset-model interpretation of SLCSη. This work is performed in the context of the geometric spatial model checker PolyLogicA and the polyhedral semantics of SLCS.