Lightweight Statistical Model Checking in Nondeterministic Continuous Time (Artifact)

Datacite citation style:
Hartmanns, Arnd (2018): Lightweight Statistical Model Checking in Nondeterministic Continuous Time (Artifact). Version 1. 4TU.ResearchData. dataset. https://doi.org/10.4121/uuid:1453a13b-10ae-418f-a1ae-4acf96028118
Other citation styles (APA, Harvard, MLA, Vancouver, Chicago, IEEE) available at Datacite

Dataset

University of Twente logo

Usage statistics

1321
views
238
downloads

Licence

4TU General Terms of Use
See License.txt files in the data.
In our ISoLA 2018 paper titled "Lightweight Statistical Model Checking in Nondeterministic Continuous Time", 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. Making use of our implementations of lightweight scheduler sampling in the 'modes' statistical model checker within the Modest Toolset, we present extended experiments and new visualisations of the distribution of schedulers. This artifact contains (1) the version of 'modes' and (2) the model files used for our experiments, (3) the raw experimental results, (4) summarising tabular views of those results (from which we derived the tables of results and histograms shown in the paper), and (5) the Linux shell scripts that we used to perform the experiments.

History

  • 2018-09-25 first online, published, posted

Publisher

University of Twente

Format

media types: application/octet-stream, application/vnd.openxmlformats-officedocument.spreadsheetml.sheet, application/x-dosexec, application/zip, text/plain

Organizations

University of Twente, Faculty of Electrical Engineering, Mathematics and Computer Science, Formal Methods and Tools (FMT) research group

Contributors

  • D'Argenio, P.R. (Pedro)
  • Sedwards, S. (Sean) orcid logo

DATA

Files (1)

  • 50,039,629 bytesMD5:53b44f6f9b6089e6e045f206aa70c8c8data.zip