PRISM-TUMheuristics is an explicit model checker for DTMC, CTMC, and MDP, based on PRISM 4.4. At its heart, the tool uses the ideas of [BCC+’14] to only explore relevant parts of the state space and focus computation on important sections. Intuitively, states which are hardly reachable can be omitted if only an approximative solution is needed. Depending on the structure of the model, this approach can yield arbitrary speedups. The tool supports (unbounded) reachabilty for CTMC (via embedding), and simple LTL (reachability, safety, and propositional until) for DTMC and MDP.
The tool can be obtained from the Git Repository. To build, follow the instructions in the README.md.
For general feedback, comments and questions contact Jan, Tobias, Pranav, or Maxi.
We’re planning to support JANI as input format. Further, the approach can be extended to handle full LTL and cost bounded properties.