A Hierarchy of Scheduler Classes for Stochastic Automata
| Title | A Hierarchy of Scheduler Classes for Stochastic Automata |
| Publication Type | Book Chapter |
| Year of Publication | 2018 |
| Authors | D'Argenio, PR, Gerhold, M, Hartmanns, A, Sedwards, S |
| Editor | Baier, C, Dal Lago, U |
| Book Title | Foundations of Software Science and Computation Structures - 21st International Conference, FOSSACS 2018, Held as Part of ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings |
| Series Title | Lecture Notes in Computer Science |
| Volume | 10803 |
| Pagination | 384–402 |
| Publisher | Springer |
| 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. |
| URL | https://doi.org/10.1007/978-3-319-89366-2_21 |
| DOI | 10.1007/978-3-319-89366-2_21 |
PDF (Full text):
