Name
Abstract | ||
|---|---|---|
The purpose of the paper is to provide an automatic trans- formation of parallel programs of an imperative probabilistic guarded command language (called Probmela) into probabilistic reactive module specifications. The latter serve as basis for the input language of the sym- bolic MTBDD-based probabilistic model checker PRISM, while Probmela is the modeling language of the model checker LiQuor which relies on an enumerative approach and supports partial order reduction and other reduction techniques. By providing the link between the model check- ers PRISM and LiQuor, our translation supports comparative studies of dierent verification paradigms and can serve to use the (more com- fortable) guarded command language for a MTBDD-based quantitative analysis. The challenges were (1) to ensure that the translation preserves the Markov decision process semantics, (2) the eciency of the transla- tion and (3) the compactness of the symbolic BDD-representation of the generated PRISM-language specifications. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/978-3-540-85114-1_7 | SPIN |
DocType | Citations | PageRank |
Conference | 2 | 0.39 |
References | Authors | |
11 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Frank Ciesinski | 1 | 299 | 14.52 |
| Christel Baier | 2 | 3053 | 185.85 |
| Marcus Größer | 3 | 334 | 18.23 |
| David Parker | 4 | 4018 | 184.00 |