A linear process-algebraic format with data for probabilistic automata (Q764285)

A novel linear process-algebraic format for probabilistic automata is presented. The key ingredient is a symbolic transformation of probabilistic process algebra terms (terms of prCRL which is restricted \(\mu \text{CRL}\) with a probabilistic choice operator) that incorporate data into this linear format while preserving strong probabilistic bisimulation. This generalizes similar techniques for traditional process algebras with data, and treats data and data-dependent probabilistic choice in a fully symbolic manner, leading to the symbolic analysis of parameterized probabilistic systems. Several reduction techniques that can be easily applied to the presented models are discussed. A validation of the presented approach is presented on a benchmark case study, namely leader election protocols. It shows significant reductions of states, transitions as well as running time.