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 n 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
DS Docta Complutense
RD 2 may 2024