PRISM-TUMheuristics

PRISM-TUMheuristics is a heuristics based model checker for DTMC, CTMC, and MDP with reachability / LTL objectives.

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.

Download and Installation

The tool can be obtained from the Git Repository. To build, follow the instructions in the README.md.

Contact

For general feedback, comments and questions contact Jan, Tobias, Pranav, or Maxi.

Future Work

We’re planning to support JANI as input format. Further, the approach can be extended to handle full LTL and cost bounded properties.