TY - GEN
T1 - Schedulers are no Prophets
AU - Hartmanns, Arnd
AU - Hermanns, H.
AU - Krčál, Jan
N1 - eemcs-eprint-27014Colli
PY - 2016/1
Y1 - 2016/1
N2 - Several formalisms for concurrent computation have been proposed in recent years that incorporate means to express stochastic continuous-time dynamics and non-determinism. In this setting, some obscure phenomena are known to exist, related to the fact that schedulers may yield too pessimistic verification results, since current non-determinism can surprisingly be resolved based on prophesying the timing of future random events. This paper provides a thorough investigation of the problem, and it presents a solution: Based on a novel semantics of stochastic automata, we identify the class of schedulers strictly unable to prophesy, and show a path towards verification algorithms with respect to that class. The latter uses an encoding into the model of stochastic timed automata under arbitrary schedulers, for which model checking tool support has recently become available.
AB - Several formalisms for concurrent computation have been proposed in recent years that incorporate means to express stochastic continuous-time dynamics and non-determinism. In this setting, some obscure phenomena are known to exist, related to the fact that schedulers may yield too pessimistic verification results, since current non-determinism can surprisingly be resolved based on prophesying the timing of future random events. This paper provides a thorough investigation of the problem, and it presents a solution: Based on a novel semantics of stochastic automata, we identify the class of schedulers strictly unable to prophesy, and show a path towards verification algorithms with respect to that class. The latter uses an encoding into the model of stochastic timed automata under arbitrary schedulers, for which model checking tool support has recently become available.
KW - EWI-27014
KW - EC Grant Agreement nr.: FP7/295261
KW - IR-100653
KW - METIS-317202
KW - EC Grant Agreement nr.: FP7/318490
U2 - 10.1007/978-3-319-27810-0_11
DO - 10.1007/978-3-319-27810-0_11
M3 - Conference contribution
SN - 978-3-319-27809-4
T3 - Lecture Notes in Computer Science
SP - 214
EP - 235
BT - Semantics, Logics, and Calculi: Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays
PB - Springer
CY - Cham
T2 - Semantics, Logics, and Calculi: Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays
Y2 - 8 January 2016 through 8 January 2016
ER -