A comparison of confluence and ample sets in probabilistic and non-probabilistic branching time
| Autor: | Hansen, Henri, Massink, M., Norman, G., Timmer, Mark, Wiklicky, H. |
|---|---|
| Rok vydání: | 2014 |
| Předmět: |
Correctness
Theoretical computer science General Computer Science EWI-24771 Ample sets Context (language use) 0102 computer and information sciences 02 engineering and technology Confluence reduction 01 natural sciences Theoretical Computer Science Reduction (complexity) EC Grant Agreement nr.: FP7/214755 Converse 0202 electrical engineering electronic engineering information engineering EC Grant Agreement nr.: FP7/2007-2013 IR-91462 Mathematics Probabilistic logic Partial order reduction METIS-305895 010201 computation theory & mathematics Confluence Markov Decision Processes Probabilistic branching time 020201 artificial intelligence & image processing Markov decision process Algorithm |
| Zdroj: | Theoretical computer science, 538, 103-123. Elsevier |
| ISSN: | 0304-3975 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect