Lightweight Statistical Model Checking in Nondeterministic Continuous Time
| Title | Lightweight Statistical Model Checking in Nondeterministic Continuous Time |
| Publication Type | Book Chapter |
| Year of Publication | 2018 |
| Authors | D'Argenio, PR, Hartmanns, A, Sedwards, S |
| Editor | Margaria, T, Steffen, B |
| Book Title | Leveraging Applications of Formal Methods, Verification and Validation. Verification - 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part II |
| Series Title | Lecture Notes in Computer Science |
| Volume | 11245 |
| Pagination | 336–353 |
| Publisher | Springer |
| 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. |
| URL | https://doi.org/10.1007/978-3-030-03421-4_22 |
| DOI | 10.1007/978-3-030-03421-4_22 |
PDF (Full text):
