Enhancing Probabilistic Model Checking with Ontologies

Clemens DubslaffClemens Dubslaff, Patrick KoopmannPatrick Koopmann, Anni-Yasmin TurhanAnni-Yasmin Turhan

DOI Link

Clemens Dubslaff, Patrick Koopmann, Anni-Yasmin Turhan
Enhancing Probabilistic Model Checking with Ontologies
Formal Aspects of Computing, 2021

Details
Bibtex

KurzfassungAbstract
Probabilistic model checking (PMC) is a well-established method for the quantitative analysis of state based operational models such as Markov decision processes. Description logics (DLs) provide a well-suited formalism to describe and reason about knowledge and are used as basis for the web ontology language (OWL). We investigate how such knowledge described by DLs can be integrated into the PMC process, introducing ontology-mediated PMC. Specifically, we propose ontologized programs as a formalism that links ontologies to behaviors specified by probabilistic guarded commands, the de-facto standard input formalism for PMC tools such as Prism. Through DL reasoning, inconsistent states in the modeled system can be detected. We present three ways to resolve these inconsistencies, leading to different Markov decision process semantics. We analyze the computational complexity of checking whether an ontologized program is consistent under these semantics. Further, we present and implement a technique for the quantitative analysis of ontologized programs relying on standard DL reasoning and PMC tools. This way, we enable the application of PMC techniques to analyze knowledge-intensive systems.We evaluate our approach and implementation on amulti-server systemcase study,where different DL ontologies are used to provide specifications of different server platforms and situations the system is executed in.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@article{DKT2021,
  author  = {Clemens Dubslaff and Patrick Koopmann and Anni-Yasmin Turhan},
  title   = {Enhancing Probabilistic Model Checking with Ontologies},
  journal = {Formal Aspects of Computing},
  year    = {2021},
  doi     = {10.1007/s00165-021-00549-0}
}