This paper presents a novel linear process-algebraic format for probabilistic automata. The key ingredient is a symbolic transformation of probabilistic process algebra terms that incorporate data into this linear format while preserving strong probabilistic bisimulation. This generalises similar techniques for traditional process algebras with data, and - more importantly - treats data and data-dependent probabilistic choice in a fully symbolic manner, leading to the symbolic analysis of parameterised probabilistic systems. We discuss several reduction techniques that can easily be applied to our models. A validation of our approach on two benchmark leader election protocols shows reductions of more than an order of magnitude.
- Probabilistic process algebra
- State space reduction
- Data-dependent probabilistic choice
- EC Grant Agreement nr.: FP7-ICT-2007-1
- EC Grant Agreement nr.: FP7/214755
- Symbolic transformations