In the context of geometric representations of spatial objects, we explore a modelchecking approach based on polyhedra. To this end we introduce the notion of a polyhedral poset model as counterpart of a polyhedron model endowed with so-called simplicial bisimilarity. The latter equivalence captures the the spatial logic SLCS-eta, which has in particular a path operator rather than the classical next operator as a modality. By encoding a polyhedral poset model as an LTS such that simplicial bisimilarity coincides with branching bisimilarity, minimization of polyhedral poset models and effective modelchecking of SLCS-eta becomes possible.
Joint work with people from CNR Pisa, Tiblisi State University, and UvA.