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

TitlePartial Order Reduction for Probabilistic Systems: A Revision for Distributed Schedulers
Publication TypeConference Paper
Year of Publication2009
AuthorsGiro, S, D'Argenio, PR, Ferrer Fioriti, LM
Conference NameCONCUR 2009 - Concurrency Theory, 20th International Conference
PublisherSpringer
ISBN Number978-3-642-04080-1
AbstractThe 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 local information. We show experimental results in which the elimination of the extra restriction leads to significant improvements.
DOI10.1007/978-3-642-04081-8_23
PDF (Full text): 
Powered by Drupal