Making random choices invisible to the scheduler

K. Chatzikokolakis, C. Palamidessi

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

    26 Citations (Scopus)
    100 Downloads (Pure)

    Abstract

    When dealing with process calculi and automata which express both nondeterministic and probabilistic behavior, it is customary to introduce the notion of scheduler to resolve the nondeterminism. It has been observed that for certain applications, notably those in security, the scheduler needs to be restricted so not to reveal the outcome of the protocol’s random choices, or otherwise the model of adversary would be too strong even for "obviously correct" protocols. We propose a process-algebraic framework in which the control on the scheduler can be specified in syntactic terms, and we show how to apply it to solve the problem mentioned above. We also consider the definition of (probabilistic) may and must preorders, and we show that they are precongruences with respect to the restricted schedulers. Furthermore, we show that all the operators of the language, except replication, distribute over probabilistic summation, which is a useful property for verification.
    Original languageEnglish
    Title of host publicationCONCUR 2007 - Concurrency Theory (18th International Conference, Lisbon, Portugal, September 3-8, 2007. Proceedings)
    EditorsL. Caires, V.T. Vasconcelos
    Place of PublicationBerlin
    PublisherSpringer
    Pages42-58
    ISBN (Print)978-3-540-74406-1
    DOIs
    Publication statusPublished - 2007

    Publication series

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

    Fingerprint

    Dive into the research topics of 'Making random choices invisible to the scheduler'. Together they form a unique fingerprint.

    Cite this