On Generative Parallel Composition

P.R. d' Argenio, H. Hermanns, Joost P. Katoen

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

34 Citations (Scopus)
31 Downloads (Pure)

Abstract

A major reason for studying probabilistic processes is to establish a link between a formal model for describing functional system behaviour and a stochastic process. Compositionality is an essential ingredient for specifying systems. Parallel composition in a probabilistic setting is complicated since it gives rise to non-determinism, for instance due to interleaving of independent autonomous activities. This paper presents a detailed study of the resolution of non-determinism in an asynchronous generative setting. Based on the intuition behind the synchronous probabilistic calculus PCCS we formulate two criteria that an asynchronous parallel composition should fulfill. We provide novel probabilistic variants of parallel composition for CCS and CSP and show that these operators satisfy these general criteria, opposed to most existing proposals. Probabilistic bisimulation is shown to be a congruence for these operators and their expansion is addressed. We would like to thank the reviewers for their constructive criticism and for pointing out the relation between BPTSs and the model of Pnueli and Zuck. We also thank Ed Brinksma and Rom Langerak (both of the University of Twente) for fruitful discussions.
Original languageEnglish
Title of host publicationPROBMIV'98
Subtitle of host publicationFirst International Workshop on Probabilistic Methods in Verification
EditorsChristel Baier, Michael Huth, Marta Kwiatkowska, Mark Ryan
Place of PublicationAmsterdam
PublisherElsevier
Pages30-54
Number of pages25
DOIs
Publication statusPublished - Jun 1999
Event1st International Workshop on Probabilistic Methods in Verification, PROBMIV 1998 - Indianapolis, United States
Duration: 19 Jun 199820 Jun 1998
Conference number: 1

Publication series

NameElectronic Notes in Theoretical Computer Science
PublisherElsevier
Volume22
ISSN (Print)1571-0661

Workshop

Workshop1st International Workshop on Probabilistic Methods in Verification, PROBMIV 1998
Abbreviated titlePROBMIV
CountryUnited States
CityIndianapolis
Period19/06/9820/06/98

Fingerprint

Chemical analysis
Random processes

Keywords

  • FMT-PM: PROBABILISTIC METHODS
  • FMT-PA: PROCESS ALGEBRAS

Cite this

d' Argenio, P. R., Hermanns, H., & Katoen, J. P. (1999). On Generative Parallel Composition. In C. Baier, M. Huth, M. Kwiatkowska, & M. Ryan (Eds.), PROBMIV'98: First International Workshop on Probabilistic Methods in Verification (pp. 30-54). (Electronic Notes in Theoretical Computer Science; Vol. 22). Amsterdam: Elsevier. https://doi.org/10.1016/S1571-0661(05)80596-1
d' Argenio, P.R. ; Hermanns, H. ; Katoen, Joost P. / On Generative Parallel Composition. PROBMIV'98: First International Workshop on Probabilistic Methods in Verification. editor / Christel Baier ; Michael Huth ; Marta Kwiatkowska ; Mark Ryan. Amsterdam : Elsevier, 1999. pp. 30-54 (Electronic Notes in Theoretical Computer Science).
@inproceedings{81a5e518c76e410eaf46ac87be2967b0,
title = "On Generative Parallel Composition",
abstract = "A major reason for studying probabilistic processes is to establish a link between a formal model for describing functional system behaviour and a stochastic process. Compositionality is an essential ingredient for specifying systems. Parallel composition in a probabilistic setting is complicated since it gives rise to non-determinism, for instance due to interleaving of independent autonomous activities. This paper presents a detailed study of the resolution of non-determinism in an asynchronous generative setting. Based on the intuition behind the synchronous probabilistic calculus PCCS we formulate two criteria that an asynchronous parallel composition should fulfill. We provide novel probabilistic variants of parallel composition for CCS and CSP and show that these operators satisfy these general criteria, opposed to most existing proposals. Probabilistic bisimulation is shown to be a congruence for these operators and their expansion is addressed. We would like to thank the reviewers for their constructive criticism and for pointing out the relation between BPTSs and the model of Pnueli and Zuck. We also thank Ed Brinksma and Rom Langerak (both of the University of Twente) for fruitful discussions.",
keywords = "FMT-PM: PROBABILISTIC METHODS, FMT-PA: PROCESS ALGEBRAS",
author = "{d' Argenio}, P.R. and H. Hermanns and Katoen, {Joost P.}",
year = "1999",
month = "6",
doi = "10.1016/S1571-0661(05)80596-1",
language = "English",
series = "Electronic Notes in Theoretical Computer Science",
publisher = "Elsevier",
pages = "30--54",
editor = "Christel Baier and Michael Huth and Marta Kwiatkowska and Mark Ryan",
booktitle = "PROBMIV'98",

}

