Probabilistic Extensions of Process Algebras

Bengt Jonsson, Wang Yi, Kim G. Larsen

Research output: Chapter in Book/Report/Conference proceedingChapterAcademic

17 Citations (Scopus)


In this chapter, we adopt Probabilistic Transition Systems as a basic model for probabilistic processes, in which probabilistic and nondeterministic choices are independent concepts. The model is essentially a nondeterministic version of Markov decision processes or probabilistic automata of Rabin. We develop a general framework to define probabilistic process languages to describe probabilistic transition systems. In particular, we show how operators for nonprobabilistic process algebras can be lifted to probabilistic process algebras in a uniform way similar to de Simone format. To establish a notion of refinement, we present a family of preorders including probabilistic bisimulation and simulation, and probabilistic testing pre-orders as well as their logical or denotational characterization. These preorders are shown to be precongruences with respect to the algebraic operators that can be defined in our general framework. Finally, we give a short account of the important work on extending the successful field of model checking to probabilistic settings and a brief discussion on current research in the area.
Original languageEnglish
Title of host publicationHandbook of Process Algebra
EditorsJ.A. Bergstra, A. Ponse, S.A. Smolka
ISBN (Print)978-0-444-82830-9
Publication statusPublished - 2001
Externally publishedYes


Dive into the research topics of 'Probabilistic Extensions of Process Algebras'. Together they form a unique fingerprint.

Cite this