Cuartero Gómez, FernandoFrutos Escrig, David DeValero Ruiz, ValentínBertran, MiquelRus, Teodor2023-06-202023-06-201997Cuartero 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.978-3-540-63010-410.1007/3-540-63010-4_23https://hdl.handle.net/20.500.14352/60660In 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.engbook parthttps//doi.org/10.1007/3-540-63010-4_23http://link.springer.com/content/pdf/10.1007%2F3-540-63010-4_23open access004Informática (Informática)1203.17 Informática