Schedulers are no Prophets

Arnd Hartmanns, H. Hermanns, Jan Krčál

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

    2 Citations (Scopus)
    82 Downloads (Pure)

    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 languageEnglish
    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 PublicationCham
    PublisherSpringer
    Pages214-235
    Number of pages22
    ISBN (Print)978-3-319-27809-4
    DOIs
    Publication statusPublished - 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). Cham: Springer. https://doi.org/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. Cham : Springer, 2016. pp. 214-235 (Lecture Notes in Computer Science).
    @inproceedings{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č{\'a}l",
    note = "eemcs-eprint-27014Colli",
    year = "2016",
    month = "1",
    doi = "10.1007/978-3-319-27810-0_11",
    language = "English",
    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, Cham, pp. 214-235. https://doi.org/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. Cham : Springer, 2016. p. 214-235 (Lecture Notes in Computer Science; Vol. 9560).

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

    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

    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. Cham: Springer. 2016. p. 214-235. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-319-27810-0_11