Added support for model checking LTL properties in the sparse (and dd-to-sparse) engine. Requires building with Spot or an external LTL to deterministic automaton converter (using option --ltl2datool). Added cmake options STORM_USE_SPOT_SYSTEM and STORM_USE_SPOT_SHIPPED to facilitate building Storm with Spot. Improved parsing of formulas in PRISM-style syntax. Added export of schedulers that use memory (in particular optimizing schedulers for LTL properties) Added support for PRISM models that use unbounded integer variables. Added support for nested arrays in JANI. Added --location-elimination that can be applied to Jani DTMC models to reduce the size of the resulting Markov models, see here. Added an export of check results to json. Use --exportresult in the command line interface. Added --exportbuilt option that exports the built model in various formats. Deprecates --io:exportexplicit, --io:exportdd and --io:exportdot Added export of built model in .json. which can be used to debug and explore the model. Added computation of steady state probabilities for DTMC/CTMC in the sparse engine. Use --steadystate in the command line interface. Added computation of the expected number of times each state in a DTMC/CTMC is visited (sparse engine). Use --expvisittimes in the command line interface. Implemented parsing and model building of Stochastic multiplayer games (SMGs) in the PRISM language. No model checking implemented (yet). API: Simulation of prism-models API: Model-builder takes a callback function to prevent extension of particular actions, prism-to-explicit mapping can be exported API: Export of dice-formatted expressions Prism-language/explicit builder: Allow action names in commands writing to global variables if these (clearly) do not conflict with assignments of synchronizing commands. Prism-language: n-ary predicates are supported (e.g., ExactlyOneOf) Added support for continuous integration with Github Actions. storm-pars: Exploit monotonicity for computing extremal values and parameter space partitioning. storm-dft: Support for analysis of static fault trees via BDDs (Flag --bdd). In particular, efficient computation of multiple time bounds was added and support for several importance measures (Argument --importance). storm-dft: Computation of minimal cut sets for static fault trees (Flag --mcs). storm-dft: Improved modularisation for DFT by exploiting SFT analysis via BDDs. storm-dft: Fixed don't care propagation for shared SPAREs which resulted in wrong results. Developer: Added support for automatic code formatting and corresponding CI workflow.