Model Checking Meets Probability: A Gentle Introduction
| Title | Model Checking Meets Probability: A Gentle Introduction |
| Publication Type | Book Chapter |
| Year of Publication | 2013 |
| Authors | Katoen, J-P |
| Book Title | Engineering Dependable Software Systems |
| Series Title | NATO Science for Peace and Security Series - D: Information and Communication Security |
| Volume | 34 |
| Pagination | 177–205 |
| Publisher | IOS Press |
| City | Amsterdam |
| ISBN | 1874-6268 |
| Abstract | This 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
