loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
The Quantitative Evaluation of Systems, First International Conference on (QEST'04)
Partial Order Reduction on Concurrent Probabilistic Programs
Enschede, the Netherlands
September 27-September 30
ISBN: 0-7695-2185-1
Pedro R. D'Argenio, Universit? de Provence, France
Peter Niebert, Universit? de Provence, France
Partial order reduction has been used to alleviate the state explosion problem in model checkers for nondeterministic systems. The method relies on exploring only a fragment of the full state space of a program that is enough to assess the validity of a property. In this paper, we discuss partial order reduction for probabilistic programs represented as Markov decision processes. The technique we propose preserves probabilistic quantification of reachability properties and is based on partial order reduction techniques for (non probabilistic) branching temporal logic. We also show that techniques for (non probabilistic) linear temporal logics are not correct for probabilistic reachability and that in turn our method is not sufficient for probabilistic CTL. We conjecture that our reduction technique also preserves maximum and minimum probabilities of next-free LTL properties.
Citation:
Pedro R. D'Argenio, Peter Niebert, "Partial Order Reduction on Concurrent Probabilistic Programs," qest, pp.240-249, The Quantitative Evaluation of Systems, First International Conference on (QEST'04), 2004
Usage of this product signifies your acceptance of the Terms of Use.