Name
Abstract | ||
|---|---|---|
A wide range of coordination protocols for distributed systems, internet protocols or systems with unreliable components can formally be modelled by Markov decision processes (MDP). MDPs can be viewed as a variant of state-transition diagrams with discrete probabilities and nondeterminism. While traditional model checking techniques for non-probabilistic systems aim to establish properties stating that all (or some) computations fulfill a certain condition, the verification problem for randomized systems requires reasoning about the quantitative behavior by means of properties that refer to the probabilities for certain computations, for instance, the probability to find a leader within 5 rounds or the probability for not reaching an error state.The paper starts with a brief introduction into modelling randomized systems with MDPs and the modelling language ProbMela which is a guarded command language with features of imperative languages, nondeterminism, parallelism, a probabilistic choice operator and lossy channels. We summarize the main steps for a quantitative analysis of MDPs against linear temporal logical specifications. The last part will report on the main features of the partial order reduction approach for MDPs and its implementation in the model checker LiQuor. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1145/1081180.1081182 | Proceedings of the 10th international workshop on Formal methods for industrial critical systems |
Keywords | DocType | ISBN |
certain computation,randomized protocol,imperative language,main step,main feature,quantitative analysis,randomized system,modelling language probmela,guarded command language,certain condition,model checker liquor,discrete probability,distributed system,linear temporal logic,partial order reduction,state transition diagram,model checking,internet protocol,markov decision process | Conference | 1-59593-148-1 |
Citations | PageRank | References |
2 | 0.36 | 18 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Christel Baier | 1 | 3053 | 185.85 |
| Frank Ciesinski | 2 | 299 | 14.52 |
| Marcus Groesser | 3 | 44 | 2.32 |