A linear process-algebraic format with data for probabilistic automata

  • 7 Citations

Abstract

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
Volume413
Issue number1
DOIs
StatePublished - 6 Jan 2012

Fingerprint

Algebra

Keywords

  • 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

Di Pierro, A. (Editor); Katoen, Joost P.; van de Pol, Jan Cornelis; Norman, G. (Editor); Stoelinga, Mariëlle Ida Antoinette; Timmer, Mark / A linear process-algebraic format with data for probabilistic automata.

In: Theoretical computer science, Vol. 413, No. 1, 06.01.2012, p. 36-57.

Research output: Scientific - peer-reviewArticle

@article{a07d79e6a04c42eeaf8293ab26c4e826,
title = "A linear process-algebraic format with data for probabilistic automata",
abstract = "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.",
keywords = "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",
author = "{Di Pierro}, A. and Katoen, {Joost P.} and {van de Pol}, {Jan Cornelis} and G. Norman and Stoelinga, {Mariëlle Ida Antoinette} and Mark Timmer",
note = "eemcs-eprint-20452",
year = "2012",
month = "1",
doi = "10.1016/j.tcs.2011.07.021",
volume = "413",
pages = "36--57",
journal = "Theoretical computer science",
issn = "0304-3975",
publisher = "Elsevier",
number = "1",

}

A linear process-algebraic format with data for probabilistic automata. / Di Pierro, A. (Editor); Katoen, Joost P.; van de Pol, Jan Cornelis; Norman, G. (Editor); Stoelinga, Mariëlle Ida Antoinette; Timmer, Mark.

In: Theoretical computer science, Vol. 413, No. 1, 06.01.2012, p. 36-57.

Research output: Scientific - peer-reviewArticle

TY - JOUR

T1 - A linear process-algebraic format with data for probabilistic automata

AU - Katoen,Joost P.

AU - van de Pol,Jan Cornelis

AU - Stoelinga,Mariëlle Ida Antoinette

AU - Timmer,Mark

A2 - Di Pierro,A.

A2 - Norman,G.

N1 - eemcs-eprint-20452

PY - 2012/1/6

Y1 - 2012/1/6

N2 - 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.

AB - 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.

KW - EWI-20452

KW - Linearisation

KW - Probabilistic process algebra

KW - State space reduction

KW - Data-dependent probabilistic choice

KW - EC Grant Agreement nr.: FP7-ICT-2007-1

KW - EC Grant Agreement nr.: FP7/214755

KW - METIS-278768

KW - IR-77938

KW - Symbolic transformations

U2 - 10.1016/j.tcs.2011.07.021

DO - 10.1016/j.tcs.2011.07.021

M3 - Article

VL - 413

SP - 36

EP - 57

JO - Theoretical computer science

T2 - Theoretical computer science

JF - Theoretical computer science

SN - 0304-3975

IS - 1

ER -