Confluence versus Ample Sets in Probabilistic Branching Time

Henri Hansen, Mark Timmer

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

16 Downloads (Pure)

Abstract

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.
Original languageUndefined
Title of host publicationProceedings of the 3rd Young Researchers Workshop on Concurrency Theory
EditorsB. Bollig
Place of PublicationCachan, France
PublisherEcole normale superieure de Cachan
Pages-
Number of pages4
ISBN (Print)not assigned
Publication statusPublished - Sep 2011

Publication series

Name
PublisherÉcole normale supérieure de Cachan

Keywords

  • METIS-278793
  • IR-78024
  • Markov Decision Processes
  • Ample sets Probabilistic branching time
  • EWI-20500
  • Partial order reduction
  • EC Grant Agreement nr.: FP7/214755
  • EC Grant Agreement nr.: FP7-ICT-2007-1
  • Confluence reduction

Cite this

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.
Hansen, Henri ; Timmer, Mark. / Confluence versus Ample Sets in Probabilistic Branching Time. Proceedings of the 3rd Young Researchers Workshop on Concurrency Theory. editor / B. Bollig. Cachan, France : Ecole normale superieure de Cachan, 2011. pp. -
@inproceedings{cd66021530314c33b59abe0b0fc304d1,
title = "Confluence versus Ample Sets in Probabilistic Branching Time",
abstract = "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.",
keywords = "METIS-278793, IR-78024, Markov Decision Processes, Ample sets Probabilistic branching time, EWI-20500, Partial order reduction, EC Grant Agreement nr.: FP7/214755, EC Grant Agreement nr.: FP7-ICT-2007-1, Confluence reduction",
author = "Henri Hansen and Mark Timmer",
note = "Informal proceedings",
year = "2011",
month = "9",
language = "Undefined",
isbn = "not assigned",
publisher = "Ecole normale superieure de Cachan",
pages = "--",
editor = "B. Bollig",
booktitle = "Proceedings of the 3rd Young Researchers Workshop on Concurrency Theory",

}

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. Ecole normale superieure de Cachan, Cachan, France, pp. -.

Confluence versus Ample Sets in Probabilistic Branching Time. / Hansen, Henri; Timmer, Mark.

Proceedings of the 3rd Young Researchers Workshop on Concurrency Theory. ed. / B. Bollig. Cachan, France : Ecole normale superieure de Cachan, 2011. p. -.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

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

ER -

Hansen H, Timmer M. Confluence versus Ample Sets in Probabilistic Branching Time. In Bollig B, editor, Proceedings of the 3rd Young Researchers Workshop on Concurrency Theory. Cachan, France: Ecole normale superieure de Cachan. 2011. p. -