A linear process-algebraic format with data for probabilistic automata

    Research output: Contribution to journalArticleAcademicpeer-review

    9 Citations (Scopus)
    206 Downloads (Pure)


    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.
    Original languageUndefined
    Pages (from-to)36-57
    Number of pages22
    JournalTheoretical computer science
    Issue number1
    Publication statusPublished - 6 Jan 2012


    • EWI-20452
    • Linearisation
    • Probabilistic process algebra
    • State space reduction
    • Data-dependent probabilistic choice
    • EC Grant Agreement nr.: FP7-ICT-2007-1
    • EC Grant Agreement nr.: FP7/214755
    • METIS-278768
    • IR-77938
    • Symbolic transformations

    Cite this