TY - GEN
T1 - Ontology-Mediated Probabilistic Model Checking
AU - Dubslaff, Clemens
AU - Koopmann, Patrick
AU - Turhan, Anni-Yasmin
PY - 2019
Y1 - 2019
N2 - Probabilistic model checking (PMC) is a well-established method for the quantitative analysis of dynamic systems. Description logics (DLs) provide a well-suited formalism to describe and reason about terminological knowledge, used in many areas to specify background knowledge on the domain. We investigate how such knowledge can be integrated into the PMC process, introducing ontology-mediated PMC. Specifically, we propose a formalism that links ontologies to dynamic behaviors specified by guarded commands, the de-facto standard input formalism for PMC tools such as Prism. Further, we present and implement a technique for their analysis relying on existing DL-reasoning and PMC tools. This way, we enable the application of standard PMC techniques to analyze knowledge-intensive systems. Our approach is implemented and evaluated on a multi-server system case study, where different DL-ontologies are used to provide specifications of different server platforms and situations the system is executed in.
AB - Probabilistic model checking (PMC) is a well-established method for the quantitative analysis of dynamic systems. Description logics (DLs) provide a well-suited formalism to describe and reason about terminological knowledge, used in many areas to specify background knowledge on the domain. We investigate how such knowledge can be integrated into the PMC process, introducing ontology-mediated PMC. Specifically, we propose a formalism that links ontologies to dynamic behaviors specified by guarded commands, the de-facto standard input formalism for PMC tools such as Prism. Further, we present and implement a technique for their analysis relying on existing DL-reasoning and PMC tools. This way, we enable the application of standard PMC techniques to analyze knowledge-intensive systems. Our approach is implemented and evaluated on a multi-server system case study, where different DL-ontologies are used to provide specifications of different server platforms and situations the system is executed in.
UR - http://www.scopus.com/inward/record.url?scp=85076948225&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-34968-4_11
DO - 10.1007/978-3-030-34968-4_11
M3 - Conference contribution
SN - 9783030349677
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 194
EP - 211
BT - Integrated Formal Methods - 15th International Conference, IFM 2019, Proceedings
A2 - Ahrendt, W.
A2 - Tapia Tarifa, S.
PB - Springer
T2 - 15th International Conference on Integrated Formal Methods, IFM 2019
Y2 - 2 December 2019 through 6 December 2019
ER -