On the expressive power of schedulers in distributed probabilistic systems

In this paper, we consider several subclasses of distributed schedulers and we investigate the ability of these subclasses to attain worst-case probabilities. Based on previous work, we consider the class of distributed schedulers, and we prove that randomization adds no extra power to distributed schedulers when trying to attain the supremum probability of any measurable set, thus showing that the subclass of deterministic schedulers suffices to attain the worst-case probability. Traditional schedulers are a particular case of distributed schedulers. So, since our result holds for any measurable set, our proof generalizes the well-known result that randomization adds no extra power to schedulers when trying to maximize the probability of an ω-regular language. However, non-Markovian schedulers are needed to attain supremum probabilities in distributed systems. We develop another class of schedulers (the strongly distributed schedulers) that restricts the nondetermin-ism concerning the order in which components execute. We compare this class against previous approaches in the same direction, showing that our definition is an important contribution. For this class, we show that randomized and non-Markovian schedulers are needed to attain worst-case probabilities. We also discuss the subclass of finite-memory schedulers, showing the intractability of the model checking problem for these schedulers