moves-rwth/storm: v1.12

Zenodo (CERN European Organization for Nuclear Research)

Abstract

Support for verifying IDTMCs. Extended DRN file format: Use --io:digits option to control precision of floats. Reading from and writing to compressed DRN files (use .drn.gz / .drn.xz file extensions and/or the new --compression option) (requires libarchive). Added @value_type to determine the type of the parsed values. Support for parsing of DRN interval models. Multi-objective model checking: Multi-objective model checking in --soundmode handles approximation errors correctly. Added --multiobjective:approxtradeoff setting to control Pareto curve approximation heuristic. Extended support for multi-objective properties: distinguish between trade-off and lexicographic properties, introduce multilex(..) syntax for Prism-style properties. storm-pars: Added BigStep transformation. Added generalized parameter lifting. Support for not graph-preserving regions and for not well-defined regions. Region verification API uses RefinementOptions. Support build without DD support. Added state-valuation transformer. Preparation for using probability matrix in CTMC bisimulation. Revised check for probabilistic transition matrix. ConstantsComparator no longer depends on global state. New (optional) dependency: libarchive which supports directly reading/writing from an archive. Updated dependencies: carl-storm, Eigen, ExprTk, gmm, googletest, Gurobi, parallel-hashmap, Spot. Bug fixes in returning rate parameters and requiring MultiObjectiveSettings. Developer: modernized CTMC helpers. Developer: general code clean up such as revising includes, assertions and CMake defines. Developer: CI treats compiler warnings as errors.

Authors 28

1. Christian Hensel
2. Tim Quatmann Aachen @moves-rwth

   RWTH Aachen University

   Affiliation as printed

   @moves-rwth

3. Matthias Volk

   Eindhoven University of Technology

   Affiliation as printed

   Eindhoven University of Technology

4. Sebastian Junges

   Radboud University Nijmegen

   Affiliation as printed

   Radboud University

5. J. Berger Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University

6. jipspel
7. Gereon Kremer
8. Alex Bork Aachen @moves-rwth

   RWTH Aachen University

   Affiliation as printed

   @moves-rwth

9. Daniel Basgöze
10. David
11. Hannah
12. Joachim Klein

    Technische Universität Dresden

    Affiliation as printed

    Ex TU Dresden, Germany

13. Timo P. Gros

    German Research Centre for Artificial Intelligence

    Affiliation as printed

    German Research Center for Artificial Intelligence (DFKI)

14. SPranger
15. Tom Janson
16. Johannes Lehmann
17. Jan Karuc
18. looomis
19. Linus
20. Sascha Vincent Kurowski
    Affiliation as printed

    Amazon Europe (@amzn)

21. SvStein
22. Florent Delgrange

    Vrije Universiteit Brussel

    Affiliation as printed

    AI Lab, Vrije Universiteit Brussel

23. Josh Jeppson
    Affiliation as printed

    @fluentverification

24. Arash Partow
    Affiliation as printed

    ἑ

25. Marckvdv
26. spacefrogg
27. Tobias Winkler
28. steffi4321