This paper presents a novel technique for state space reduction of probabilistic specifications, based on a newly developed notion of confluence for probabilistic automata. We prove that this reduction preserves branching probabilistic bisimulation and can be applied on-the-fly. To support the technique, we introduce a method for detecting confluent transitions in the context of a probabilistic process algebra with data, facilitated by an earlier defined linear format.
A case study demonstrates that significant reductions can be obtained.
|Title of host publication||Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011|
|Editors||P.A. Abdulla, K.R.M. Leino|
|Place of Publication||Berlin|
|Number of pages||15|
|Publication status||Published - Mar 2011|
|Name||Lecture Notes in Computer Science|
- Branching probabilistic bisimulation
- EC Grant Agreement nr.: FP7/214755
- State space reduction
- Probabilistic process algebra
- Probabilistic automata