Probabilistic CSP: Preserving the laws via restricted schedulers

S. Georgievska, S. Andova

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    4 Citations (Scopus)
    2 Downloads (Pure)

    Abstract

    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.
    Original languageEnglish
    Title of host publicationMeasurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance (16th International GI/ITG Conference, MMB & DFT 2012, Kaiserslautern, Germany, March 19-21, 2012. Proceedings)
    EditorsJ.B. Schmitt
    Place of PublicationBerlin
    PublisherSpringer
    Pages136-150
    ISBN (Print)978-3-642-28539-4
    DOIs
    Publication statusPublished - 2012

    Publication series

    NameLecture Notes in Computer Science
    Volume7201
    ISSN (Print)0302-9743

    Fingerprint

    Dive into the research topics of 'Probabilistic CSP: Preserving the laws via restricted schedulers'. Together they form a unique fingerprint.

    Cite this