2026-06-27T15:15:31Zhttps://docta.ucm.es/rest/oai/request

oai:docta.ucm.es:20.500.14352/606602024-07-10T15:44:03Zcom_20.500.14352_14col_20.500.14352_21

Cuartero Gómez, Fernando Frutos Escrig, David De Valero Ruiz, Valentín 2023-06-20T21:05:24Z 2023-06-20T21:05:24Z 1997 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. 978-3-540-63010-4 10.1007/3-540-63010-4_23 https://hdl.handle.net/20.500.14352/60660 https//doi.org/10.1007/3-540-63010-4_23 http://link.springer.com/content/pdf/10.1007%2F3-540-63010-4_23 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. eng open access A sound and complete proof system for probabilistic processes book part