Weak ±-minimisation for model checking polyhedra

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

Polyhedral models  Spatial bisimilarity  Spatial logics  Logical equivalence  Spatial model checking  Strong bisimulation  Branching bisimulation 

The work in this paper builds on the polyhedral semantics of the Spatial Logic for Closure Spaces (SLCS), and the geometric spatial model checker PolyLogicA. Polyhedral models are central in domains that exploit mesh processing, such as 3D computer graphics. A discrete representation of polyhedra is given by face-poset models, which are amenable to spatial model checking using the logical language SLCSη and PolyLogicA. In this work, we propose a procedure that computes the minimal model with respect to weak ±-bisimilarity – that is SLCSη- logical equivalence – via a translation to LTSs and branching bisimilarity. Because of its reduced size, the minimal model makes geometric model checking more efficient. We provide a preliminary experimental valida- tion of the approach exploiting the minimization capabilities of mCRL2.

Metrics