In this paper, 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 of interest. Using this framework we study verification and adversarial synthesis for specifications expressed in a variant of first-order μ-calculus, with a controlled form of quantification across successive states. We provide key decidability results for both verification and synthesis, under a "bounded-state" assumption. We then study two instantiations of this general framework, where the description logic knowledge base is expressed in DL-Lite and scriptAscriptLscriptCscriptQscriptI, respectively. © 2013 Springer-Verlag.

Verification and synthesis in description logic based dynamic systems / Diego, Calvanese; De Giacomo, Giuseppe; Marco, Montali; Patrizi, Fabio. - STAMPA. - 7994 LNCS:(2013), pp. 50-64. (Intervento presentato al convegno 7th International Conference on Web Reasoning and Rule Systems, RR 2013 tenutosi a Mannheim nel 27 July 2013 through 29 July 2013) [10.1007/978-3-642-39666-3_5].

Verification and synthesis in description logic based dynamic systems

DE GIACOMO, Giuseppe;PATRIZI, FABIO
2013

Abstract

In this paper, 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 of interest. Using this framework we study verification and adversarial synthesis for specifications expressed in a variant of first-order μ-calculus, with a controlled form of quantification across successive states. We provide key decidability results for both verification and synthesis, under a "bounded-state" assumption. We then study two instantiations of this general framework, where the description logic knowledge base is expressed in DL-Lite and scriptAscriptLscriptCscriptQscriptI, respectively. © 2013 Springer-Verlag.
2013
7th International Conference on Web Reasoning and Rule Systems, RR 2013
automated verification and synthesis; description logics; processes
04 Pubblicazione in atti di convegno::04c Atto di convegno in rivista
Verification and synthesis in description logic based dynamic systems / Diego, Calvanese; De Giacomo, Giuseppe; Marco, Montali; Patrizi, Fabio. - STAMPA. - 7994 LNCS:(2013), pp. 50-64. (Intervento presentato al convegno 7th International Conference on Web Reasoning and Rule Systems, RR 2013 tenutosi a Mannheim nel 27 July 2013 through 29 July 2013) [10.1007/978-3-642-39666-3_5].
File allegati a questo prodotto
File Dimensione Formato  
VE_2013_11573-531055.pdf

solo gestori archivio

Tipologia: Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 290.9 kB
Formato Adobe PDF
290.9 kB Adobe PDF   Contatta l'autore

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11573/531055
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 17
  • ???jsp.display-item.citation.isi??? 6
social impact