Sciweavers

Share
CONCUR
2009
Springer

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

8 years 10 months ago
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...
Sergio Giro, Pedro R. D'Argenio, Luis María
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Where CONCUR
Authors Sergio Giro, Pedro R. D'Argenio, Luis María Ferrer Fioriti
Comments (0)
books