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.
|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|
|Number of pages||18|
|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
|Name||Lecture Notes in Computer Science|
|Conference||8th International Symposium, ISoLA 2018|
|Abbreviated title||ISoLA 2018|
|Period||5/11/18 → 9/11/18|
FingerprintDive into the research topics of 'Lightweight Statistical Model Checking in Nondeterministic Continuous Time'. Together they form a unique fingerprint.
Hartmanns, A. (Creator), D'Argenio, P. R. (Contributor) & Sedwards, S. (Contributor), 4TU.Centre for Research Data, 2018