Distributed probabilistic input/output automata: Expressiveness, (un)decidability and algorithms

In this paper, we provide an overview of the work we have done in the last years which includes: (1) the definitions of distributed and strongly distributed schedulers, providing motivation and intuition; (2) expressiveness results, comparing them to restricted versions such as deterministic variants or finite-memory variants; (3) undecidability results-in particular the model checking problem is not decidable in general when restricting to distributed schedulers; (4) a counterexample-guided refinement technique that, using standard probabilistic model checking, allows to increase precision in the actual bounds in the distributed setting; and (5) a revision of the partial order reduction technique for probabilistic model checking. We conclude the paper with an extensive review of related work dealing with similar approaches to ours.