@inproceedings{ DBLP:conf/ecai/HaririCGMFM12,
  author = {Babak Bagheri Hariri and
               Diego Calvanese and
               Giuseppe {De Giacomo} and
               Riccardo De Masellis and
               Paolo Felli and
               Marco Montali},
  title = {Verification of Description Logic Knowledge and Action Bases},
  booktitle = {{ECAI} 2012 - 20th European Conference on Artificial Intelligence.
               Including Prestigious Applications of Artificial Intelligence {(PAIS-2012)}
               System Demonstrations Track, Montpellier, France, August 27-31 , 2012},
  year = {2012},
  pages = {103--108},
  crossref = {DBLP:conf/ecai/2012},
  url = {http://dx.doi.org/10.3233/978-1-61499-098-7-103},
  doi = {10.3233/978-1-61499-098-7-103},
  abstract = {Description logic Knowledge and Action Bases (KAB) are a mechanism for providing both a semantically rich representation of the information on the domain of interest in terms of a description logic knowledge base and actions to change such information over time, possibly introducing new objects. We resort to a variant of DL-Lite where UNA is not enforced and where equality between objects may be asserted and inferred. Actions are specified as sets of conditional effects, where conditions are based on epistemic queries over the knowledge base (TBox and ABox), and effects are expressed in terms of new ABoxes. In this setting, we address verification of temporal properties expressed in a variant of first-order μ-calculus with quantification across states. Notably, we show decidability of verification, under a suitable restriction inspired by the notion of weak acyclicity in data exchange.}
}

{"_id":{"_str":"54183d53ffe14fcc4f000ce2"},"__v":0,"authorIDs":["5457757b2abc8e9f37000408"],"author_short":["Hariri, B.<nbsp>B.","Calvanese, D.","De Giacomo, G.","Masellis, R.<nbsp>D.","Felli, P.","Montali, M."],"bibbaseid":"hariri-calvanese-degiacomo-masellis-felli-montali-verificationofdescriptionlogicknowledgeandactionbases-2012","bibdata":{"abstract":"Description logic Knowledge and Action Bases (KAB) are a mechanism for providing both a semantically rich representation of the information on the domain of interest in terms of a description logic knowledge base and actions to change such information over time, possibly introducing new objects. We resort to a variant of DL-Lite where UNA is not enforced and where equality between objects may be asserted and inferred. Actions are specified as sets of conditional effects, where conditions are based on epistemic queries over the knowledge base (TBox and ABox), and effects are expressed in terms of new ABoxes. In this setting, we address verification of temporal properties expressed in a variant of first-order μ-calculus with quantification across states. Notably, we show decidability of verification, under a suitable restriction inspired by the notion of weak acyclicity in data exchange.","author":["Hariri, Babak Bagheri","Calvanese, Diego","De Giacomo, Giuseppe","Masellis, Riccardo De","Felli, Paolo","Montali, Marco"],"author_short":["Hariri, B.<nbsp>B.","Calvanese, D.","De Giacomo, G.","Masellis, R.<nbsp>D.","Felli, P.","Montali, M."],"bibtex":"@inproceedings{ DBLP:conf/ecai/HaririCGMFM12,\n author = {Babak Bagheri Hariri and\n Diego Calvanese and\n Giuseppe {De Giacomo} and\n Riccardo De Masellis and\n Paolo Felli and\n Marco Montali},\n title = {Verification of Description Logic Knowledge and Action Bases},\n booktitle = {{ECAI} 2012 - 20th European Conference on Artificial Intelligence.\n Including Prestigious Applications of Artificial Intelligence {(PAIS-2012)}\n System Demonstrations Track, Montpellier, France, August 27-31 , 2012},\n year = {2012},\n pages = {103--108},\n crossref = {DBLP:conf/ecai/2012},\n url = {http://dx.doi.org/10.3233/978-1-61499-098-7-103},\n doi = {10.3233/978-1-61499-098-7-103},\n abstract = {Description logic Knowledge and Action Bases (KAB) are a mechanism for providing both a semantically rich representation of the information on the domain of interest in terms of a description logic knowledge base and actions to change such information over time, possibly introducing new objects. We resort to a variant of DL-Lite where UNA is not enforced and where equality between objects may be asserted and inferred. Actions are specified as sets of conditional effects, where conditions are based on epistemic queries over the knowledge base (TBox and ABox), and effects are expressed in terms of new ABoxes. In this setting, we address verification of temporal properties expressed in a variant of first-order μ-calculus with quantification across states. Notably, we show decidability of verification, under a suitable restriction inspired by the notion of weak acyclicity in data exchange.}\n}","bibtype":"inproceedings","booktitle":"ECAI 2012 - 20th European Conference on Artificial Intelligence. Including Prestigious Applications of Artificial Intelligence (PAIS-2012) System Demonstrations Track, Montpellier, France, August 27-31 , 2012","crossref":"DBLP:conf/ecai/2012","doi":"10.3233/978-1-61499-098-7-103","id":"DBLP:conf/ecai/HaririCGMFM12","key":"DBLP:conf/ecai/HaririCGMFM12","pages":"103--108","title":"Verification of Description Logic Knowledge and Action Bases","type":"inproceedings","url":"http://dx.doi.org/10.3233/978-1-61499-098-7-103","year":"2012","bibbaseid":"hariri-calvanese-degiacomo-masellis-felli-montali-verificationofdescriptionlogicknowledgeandactionbases-2012","role":"author","urls":{"Paper":"http://dx.doi.org/10.3233/978-1-61499-098-7-103"},"downloads":2,"html":""},"bibtype":"inproceedings","biburl":"http://www.dis.uniroma1.it/~felli/inc/bib.bib","creationDate":"2014-09-16T13:38:27.535Z","downloads":2,"keywords":[],"search_terms":["verification","description","logic","knowledge","action","bases","hariri","calvanese","de giacomo","masellis","felli","montali"],"title":"Verification of Description Logic Knowledge and Action Bases","year":2012,"dataSources":["sE2LX8PQvdW3BDkaj"]}