Practical polyhedral model checking. A gentle introduction

We illustrate the potential of spatial model checking of poly- hedral models on a number of selected examples. In computer graphics polyhedral models can be commonly found in the form of triangular sur- face meshes or tetrahedral volume meshes. Polyhedral model checking is used to analyse spatial properties of interest of such models expressed in a suitable spatial logic. For this work we use the recently developed geo- metric spatial model checker PolyLogicA, the visualiser PolyVisualizer and the polyhedral semantics of the Spatial Logic for Closure Spaces SLCS.