Partial Order Reduction for Probabilistic Branching Time

Christel BaierChristel Baier, Pedro R. D'ArgenioPedro R. D'Argenio, Marcus GrößerMarcus Größer

DOI Link

Christel Baier, Pedro R. D'Argenio, Marcus Größer
Partial Order Reduction for Probabilistic Branching Time
Proc. of the Third Workshop on Quantitative Aspects of Programming Languages (QAPL), volume 153(2) of Electronic Notes in Theoretical Computer Science, 97--116, 2005. Elsevier

Details
Bibtex

KurzfassungAbstract
In the past, partial order reduction has been used successfully to combat the state explosion problem in the context of model checking for non-probabilistic systems. For both linear time and branching time specifications, methods have been developed to apply partial order reduction in the context of model checking. Only recently, results were published that give criteria on applying partial order reduction for verifying quantitative linear time properties for probabilistic systems. This paper presents partial order reduction criteria for Markov decision processes and branching time properties, such as formulas of probabilistic computation tree logic. Moreover, we provide a comparison of the results established so far about reduction conditions for Markov decision processes.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@inproceedings{B{G2005,
  author    = {Christel Baier and Pedro R. {D'Argenio} and Marcus
               Gr{\"{o}}{\ss}er},
  title     = {Partial Order Reduction for Probabilistic Branching Time},
  booktitle = {Proc. of the Third Workshop on Quantitative Aspects of
               Programming Languages (QAPL)},
  series    = {Electronic Notes in Theoretical Computer Science},
  volume    = {153(2)},
  publisher = {Elsevier},
  year      = {2005},
  pages     = {97--116},
  doi       = {10.1016/J.ENTCS.2005.10.034}
}