Making Random Choices Invisible to the Scheduler

Konstantinos Chatzikokolakis 1 Catuscia Palamidessi 1
1 COMETE - Concurrency, Mobility and Transactions
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
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.
Type de document :
Communication dans un congrès
Luís Caires and Vasco Thudichum Vasconcelos. CONCUR'07, Sep 2007, Lisboa, Portugal. Springer, 4703, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-74407-8_4〉
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00200967
Contributeur : Catuscia Palamidessi <>
Soumis le : samedi 22 décembre 2007 - 09:56:40
Dernière modification le : jeudi 10 mai 2018 - 02:06:57
Document(s) archivé(s) le : mardi 13 avril 2010 - 15:15:02

Fichier

report.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Konstantinos Chatzikokolakis, Catuscia Palamidessi. Making Random Choices Invisible to the Scheduler. Luís Caires and Vasco Thudichum Vasconcelos. CONCUR'07, Sep 2007, Lisboa, Portugal. Springer, 4703, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-74407-8_4〉. 〈inria-00200967〉

Partager

Métriques

Consultations de la notice

316

Téléchargements de fichiers

69