Abstract

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.
Original languageUndefined
Title of host publicationSemantics, Logics, and Calculi: Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays
Place of PublicationBerlin
PublisherSpringer
Pages214-235
Number of pages22
ISBN (Print)978-3-319-27809-4
DOIs
StatePublished - Jan 2016

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume9560
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Model checking
Semantics

Keywords

  • EWI-27014
  • EC Grant Agreement nr.: FP7/295261
  • IR-100653
  • METIS-317202
  • EC Grant Agreement nr.: FP7/318490

Cite this

Hartmanns, A., Hermanns, H., & Krčál, J. (2016). Schedulers are no Prophets. In Semantics, Logics, and Calculi: Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays (pp. 214-235). (Lecture Notes in Computer Science; Vol. 9560). Berlin: Springer. DOI: 10.1007/978-3-319-27810-0_11

Hartmanns, Arnd; Hermanns, H.; Krčál, Jan / Schedulers are no Prophets.

Semantics, Logics, and Calculi: Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays. Berlin : Springer, 2016. p. 214-235 (Lecture Notes in Computer Science; Vol. 9560).

Research output: Scientific - peer-reviewConference contribution

@inbook{f46296a2400a41818ddbe62537378ef3,
title = "Schedulers are no Prophets",
abstract = "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.",
keywords = "EWI-27014, EC Grant Agreement nr.: FP7/295261, IR-100653, METIS-317202, EC Grant Agreement nr.: FP7/318490",
author = "Arnd Hartmanns and H. Hermanns and Jan Krčál",
note = "eemcs-eprint-27014Colli",
year = "2016",
month = "1",
doi = "10.1007/978-3-319-27810-0_11",
isbn = "978-3-319-27809-4",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "214--235",
booktitle = "Semantics, Logics, and Calculi: Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays",

}

Hartmanns, A, Hermanns, H & Krčál, J 2016, Schedulers are no Prophets. in Semantics, Logics, and Calculi: Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays. Lecture Notes in Computer Science, vol. 9560, Springer, Berlin, pp. 214-235. DOI: 10.1007/978-3-319-27810-0_11

Schedulers are no Prophets. / Hartmanns, Arnd; Hermanns, H.; Krčál, Jan.

Semantics, Logics, and Calculi: Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays. Berlin : Springer, 2016. p. 214-235 (Lecture Notes in Computer Science; Vol. 9560).

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

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

ER -

Hartmanns A, Hermanns H, Krčál J. Schedulers are no Prophets. In Semantics, Logics, and Calculi: Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays. Berlin: Springer. 2016. p. 214-235. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-319-27810-0_11