TY - GEN
T1 - Making random choices invisible to the scheduler
AU - Chatzikokolakis, Konstantinos
AU - Palamidessi, Catuscia
PY - 2007/1/1
Y1 - 2007/1/1
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/38149090986
U2 - 10.1007/978-3-540-74407-8_4
DO - 10.1007/978-3-540-74407-8_4
M3 - Conference contribution
AN - SCOPUS:38149090986
SN - 9783540744061
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 42
EP - 58
BT - CONCUR 2007 - Concurrency Theory - 18th International Conference, CONCUR 2007, Proceedings
PB - Springer Verlag
T2 - 18th International Conference on Concurrency Theory, CONCUR 2007
Y2 - 3 September 2007 through 8 September 2007
ER -