Enhancing Probabilistic Model Checking with Ontologies

Publikation: Beitrag in FachzeitschriftForschungsartikelBeigetragenBegutachtung

Beitragende

Abstract

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.

Details

OriginalspracheEnglisch
Seiten (von - bis)885–921
Seitenumfang37
FachzeitschriftFormal Aspects of Computing
Jahrgang33
Ausgabenummer6
PublikationsstatusVeröffentlicht - 26 Mai 2021
Peer-Review-StatusJa

Externe IDs

Scopus 85106487294

Schlagworte

Schlagwörter

  • Context dependent systems analysis, Description logics, Ontologies, Ontology-mediated verification, Probabilisticmodel checking

Bibliotheksschlagworte