2012 | OriginalPaper | Chapter
Probabilistic CSP: Preserving the Laws via Restricted Schedulers
Authors : Sonja Georgievska, Suzana Andova
Published in: Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Extending Communicating Sequential Processes (CSP) by preserving the distributivity laws for internal choice, in the presence of probabilistic choice, has been an open problem so far. The problem stems from a well known disagreement between probabilistic choice and nondeterministic choice, that raises congruence issues for parallel composition. Recently, it has been argued that the congruence issue can be resolved only by restricting the power of the schedulers that resolve the nondeterminism. In our previous work, we have restricted the schedulers by suitably labeling the nondeterministic transitions. We have defined a ready-trace equivalence and a parallel composition with hiding for which the equivalence is a congruence. In this paper, we generalize our model and give a CSP-style axiomatic characterization of the ready-trace equivalence. From the axiomatization it follows that all distributivity axioms for internal choice from CSP are preserved, and no new axioms are added.