Lightweight Statistical Model Checking in Nondeterministic Continuous Time

Pedro R. D'Argenio; Arnd Hartmanns; Sean Sedwards

doi:10.1007/978-3-030-03421-4_22

Lightweight Statistical Model Checking in Nondeterministic Continuous Time

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

12 Citations (Scopus)

Abstract

Lightweight scheduler sampling brings statistical model checking to nondeterministic formalisms with undiscounted properties, in constant memory. Its direct application to continuous-time models is rendered ineffective by their dense concrete state spaces and the need to consider continuous input for optimal decisions. In this paper we describe the challenges and state of the art in applying lightweight scheduler sampling to three continuous-time formalisms: After a review of recent work on exploiting discrete abstractions for probabilistic timed automata, we discuss scheduler sampling for Markov automata and apply it on two case studies. We provide further insights into the tradeoffs between scheduler classes for stochastic automata. Throughout, we present extended experiments and new visualisations of the distribution of schedulers.

Original language	English
Title of host publication	Proceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2018)
Editors	Tiziana Margaria, Bernhard Steffen
Publisher	Springer
Pages	336-353
Number of pages	18
Volume	11245
ISBN (Print)	978-3-030-03420-7
DOIs	https://doi.org/10.1007/978-3-030-03421-4_22
Publication status	Published - 2018
Event	8th International Symposium, ISoLA 2018 - Royal Apollonia Beach Hotel, Limassol, Cyprus Duration: 5 Nov 2018 → 9 Nov 2018 Conference number: 8 http://www.isola-conference.org/isola2018/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	11245
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	8th International Symposium, ISoLA 2018
Abbreviated title	ISoLA 2018
Country/Territory	Cyprus
City	Limassol
Period	5/11/18 → 9/11/18
Internet address	http://www.isola-conference.org/isola2018/

Access to Document

10.1007/978-3-030-03421-4_22

Cite this

D'Argenio, P. R., Hartmanns, A., & Sedwards, S. (2018). Lightweight Statistical Model Checking in Nondeterministic Continuous Time. In T. Margaria, & B. Steffen (Eds.), Proceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2018) (Vol. 11245, pp. 336-353). (Lecture Notes in Computer Science; Vol. 11245). Springer. https://doi.org/10.1007/978-3-030-03421-4_22

D'Argenio, Pedro R. ; Hartmanns, Arnd ; Sedwards, Sean. / Lightweight Statistical Model Checking in Nondeterministic Continuous Time. Proceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2018). editor / Tiziana Margaria ; Bernhard Steffen. Vol. 11245 Springer, 2018. pp. 336-353 (Lecture Notes in Computer Science).

@inproceedings{14767fcb80b344c8bd4982e67d99bd18,

title = "Lightweight Statistical Model Checking in Nondeterministic Continuous Time",

abstract = "Lightweight scheduler sampling brings statistical model checking to nondeterministic formalisms with undiscounted properties, in constant memory. Its direct application to continuous-time models is rendered ineffective by their dense concrete state spaces and the need to consider continuous input for optimal decisions. In this paper we describe the challenges and state of the art in applying lightweight scheduler sampling to three continuous-time formalisms: After a review of recent work on exploiting discrete abstractions for probabilistic timed automata, we discuss scheduler sampling for Markov automata and apply it on two case studies. We provide further insights into the tradeoffs between scheduler classes for stochastic automata. Throughout, we present extended experiments and new visualisations of the distribution of schedulers.",

author = "D'Argenio, {Pedro R.} and Arnd Hartmanns and Sean Sedwards",

year = "2018",

doi = "10.1007/978-3-030-03421-4_22",

language = "English",

isbn = "978-3-030-03420-7",

volume = "11245",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "336--353",

editor = "Tiziana Margaria and Bernhard Steffen",

booktitle = "Proceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2018)",

address = "Netherlands",

note = "8th International Symposium, ISoLA 2018, ISoLA 2018 ; Conference date: 05-11-2018 Through 09-11-2018",

url = "http://www.isola-conference.org/isola2018/",

}

D'Argenio, PR, Hartmanns, A & Sedwards, S 2018, Lightweight Statistical Model Checking in Nondeterministic Continuous Time. in T Margaria & B Steffen (eds), Proceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2018). vol. 11245, Lecture Notes in Computer Science, vol. 11245, Springer, pp. 336-353, 8th International Symposium, ISoLA 2018, Limassol, Cyprus, 5/11/18. https://doi.org/10.1007/978-3-030-03421-4_22

Lightweight Statistical Model Checking in Nondeterministic Continuous Time. / D'Argenio, Pedro R.; Hartmanns, Arnd; Sedwards, Sean.

Proceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2018). ed. / Tiziana Margaria; Bernhard Steffen. Vol. 11245 Springer, 2018. p. 336-353 (Lecture Notes in Computer Science; Vol. 11245).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Lightweight Statistical Model Checking in Nondeterministic Continuous Time

AU - D'Argenio, Pedro R.

AU - Hartmanns, Arnd

AU - Sedwards, Sean

N1 - Conference code: 8

PY - 2018

Y1 - 2018

N2 - Lightweight scheduler sampling brings statistical model checking to nondeterministic formalisms with undiscounted properties, in constant memory. Its direct application to continuous-time models is rendered ineffective by their dense concrete state spaces and the need to consider continuous input for optimal decisions. In this paper we describe the challenges and state of the art in applying lightweight scheduler sampling to three continuous-time formalisms: After a review of recent work on exploiting discrete abstractions for probabilistic timed automata, we discuss scheduler sampling for Markov automata and apply it on two case studies. We provide further insights into the tradeoffs between scheduler classes for stochastic automata. Throughout, we present extended experiments and new visualisations of the distribution of schedulers.

AB - Lightweight scheduler sampling brings statistical model checking to nondeterministic formalisms with undiscounted properties, in constant memory. Its direct application to continuous-time models is rendered ineffective by their dense concrete state spaces and the need to consider continuous input for optimal decisions. In this paper we describe the challenges and state of the art in applying lightweight scheduler sampling to three continuous-time formalisms: After a review of recent work on exploiting discrete abstractions for probabilistic timed automata, we discuss scheduler sampling for Markov automata and apply it on two case studies. We provide further insights into the tradeoffs between scheduler classes for stochastic automata. Throughout, we present extended experiments and new visualisations of the distribution of schedulers.

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

U2 - 10.1007/978-3-030-03421-4_22

DO - 10.1007/978-3-030-03421-4_22

M3 - Conference contribution

SN - 978-3-030-03420-7

VL - 11245

T3 - Lecture Notes in Computer Science

SP - 336

EP - 353

BT - Proceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2018)

A2 - Margaria, Tiziana

A2 - Steffen, Bernhard

PB - Springer

T2 - 8th International Symposium, ISoLA 2018

Y2 - 5 November 2018 through 9 November 2018

ER -

D'Argenio PR, Hartmanns A, Sedwards S. Lightweight Statistical Model Checking in Nondeterministic Continuous Time. In Margaria T, Steffen B, editors, Proceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2018). Vol. 11245. Springer. 2018. p. 336-353. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-030-03421-4_22

Lightweight Statistical Model Checking in Nondeterministic Continuous Time

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint