To improve the efficiency of model checking in general, and probabilistic model checking in particular, several reduction techniques have been introduced. Two of these, confluence reduction and partial-order reduction by means of ample sets, are based on similar principles, and both preserve branching-time properties for probabilistic models. Confluence reduction has been introduced for probabilistic automata, whereas ample set reduction has been introduced for Markov decision processes. In this presentation we will explore the relationship between confluence and ample sets. To this end, we redefine confluence reduction to handle MDPs. We show that all non-trivial ample sets consist of confluent transitions, but that the converse is not true. We also show that the two notions coincide if the definition of confluence is restricted, and point out the relevant parts where the two theories differ. The results we present also hold for non-probabilistic models, as our theorems can just as well be applied in a context where all transitions are non-probabilistic. To show a practical application of our results, we adapt a state space generation technique based on representative states, already known in combination with confluence reduction, so that it can also be applied with partial-order reduction.
|Title of host publication||Proceedings of the 3rd Young Researchers Workshop on Concurrency Theory|
|Place of Publication||Cachan, France|
|Publisher||Ecole normale superieure de Cachan|
|Number of pages||4|
|ISBN (Print)||not assigned|
|Publication status||Published - Sep 2011|
|Publisher||École normale supérieure de Cachan|
- Markov Decision Processes
- Ample sets Probabilistic branching time
- Partial order reduction
- EC Grant Agreement nr.: FP7/214755
- EC Grant Agreement nr.: FP7-ICT-2007-1
- Confluence reduction
Hansen, H., & Timmer, M. (2011). Confluence versus Ample Sets in Probabilistic Branching Time. In B. Bollig (Ed.), Proceedings of the 3rd Young Researchers Workshop on Concurrency Theory (pp. -). Cachan, France: Ecole normale superieure de Cachan.