Static Partial Order Reduction for Probabilistic Concurrent Systems

Álvaro Fernández DíazÁlvaro Fernández Díaz, Christel BaierChristel Baier, Clara Benac EarleClara Benac Earle, Lars-Åke FredlundLars-Åke Fredlund

DOI Link

Álvaro Fernández Díaz, Christel Baier, Clara Benac Earle, Lars-Åke Fredlund
Static Partial Order Reduction for Probabilistic Concurrent Systems
Proc. of the 9th International Conference on Quantitative Evaluation of Systems (QEST), 104--113, 2012. IEEE Computer Society Press

Details
Bibtex

KurzfassungAbstract
Sound criteria for partial order reduction for probabilistic concurrent systems have been presented in the literature. Their realization relies on a depth-first search-based approach for generating the reduced model. The drawback of this dynamic approach is that it can hardly be combined with other techniques to tackle the state explosion problem, e.g., symbolic probabilistic model checking with multi-terminal variants of binary decision diagrams. Following the approach presented by Kurshan et al. for non-probabilistic systems, we study partial order reduction techniques for probabilistic concurrent systems that can be realized by a static analysis. The idea is to inject the reduction criteria into the control flow graphs of the processes of the system to be analyzed. We provide the theoretical foundations of static partial order reduction for probabilistic concurrent systems and present algorithms to realize them. Finally, we report on some experimental results.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@inproceedings{DBEF2012,
  author    = {{\'{A}}lvaro Fern{\'{a}}ndez D{\'{\i}}az and Christel Baier and
               Clara Benac Earle and Lars-{\AA}ke Fredlund},
  title     = {Static Partial Order Reduction for Probabilistic Concurrent
               Systems},
  booktitle = {Proc. of the 9th International Conference on Quantitative
               Evaluation of Systems (QEST)},
  publisher = {IEEE Computer Society Press},
  year      = {2012},
  pages     = {104--113},
  doi       = {10.1109/QEST.2012.22}
}