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 contribution

  • 1 Citations

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.
LanguageEnglish
Title of host publicationFoundations of Software Science and Computation Structures
Subtitle of host publication21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings
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
StatePublished - 2018

Publication series

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

Fingerprint

Scheduler
Automata
Trade-offs
Nondeterminism
Reachability
Concurrent
Resolve
Class
Hierarchy
Synthesis
Restriction
Demonstrate

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.), Foundations of Software Science and Computation Structures: 21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings (pp. 384-402). (Lecture Notes in Computer Science; Vol. 10803). Cham: Springer. DOI: 10.1007/978-3-319-89366-2_21
D'Argenio, Pedro R. ; Gerhold, Marcus ; Hartmanns, Arnd ; Sedwards, Sean. / A Hierarchy of Scheduler Classes for Stochastic Automata. Foundations of Software Science and Computation Structures: 21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings. editor / Christel Baier ; Ugo Dal Lago. Cham : Springer, 2018. pp. 384-402 (Lecture Notes in Computer Science).
@inproceedings{974761194a6d475a9dedae6a26750160,
title = "A Hierarchy of Scheduler Classes for Stochastic Automata",
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.",
author = "D'Argenio, {Pedro R.} and Marcus Gerhold and Arnd Hartmanns and Sean Sedwards",
note = "Open Access",
year = "2018",
doi = "10.1007/978-3-319-89366-2_21",
language = "English",
isbn = "978-0-319-89365-5",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "384--402",
editor = "Christel Baier and {Dal Lago}, Ugo",
booktitle = "Foundations of Software Science and Computation Structures",

}

D'Argenio, PR, Gerhold, M, Hartmanns, A & Sedwards, S 2018, A Hierarchy of Scheduler Classes for Stochastic Automata. in C Baier & U Dal Lago (eds), Foundations of Software Science and Computation Structures: 21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10803, Springer, Cham, pp. 384-402. DOI: 10.1007/978-3-319-89366-2_21

A Hierarchy of Scheduler Classes for Stochastic Automata. / D'Argenio, Pedro R.; Gerhold, Marcus; Hartmanns, Arnd; Sedwards, Sean.

Foundations of Software Science and Computation Structures: 21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings. ed. / Christel Baier; Ugo Dal Lago. Cham : Springer, 2018. p. 384-402 (Lecture Notes in Computer Science; Vol. 10803).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - A Hierarchy of Scheduler Classes for Stochastic Automata

AU - D'Argenio,Pedro R.

AU - Gerhold,Marcus

AU - Hartmanns,Arnd

AU - Sedwards,Sean

N1 - Open Access

PY - 2018

Y1 - 2018

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-89366-2_21

DO - 10.1007/978-3-319-89366-2_21

M3 - Conference contribution

SN - 978-0-319-89365-5

T3 - Lecture Notes in Computer Science

SP - 384

EP - 402

BT - Foundations of Software Science and Computation Structures

PB - Springer

CY - Cham

ER -

D'Argenio PR, Gerhold M, Hartmanns A, Sedwards S. A Hierarchy of Scheduler Classes for Stochastic Automata. In Baier C, Dal Lago U, editors, Foundations of Software Science and Computation Structures: 21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings. Cham: Springer. 2018. p. 384-402. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-319-89366-2_21