d' Argenio, PR, Hermanns, H & Katoen, JP 1999, On Generative Parallel Composition. in C Baier, M Huth, M Kwiatkowska & M Ryan (eds), PROBMIV'98: First International Workshop on Probabilistic Methods in Verification. Electronic Notes in Theoretical Computer Science, vol. 22, Elsevier, Amsterdam, pp. 30-54, 1st International Workshop on Probabilistic Methods in Verification, PROBMIV 1998, Indianapolis, United States, 19/06/98. https://doi.org/10.1016/S1571-0661(05)80596-1

On Generative Parallel Composition. / d' Argenio, P.R.; Hermanns, H.; Katoen, Joost P.

PROBMIV'98: First International Workshop on Probabilistic Methods in Verification. ed. / Christel Baier; Michael Huth; Marta Kwiatkowska; Mark Ryan. Amsterdam : Elsevier, 1999. p. 30-54 (Electronic Notes in Theoretical Computer Science; Vol. 22).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - On Generative Parallel Composition

AU - d' Argenio, P.R.

AU - Hermanns, H.

AU - Katoen, Joost P.

PY - 1999/6

Y1 - 1999/6

N2 - A major reason for studying probabilistic processes is to establish a link between a formal model for describing functional system behaviour and a stochastic process. Compositionality is an essential ingredient for specifying systems. Parallel composition in a probabilistic setting is complicated since it gives rise to non-determinism, for instance due to interleaving of independent autonomous activities. This paper presents a detailed study of the resolution of non-determinism in an asynchronous generative setting. Based on the intuition behind the synchronous probabilistic calculus PCCS we formulate two criteria that an asynchronous parallel composition should fulfill. We provide novel probabilistic variants of parallel composition for CCS and CSP and show that these operators satisfy these general criteria, opposed to most existing proposals. Probabilistic bisimulation is shown to be a congruence for these operators and their expansion is addressed. We would like to thank the reviewers for their constructive criticism and for pointing out the relation between BPTSs and the model of Pnueli and Zuck. We also thank Ed Brinksma and Rom Langerak (both of the University of Twente) for fruitful discussions.

AB - A major reason for studying probabilistic processes is to establish a link between a formal model for describing functional system behaviour and a stochastic process. Compositionality is an essential ingredient for specifying systems. Parallel composition in a probabilistic setting is complicated since it gives rise to non-determinism, for instance due to interleaving of independent autonomous activities. This paper presents a detailed study of the resolution of non-determinism in an asynchronous generative setting. Based on the intuition behind the synchronous probabilistic calculus PCCS we formulate two criteria that an asynchronous parallel composition should fulfill. We provide novel probabilistic variants of parallel composition for CCS and CSP and show that these operators satisfy these general criteria, opposed to most existing proposals. Probabilistic bisimulation is shown to be a congruence for these operators and their expansion is addressed. We would like to thank the reviewers for their constructive criticism and for pointing out the relation between BPTSs and the model of Pnueli and Zuck. We also thank Ed Brinksma and Rom Langerak (both of the University of Twente) for fruitful discussions.

KW - FMT-PM: PROBABILISTIC METHODS

KW - FMT-PA: PROCESS ALGEBRAS

U2 - 10.1016/S1571-0661(05)80596-1

DO - 10.1016/S1571-0661(05)80596-1

M3 - Conference contribution

T3 - Electronic Notes in Theoretical Computer Science

SP - 30

EP - 54

BT - PROBMIV'98

A2 - Baier, Christel

A2 - Huth, Michael

A2 - Kwiatkowska, Marta

A2 - Ryan, Mark

PB - Elsevier

CY - Amsterdam

ER -

d' Argenio PR, Hermanns H, Katoen JP. On Generative Parallel Composition. In Baier C, Huth M, Kwiatkowska M, Ryan M, editors, PROBMIV'98: First International Workshop on Probabilistic Methods in Verification. Amsterdam: Elsevier. 1999. p. 30-54. (Electronic Notes in Theoretical Computer Science). https://doi.org/10.1016/S1571-0661(05)80596-1