DatasetA Modest Approach to Modelling and Checking Markov Automata (Artifact)
►►►►► Link as https://doi.org/10.4121/uuid:98d571be-cdd4-4e5a-a589-7c5b1320e569 | How to cite this dataset
| ?title | A Modest Approach to Modelling and Checking Markov Automata (Artifact) |
| ?creator |  Butkova, Y. (Yuliya) |
| ?contributor | Hartmanns, A. (Arnd) |
| ?contributor | Hermanns, H. (Holger) |
| ?contributor | University of Twente, Faculty of Electrical Engineering, Mathematics and Computer Science, Formal Methods and Tools (FMT) research |
| ?date accepted | 2019-09-05 |
| ?date created | 2019-08 |
| ?date published | 2019-09-05 |
| ?description | Markov automata are a compositional modelling formalism with continuous stochastic time, discrete probabilities, and nondeterministic choices. In our QEST 2019 paper titled "A Modest Approach to Modelling and Checking Markov Automata", we present extensions to the Modest language and the 'mcsta' model checker of the Modest Toolset to describe and analyse Markov automata models. The verification of Markov automata models requires dedicated algorithms for time-bounded probabilistic reachability and long-run average rewards. In the paper, we describe several recently developed such algorithms as implemented in 'mcsta' and evaluate them on a comprehensive set of benchmarks. Our evaluation shows that 'mcsta' improves the performance and scalability of Markov automata model checking compared to earlier and alternative tools. This artifact contains (1) the version of 'mcsta' and (2) the model files used for our experiments, (3) the raw experimental results, and (4) Linux scripts to replicate the experiments. |
| ?keyword | Markov processes ◊ Probabilistic verification |
| ?language | en |
| ?publisher | 4TU.Centre for Research Data |
| ? subject | |
| ? subject | |
| ? ▲ in collection | |
| ?related publication |  doi.org/10.1007/978-3-030-30281-8_4 |
| ?licence |  CC-BY [ more info... ]Other licence for specific components (software): see file /modest/License.txt in the data. |
DATA
MD5: d2e82fb246ff2492a3c83c39eedfbcffsize: 1212464150 B (1.13 GiB)
data.zip (application/zip)This file contains files with the following mime types:
- application/octet-stream
- application/x-archive
- application/x-dosexec
- application/x-sharedlib
- application/zip
- text/plain
- text/x-python
