Dynamic logics of polyhedra and their application in 3D modeling
Kirill Kopnev

Abstract:
This thesis investigates dynamic polyhedra. We establish the connection between models of dynamic polyhedra and dynamic Kripke frames. Based on this result, we introduce a model checker for dynamic models. We demonstrate the application of PolyLogicA model checker on a real-world example from the architectural domain. Several novel theoretical results are obtained, including the Hennessy-Milner theorem for the language of basic modal logic extended by reachability modality γ and polyhedral completeness for two dynamic logics. The work contributes to the field of spatial reasoning, bridging theoretical and practical aspects in spatial model checking for dynamic objects.