TY - GEN

T1 - Confluence versus Ample Sets in Probabilistic Branching Time

AU - Hansen, Henri

AU - Timmer, Mark

N1 - Informal proceedings

PY - 2011/9

Y1 - 2011/9

N2 - 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.

AB - 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.

KW - METIS-278793

KW - IR-78024

KW - Markov Decision Processes

KW - Ample sets Probabilistic branching time

KW - EWI-20500

KW - Partial order reduction

KW - EC Grant Agreement nr.: FP7/214755

KW - EC Grant Agreement nr.: FP7-ICT-2007-1

KW - Confluence reduction

M3 - Conference contribution

SN - not assigned

SP - -

BT - Proceedings of the 3rd Young Researchers Workshop on Concurrency Theory

A2 - Bollig, B.

PB - Ecole normale superieure de Cachan

CY - Cachan, France

Y2 - 10 September 2011 through 10 September 2011

ER -