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

2 Citations (Scopus)
40 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

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.), 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
D'Argenio, Pedro R. ; Gerhold, Marcus ; Hartmanns, Arnd ; Sedwards, Sean. / A Hierarchy of Scheduler Classes for Stochastic Automata. Proceedings of the 21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2018). 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",
month = "1",
day = "1",
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 = "Proceedings of the 21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2018)",

}

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), Proceedings of the 21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2018). Lecture Notes in Computer Science, vol. 10803, Springer, Cham, pp. 384-402. https://doi.org/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.

Proceedings of the 21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2018). 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 contributionAcademicpeer-review

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/1/1

Y1 - 2018/1/1

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.

UR - http://www.scopus.com/inward/record.url?scp=85045647980&partnerID=8YFLogxK

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 - Proceedings of the 21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2018)

A2 - Baier, Christel

A2 - Dal Lago, Ugo

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, Proceedings of the 21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2018). Cham: Springer. 2018. p. 384-402. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-319-89366-2_21