Dynamic Logics for Model Transformations
Frans Maarten Westers

Abstract:
This thesis is concerned with internalizing model transformations as ‘dynamic’ modalities in modal logic. The model-theoretic operations discussed here are (strong) simulations, homomorphisms, and functional powersets. For each of these transformations, we will extend the basic modal language with a modality, which expresses truth along this transformation. We then provide a sound and complete axiomatization for the new logic. As a part of the axiomatization of the simulation modality, we also study the so-called validity modality, which expresses whether a formula is a validity in a given logic. It is shown how to obtain a sound and complete axiomatization for this logic of validity, given an axiomatization and refutation system for the underlying logic. Finally, we show how the preservation laws for (strong) simulations and homomorphisms can be derived syntactically inside the logic. To this end, we provide a new proof of Lyndon’s positivity theorem in modal logic: a modal formula is preserved under homomorphisms iff it is equivalent to a positive existential formula.