Weak simplicial bisimilarity for polyhedral models and SLCSη

Bezhanishvili N., Ciancia V., Gabelaia D., Jibladze M., Latella D., Massink M., De Vink E. P.

Spatial model checking  Spatial logics  Spatial bisimilarity  Logical Equivalence  Polyhedral models  Bisimulation relations 

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.

Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 14678, pp. 20-38. Groningen, NL, 17-21/06/2024

Metrics