Partial order reduction for probabilistic systems assuming distributed schedulers

Abstract. In the verification of probabilistic systems, distributed sched-ulers are used to obtain tight bounds on worst-case probabilities, these bounds being more realistic than the ones obtained by considering un-restricted full-history dependent schedulers. In this paper, we define two classes of distributed schedulers. We present undecidability results re-lated to the automatic verification under these classes of schedulers. In previous literature, we have proven that the model checking problem is undecidable for distributed schedulers. However, in this paper we show that, by assuming that the schedulers are in a given class, the technique of partial order reduction (POR) for LTL properties can be applied in a more efficient way than usual, thus yielding a system with less states and transitions than if reduced assuming unrestricted schedulers. The reduced system can then be analysed using well-known algorithms for full-history dependent schedulers. Our partial order reduction technique may also obtain bounds strictly tighter than the ones obtained by con-sidering unrestricted schedulers (of course, such bounds are safe with respect to the class of schedulers under consideration). We explain that the two variants we present are obtained from a general theorem, thus raising the question of whether there are other “natural ” classes of sched-ulers for which POR variants can be developed.