Model Checking Meets Probability: A Gentle Introduction

TitleModel Checking Meets Probability: A Gentle Introduction
Publication TypeBook Chapter
Year of Publication2013
AuthorsKatoen, J-P
Book TitleEngineering Dependable Software Systems
Series TitleNATO Science for Peace and Security Series - D: Information and Communication Security
Volume34
Pagination177–205
PublisherIOS Press
CityAmsterdam
ISBN1874-6268
AbstractThis paper considers fully probabilistic system models. Each transition is quantified with a probability–-its likelihood of occurrence. Properties are expressed as automata that either accept or reject system runs. The central question is to determine the fraction of accepted system runs. We also consider probabilistic timed system models. Their properties are timed automata that accept timed runs iff all timing constraints resent in the automaton are met; otherwise it rejects. The central question is to determine the fraction of accepted timed system runs.
Work Package: 
WP1