Automated Verification Techniques for Probabilistic Systems

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F11%3A00067395" target="_blank" >RIV/00216224:14330/11:00067395 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-642-21455-4_3" target="_blank" >http://dx.doi.org/10.1007/978-3-642-21455-4_3</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-642-21455-4_3" target="_blank" >10.1007/978-3-642-21455-4_3</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Automated Verification Techniques for Probabilistic Systems

Popis výsledku v původní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.

Název v anglickém jazyce

Automated Verification Techniques for Probabilistic Systems

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/1M0545" target="_blank" >1M0545: Institut Teoretické Informatiky</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2011

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Formal Methods for Eternal Networked Software Systems (SFM'11)

ISBN

9783642214547

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

61

Strana od-do

53-113

Název nakladatele

Springer

Místo vydání

Berlin, Germany

Místo konání akce

Bertinoro, Italy

Datum konání akce

1. 1. 2011

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—