A Hierarchy of Scheduler Classes for Stochastic Automata

Pedro R. D'Argenio, Marcus Gerhold, Arnd Hartmanns, Sean Sedwards

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

    4 Citations (Scopus)
    54 Downloads (Pure)

    Abstract

    Stochastic automata are a formal compositional model for concurrent stochastic timed systems, with general distributions and nondeterministic choices. Measures of interest are defined over schedulers that resolve the nondeterminism. In this paper we investigate the power of various theoretically and practically motivated classes of schedulers, considering the classic complete-information view and a restriction to non-prophetic schedulers. We prove a hierarchy of scheduler classes w.r.t. unbounded probabilistic reachability. We find that, unlike Markovian formalisms, stochastic automata distinguish most classes even in this basic setting. Verification and strategy synthesis methods thus face a tradeoff between powerful and efficient classes. Using lightweight scheduler sampling, we explore this tradeoff and demonstrate the concept of a useful approximative verification technique for stochastic automata.
    Original languageEnglish
    Title of host publicationProceedings of the 21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2018)
    EditorsChristel Baier, Ugo Dal Lago
    Place of PublicationCham
    PublisherSpringer
    Pages384-402
    Number of pages19
    ISBN (Electronic)978-3-319-89366-2
    ISBN (Print)978-0-319-89365-5
    DOIs
    Publication statusPublished - 1 Jan 2018

    Publication series

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

    Fingerprint Dive into the research topics of 'A Hierarchy of Scheduler Classes for Stochastic Automata'. Together they form a unique fingerprint.

  • Cite this

    D'Argenio, P. R., Gerhold, M., Hartmanns, A., & Sedwards, S. (2018). A Hierarchy of Scheduler Classes for Stochastic Automata. In C. Baier, & U. Dal Lago (Eds.), Proceedings of the 21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2018) (pp. 384-402). (Lecture Notes in Computer Science; Vol. 10803). Cham: Springer. https://doi.org/10.1007/978-3-319-89366-2_21