Give Inconsistency a Chance: Semantics for Ontology-Mediated Verification

Research output: Contribution to book/conference proceedings/anthology/reportConference contributionContributedpeer-review

Contributors

Abstract

Recently, we have introduced ontologized programs as a for-
malism to link description logic ontologies with programs specified in
the guarded command language, the de-facto standard input formalism
for probabilistic model checking tools such as Prism, to allow for an
ontology-mediated verification of stochastic systems. Central to our ap-
proach is a complete separation of the two formalisms involved: guarded
command language to describe the dynamics of the stochastic system
and description logics are used to model background knowledge about
the system in an ontology. In ontologized programs, these two languages
are loosely coupled by an interface that mediates between these two
worlds. Under the original semantics defined for ontologized programs, a
program may enter a state that is inconsistent with the ontology, which
limits the capabilities of the description logic component. We approach
this issue in different ways by introducing consistency notions, and dis-
cuss two alternative semantics for ontologized programs. Furthermore,
we present complexity results for checking whether a program is consis-
tent under the different semantics.

Details

Original languageEnglish
Title of host publicationProceedings of the 33rd International Workshop on Description Logics (DL 2020)
PublisherCEUR-WS
Publication statusPublished - 2020
Peer-reviewedYes

Publication series

SeriesCEUR Workshop Proceedings
Volume2663
ISSN1613-0073

Keywords

Keywords

  • Give Inconsistency a Chance: Semantics for Ontology-Mediated Verification