A comparison of confluence and ample sets in probabilistic and non-probabilistic branching time

Henri Hansen, M. Massink (Editor), G. Norman (Editor), Mark Timmer, H. Wiklicky (Editor)

Research output: Contribution to journalArticleAcademicpeer-review

3 Citations (Scopus)
46 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 paper provides an extensive comparison between these two methods, and answers the question how they relate in terms of reduction power when preserving branching time properties. We prove that, while both preserve the same 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. The main challenge for the comparison is that confluence reduction was defined in an action-based setting, whereas ample set reduction is often defined in a state-based setting. We therefore redefine confluence reduction in the state-based setting of Markov decision processes, and provide a nontrivial proof of its correctness. Additionally, we pinpoint precisely in what way confluence reduction is more general, and provide conditions under which the two notions 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 discuss 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 to ample sets.
Original languageUndefined
Pages (from-to)103-123
Number of pages21
JournalTheoretical computer science
Volume538
DOIs
Publication statusPublished - 12 Jun 2014

Keywords

  • EC Grant Agreement nr.: FP7/2007-2013
  • EC Grant Agreement nr.: FP7/214755
  • EWI-24771
  • Partial order reduction
  • IR-91462
  • Confluence reduction
  • Markov Decision Processes
  • Ample sets
  • METIS-305895
  • Probabilistic branching time

Cite this

Hansen, Henri ; Massink, M. (Editor) ; Norman, G. (Editor) ; Timmer, Mark ; Wiklicky, H. (Editor). / A comparison of confluence and ample sets in probabilistic and non-probabilistic branching time. In: Theoretical computer science. 2014 ; Vol. 538. pp. 103-123.
@article{62dece1fee0b425fb71c7be840697612,
title = "A comparison of confluence and 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 paper provides an extensive comparison between these two methods, and answers the question how they relate in terms of reduction power when preserving branching time properties. We prove that, while both preserve the same 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. The main challenge for the comparison is that confluence reduction was defined in an action-based setting, whereas ample set reduction is often defined in a state-based setting. We therefore redefine confluence reduction in the state-based setting of Markov decision processes, and provide a nontrivial proof of its correctness. Additionally, we pinpoint precisely in what way confluence reduction is more general, and provide conditions under which the two notions 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 discuss 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 to ample sets.",
keywords = "EC Grant Agreement nr.: FP7/2007-2013, EC Grant Agreement nr.: FP7/214755, EWI-24771, Partial order reduction, IR-91462, Confluence reduction, Markov Decision Processes, Ample sets, METIS-305895, Probabilistic branching time",
author = "Henri Hansen and M. Massink and G. Norman and Mark Timmer and H. Wiklicky",
note = "eemcs-eprint-24771. Quantitative Aspects of Programming Languages and Systems (2011-12)",
year = "2014",
month = "6",
day = "12",
doi = "10.1016/j.tcs.2013.07.014",
language = "Undefined",
volume = "538",
pages = "103--123",
journal = "Theoretical computer science",
issn = "0304-3975",
publisher = "Elsevier",

}

A comparison of confluence and ample sets in probabilistic and non-probabilistic branching time. / Hansen, Henri; Massink, M. (Editor); Norman, G. (Editor); Timmer, Mark; Wiklicky, H. (Editor).

In: Theoretical computer science, Vol. 538, 12.06.2014, p. 103-123.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - A comparison of confluence and ample sets in probabilistic and non-probabilistic branching time

AU - Hansen, Henri

AU - Timmer, Mark

A2 - Massink, M.

A2 - Norman, G.

A2 - Wiklicky, H.

N1 - eemcs-eprint-24771. Quantitative Aspects of Programming Languages and Systems (2011-12)

PY - 2014/6/12

Y1 - 2014/6/12

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 paper provides an extensive comparison between these two methods, and answers the question how they relate in terms of reduction power when preserving branching time properties. We prove that, while both preserve the same 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. The main challenge for the comparison is that confluence reduction was defined in an action-based setting, whereas ample set reduction is often defined in a state-based setting. We therefore redefine confluence reduction in the state-based setting of Markov decision processes, and provide a nontrivial proof of its correctness. Additionally, we pinpoint precisely in what way confluence reduction is more general, and provide conditions under which the two notions 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 discuss 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 to ample sets.

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 paper provides an extensive comparison between these two methods, and answers the question how they relate in terms of reduction power when preserving branching time properties. We prove that, while both preserve the same 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. The main challenge for the comparison is that confluence reduction was defined in an action-based setting, whereas ample set reduction is often defined in a state-based setting. We therefore redefine confluence reduction in the state-based setting of Markov decision processes, and provide a nontrivial proof of its correctness. Additionally, we pinpoint precisely in what way confluence reduction is more general, and provide conditions under which the two notions 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 discuss 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 to ample sets.

KW - EC Grant Agreement nr.: FP7/2007-2013

KW - EC Grant Agreement nr.: FP7/214755

KW - EWI-24771

KW - Partial order reduction

KW - IR-91462

KW - Confluence reduction

KW - Markov Decision Processes

KW - Ample sets

KW - METIS-305895

KW - Probabilistic branching time

U2 - 10.1016/j.tcs.2013.07.014

DO - 10.1016/j.tcs.2013.07.014

M3 - Article

VL - 538

SP - 103

EP - 123

JO - Theoretical computer science

JF - Theoretical computer science

SN - 0304-3975

ER -