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.
|Title of host publication||Engineering Dependable Software Systems|
|Place of Publication||Amsterdam|
|Number of pages||29|
|Publication status||Published - 2013|
|Name||NATO Science for Peace and Security Series - D: Information and Communication Security|
Katoen, J. P. (2013). Model checking meets probability: a gentle introduction. In Engineering Dependable Software Systems (pp. 177-205). (NATO Science for Peace and Security Series - D: Information and Communication Security; Vol. 34, No. 34). Amsterdam: IOS Press. https://doi.org/10.3233/978-1-61499-207-3-177