iscasMc: A web-based probabilistic model checker. We introduce the web-based model checker iscasMc for probabilistic systems (see ). This Java application offers an easy-to-use web interface for the evaluation of Markov chains and decision processes against PCTL and PCTL* specifications. Compared to PRISM or MRMC, iscasMc is particularly efficient in evaluating the probabilities of LTL properties.