Dynamic Systems based on Description Logics: Formalization, verification, and synthesis

We devise a general framework for formalizing Dynamic Systems centered around a Description Logic knowledge base. Our framework is parametric w.r.t. both the description logic and the progression mechanism. For such kinds of systems, we provide general decidability results for verification and adversarial synthesis of first-order μ-calculus properties under a natural assumption which we call "state-boundedness". We then apply such results to the case of DL-Lite and ALCQIknowledge bases and a progression mechanism grounded in epistemic first-order queries.