RT Book, Section
T1 A sound and complete proof system for probabilistic processes
A1 Cuartero Gómez, Fernando
A1 Frutos Escrig, David De
A1 Valero Ruiz, Valentín
A2 Bertran, Miquel
A2 Rus, Teodor
AB In this paper we present a process algebra model of probabilistic communicating processes based on classical CSP. To define our model we have replaced internal non-determinism by generative probabilistic choices, and external non-determinism by reactive probabilistic choices, with the purpose of maintaining the meaning of the classical CSP operators, once generalized in a probabilistic way. Thus we try to keep valid, as far as possible, the laws of CSP. This combination of both internal and external choice makes strongly difficult the definition of a probabilistic version of CSP. In fact, we can find in the current literature quite a number of papers on probabilistic processes, but only in a few of them internal and external choices are combined, trying to preserve their original meaning.Starting with a denotational semantics where the corresponding domain is a set of probabilistic trees with two kinds of nodes, representing the internal and external choices, we define a sound and complete proof system, with very similar laws to those of the corresponding CSP.
PB Springer
SN 978-3-540-63010-4
YR 1997
FD 1997
LK https://hdl.handle.net/20.500.14352/60660
UL https://hdl.handle.net/20.500.14352/60660
LA eng
NO Cuartero Gómez, F., Frutos Escrig, D. & Valero Ruiz, V. «A sound and complete proof system for probabilistic processes». Transformation-Based Reactive Systems Development, editado por Miquel Bertran y Teodor Rus, vol. 1231, Springer Berlin Heidelberg, 1997, pp. 340-52. DOI.org (Crossref), https://doi.org/10.1007/3-540-63010-4_23.
DS Docta Complutense
RD 3 jul 2025