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 |
Place of Publication | Cham |
Publisher | Springer |
Pages | 336-353 |
Number of pages | 18 |
ISBN (Electronic) | 978-3-030-03421-4 |
ISBN (Print) | 978-3-030-03420-7 |
DOIs | |
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 |
Keywords
- 2025 OA procedure
Fingerprint
Dive into the research topics of 'Lightweight Statistical Model Checking in Nondeterministic Continuous Time'. Together they form a unique fingerprint.Datasets
-
Lightweight Statistical Model Checking in Nondeterministic Continuous Time (Artifact)
Hartmanns, A. (Creator), d' Argenio, P. R. (Contributor) & Sedwards, S. (Contributor), 4TU.Centre for Research Data, 25 Sept 2018
DOI: 10.4121/uuid:1453a13b-10ae-418f-a1ae-4acf96028118
Dataset