On Generative Parallel Composition

D'Argenio, P.R. and Hermanns, H. and Katoen, J.P. (1999) On Generative Parallel Composition. In: First International Workshop on Probabilistic Methods in Verification, PROBMIV '98, 19-20 June 1998, Indianapolis, Indiana.

Preview

PDF
1541Kb

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.
Item Type:	Conference or Workshop Item
Copyright:	© 1999 Elsevier
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Formal Methods and Tools (FMT)
Link to this item:	http://purl.utwente.nl/publications/66255
Official URL:	http://dx.doi.org/10.1016/S1571-0661(05)80596-1
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page

Metis ID: 119152