Why Confluence is More Powerful than Ample Sets in Probabilistic and Non-Probabilistic Branching Time

Henri Hansen, Mark Timmer

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

12 Downloads (Pure)

Abstract

Confluence reduction and partial order reduction by means of ample sets are two different techniques for state space reduction in both traditional and probabilistic model checking. This presentation provides an extensive comparison between these two methods, answering the long-standing question of how they relate. We show that, while both preserve branching time properties, confluence reduction is strictly more powerful than partial order reduction: every reduction that can be obtained with partial order reduction can also be obtained with confluence reduction, but the converse is not true. A core problem in the comparison is that confluence reduction was de﬿ned in an action-based setting, whereas partial order reduction was de﬿ned in a state-based setting. We therefore rede﬿ne confluence reduction in the state-based setting of Markov decision processes, and discuss a nontrivial proof of its correctness. Additionally, we pinpoint precisely in what way confluence reduction is more general, and provide a restricted variant of confluence and relaxed variant of partial order reduction that exactly coincide. The results we present also hold for non-probabilistic models, as they can just as well be applied in a context where all transitions are non-probabilistic. To show the practical applicability 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 publication10th Workshop on Quantitative Aspects of Programming Languages (QAPL 2012)
Place of PublicationPisa
PublisherIstituto di Scienza e Tecnologie dell'Informazione
Pages-
Number of pages4
ISBN (Print)not assigned
Publication statusPublished - 1 Apr 2012

Publication series

Name
PublisherIstituto di Scienza e Tecnologie dell'Informazione

Keywords

  • METIS-286343
  • IR-80456
  • Markov Decision Processes
  • Probabilistic branching time
  • Confluence reduction
  • Partial order reduction
  • EWI-21805
  • Ample sets

Cite this

Hansen, H., & Timmer, M. (2012). Why Confluence is More Powerful than Ample Sets in Probabilistic and Non-Probabilistic Branching Time. In 10th Workshop on Quantitative Aspects of Programming Languages (QAPL 2012) (pp. -). Pisa: Istituto di Scienza e Tecnologie dell'Informazione.
Hansen, Henri ; Timmer, Mark. / Why Confluence is More Powerful than Ample Sets in Probabilistic and Non-Probabilistic Branching Time. 10th Workshop on Quantitative Aspects of Programming Languages (QAPL 2012). Pisa : Istituto di Scienza e Tecnologie dell'Informazione, 2012. pp. -
@inproceedings{4c8dc3b270284ef0be3ca58efb43f498,
title = "Why Confluence is More Powerful than Ample Sets in Probabilistic and Non-Probabilistic Branching Time",
abstract = "Confluence reduction and partial order reduction by means of ample sets are two different techniques for state space reduction in both traditional and probabilistic model checking. This presentation provides an extensive comparison between these two methods, answering the long-standing question of how they relate. We show that, while both preserve branching time properties, confluence reduction is strictly more powerful than partial order reduction: every reduction that can be obtained with partial order reduction can also be obtained with confluence reduction, but the converse is not true. A core problem in the comparison is that confluence reduction was de﬿ned in an action-based setting, whereas partial order reduction was de﬿ned in a state-based setting. We therefore rede﬿ne confluence reduction in the state-based setting of Markov decision processes, and discuss a nontrivial proof of its correctness. Additionally, we pinpoint precisely in what way confluence reduction is more general, and provide a restricted variant of confluence and relaxed variant of partial order reduction that exactly coincide. The results we present also hold for non-probabilistic models, as they can just as well be applied in a context where all transitions are non-probabilistic. To show the practical applicability 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-286343, IR-80456, Markov Decision Processes, Probabilistic branching time, Confluence reduction, Partial order reduction, EWI-21805, Ample sets",
author = "Henri Hansen and Mark Timmer",
year = "2012",
month = "4",
day = "1",
language = "Undefined",
isbn = "not assigned",
publisher = "Istituto di Scienza e Tecnologie dell'Informazione",
pages = "--",
booktitle = "10th Workshop on Quantitative Aspects of Programming Languages (QAPL 2012)",

}

Hansen, H & Timmer, M 2012, Why Confluence is More Powerful than Ample Sets in Probabilistic and Non-Probabilistic Branching Time. in 10th Workshop on Quantitative Aspects of Programming Languages (QAPL 2012). Istituto di Scienza e Tecnologie dell'Informazione, Pisa, pp. -.

Why Confluence is More Powerful than Ample Sets in Probabilistic and Non-Probabilistic Branching Time. / Hansen, Henri; Timmer, Mark.

10th Workshop on Quantitative Aspects of Programming Languages (QAPL 2012). Pisa : Istituto di Scienza e Tecnologie dell'Informazione, 2012. p. -.

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

TY - GEN

T1 - Why Confluence is More Powerful than Ample Sets in Probabilistic and Non-Probabilistic Branching Time

AU - Hansen, Henri

AU - Timmer, Mark

PY - 2012/4/1

Y1 - 2012/4/1

N2 - Confluence reduction and partial order reduction by means of ample sets are two different techniques for state space reduction in both traditional and probabilistic model checking. This presentation provides an extensive comparison between these two methods, answering the long-standing question of how they relate. We show that, while both preserve branching time properties, confluence reduction is strictly more powerful than partial order reduction: every reduction that can be obtained with partial order reduction can also be obtained with confluence reduction, but the converse is not true. A core problem in the comparison is that confluence reduction was de﬿ned in an action-based setting, whereas partial order reduction was de﬿ned in a state-based setting. We therefore rede﬿ne confluence reduction in the state-based setting of Markov decision processes, and discuss a nontrivial proof of its correctness. Additionally, we pinpoint precisely in what way confluence reduction is more general, and provide a restricted variant of confluence and relaxed variant of partial order reduction that exactly coincide. The results we present also hold for non-probabilistic models, as they can just as well be applied in a context where all transitions are non-probabilistic. To show the practical applicability 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 - Confluence reduction and partial order reduction by means of ample sets are two different techniques for state space reduction in both traditional and probabilistic model checking. This presentation provides an extensive comparison between these two methods, answering the long-standing question of how they relate. We show that, while both preserve branching time properties, confluence reduction is strictly more powerful than partial order reduction: every reduction that can be obtained with partial order reduction can also be obtained with confluence reduction, but the converse is not true. A core problem in the comparison is that confluence reduction was de﬿ned in an action-based setting, whereas partial order reduction was de﬿ned in a state-based setting. We therefore rede﬿ne confluence reduction in the state-based setting of Markov decision processes, and discuss a nontrivial proof of its correctness. Additionally, we pinpoint precisely in what way confluence reduction is more general, and provide a restricted variant of confluence and relaxed variant of partial order reduction that exactly coincide. The results we present also hold for non-probabilistic models, as they can just as well be applied in a context where all transitions are non-probabilistic. To show the practical applicability 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-286343

KW - IR-80456

KW - Markov Decision Processes

KW - Probabilistic branching time

KW - Confluence reduction

KW - Partial order reduction

KW - EWI-21805

KW - Ample sets

M3 - Conference contribution

SN - not assigned

SP - -

BT - 10th Workshop on Quantitative Aspects of Programming Languages (QAPL 2012)

PB - Istituto di Scienza e Tecnologie dell'Informazione

CY - Pisa

ER -

Hansen H, Timmer M. Why Confluence is More Powerful than Ample Sets in Probabilistic and Non-Probabilistic Branching Time. In 10th Workshop on Quantitative Aspects of Programming Languages (QAPL 2012). Pisa: Istituto di Scienza e Tecnologie dell'Informazione. 2012. p. -