We devise a general framework for formalizing Description Logic Based Dynamic Systems that is parametric w.r.t. the description logic knowledge base and the progression mechanism. We study verification and adversarial syn- thesis for specifications expressed in a variant of first-order -calculus, with a controlled form of quantification across successive states. We provide key de- cidability results for both verification and synthesis, under a "bounded-state" assumption. We then study two instantiations of this general framework, where the knowledge base is expressed in DL-Lite andALCQI, respectively.
['Diego Calvanese', 'Giuseppe De Giacomo', 'Marco Montali', 'Fabio Patrizi']
Verification and Synthesis in Description Logic Based Dynamic Systems (Abridged Version)