Counterexamples for Discrete Time Markov Models

by Jens Katelaan for PRISM Model Checker

This project will add support for counterexample generation for Discrete Time Markov Chains and Markov Decision Processes to PRISM. That is, during the course of the project, several algorithms will be implemented in PRISM that, given a probabilistic reachability property and a DTMC or an MDP that violates said property, generate a counterexample explaining to the user why the model does not satisfy the property.