ePMC, the Extendible Probabilistic Model Checker, is now available publicly. It can be accessed online on GitHub, at this repository.
ePMC is the successor of IscasMC, from which it keeps all features about Linear Time Logic probabilistic model checking. ePMC is highly modular, which allows everyone to extend and improve the functionalities of the model checker.
We are hosting the IscasMC summer school on the Practical Aspects on Probabilistic Model Checking, where we survey the main aspects relative to probabilistic model checking, with a specific attention to the practical aspects, in particular relative to the implementation of IscasMC.
See the official page for more details.
When you cite our IscasMC model checker, please use [HahnLSTZ14].
Feel free to contact us by email if you find issues with the online model checker.
The ISCAS model checker goes live today. It supports now
- Markov chains, wrt. logic PCTL*
- Markov decision processes, wrt. logic PCTL*
- Quantum Markov chains, wrt. logic QCTL