Generating compact MTBDD-representations from Probmela specifications

Frank CiesinskiFrank Ciesinski, Christel BaierChristel Baier, Marcus GrößerMarcus Größer, David ParkerDavid Parker

DOI Link

Frank Ciesinski, Christel Baier, Marcus Größer, David Parker
Generating compact MTBDD-representations from Probmela specifications
Proc. of the 15th International SPIN Workshop on Model Checking of Software (SPIN), volume 5156 of Lecture Notes in Computer Science, 60--76, 2008. Springer

Details
Bibtex

KurzfassungAbstract
The purpose of the paper is to provide an automatic transformation 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 symbolic 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 checkers PRISM and LiQuor, our translation supports comparative studies of different verification paradigms and can serve to use the (more comfortable) 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 efficiency of the translation and (3) the compactness of the symbolic BDD-representation of the generated PRISM-language specifications.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-540-85114-1_7.

@inproceedings{CBGP2008,
  author    = {Frank Ciesinski and Christel Baier and Marcus Gr{\"{o}}{\ss}er
               and David Parker},
  title     = {Generating compact {MTBDD-representations} from Probmela
               specifications},
  booktitle = {Proc. of the 15th International {SPIN} Workshop on Model Checking
               of Software (SPIN)},
  series    = {Lecture Notes in Computer Science},
  volume    = {5156},
  publisher = {Springer},
  year      = {2008},
  pages     = {60--76},
  doi       = {10.1007/978-3-540-85114-1_7}
}