| Identifikační kód | RIV/00216224:14330/11:00067395 |
|---|
| Název v anglickém jazyce | Automated Verification Techniques for Probabilistic Systems |
|---|
| Druh | D - Článek ve sborníku |
|---|
| Jazyk | eng - angličtina |
|---|
| Obor - skupina | I - Informatika |
|---|
| Obor | IN - Informatika |
|---|
| Rok uplatnění | 2011 |
|---|
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
|---|
| Počet výskytů výsledku | 1 |
|---|
| Počet tvůrců celkem | 4 |
|---|
| Počet domácích tvůrců | 1 |
|---|
| Výčet všech uvedených jednotlivých tvůrců | Vojtěch Forejt (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 2477912)
Marta Kwiatkowska (státní příslušnost: GB - Spojené království Velké Británie a Severního Irska)
Gethin Norman (státní příslušnost: GB - Spojené království Velké Británie a Severního Irska)
David Parker (státní příslušnost: GB - Spojené království Velké Británie a Severního Irska) |
|---|
| Popis výsledku v anglickém jazyce | This tutorial provides an introduction to probabilistic model checking, a technique for automatically verifying quantitative properties of probabilistic systems. We focus on Markov decision processes (MDPs), which model both stochastic and nondeterministic behaviour. We describe methods to analyse a wide range of their properties, including specifications in the temporal logics PCTL and LTL, probabilistic safety properties and cost- or reward-based measures. We also discuss multi-objective probabilisticmodel checking, used to analyse trade-offs between several different quantitative properties. Applications of the techniques in this tutorial include performance and dependability analysis of networked systems, communication protocols and randomised distributed algorithms. Since such systems often comprise several components operating in parallel, we also cover techniques for compositional modelling and verification of multi-component probabilistic systems. |
|---|
| Klíčová slova oddělená středníkem | tutorial; pctl model checking; markov decision processes |
|---|
| Stránka www, na které se nachází výsledek | - |
|---|
| DOI výsledku | 10.1007/978-3-642-21455-4_3 |
|---|