Partial Order Reduction for Probabilistic Systems: A Revision for Distributed Schedulers

Abstract. The technique of partial order reduction (POR) for probabilistic model checking prunes the state space of the model so that a maximizing scheduler and a minimizing one persist in the reduced system. This technique extends Peled’s original restrictions with a new one specially tailored to deal with probabilities. It has been argued that not all schedulers provide appropriate resolutions of nondeterminism and they yield overly safe answers on systems of distributed nature or that partially hide information. In this setting, maximum and minimum probabilities are obtained considering only the subset of so-called distributed or partial information schedulers. In this article we revise the technique of partial order reduction (POR) for LTL properties applied to probabilistic model checking. Our reduction ensures that distributed schedulers are preserved. We focus on two classes of distributed schedulers and show that Peled’s restrictions are valid whenever schedulers use only l...

• Type: Conference
• Year: 2009
• Where: CONCUR
• Authors: Sergio Giro, Pedro R. D'Argenio, Luis María Ferrer Fioriti
• Keywords: CONCUR 2009, Distributed And Parallel Computing, Partial Information Schedulers, Partial Order Reduction, Probabilistic Model Checking