Verifying Reachability Properties in Markov Chains via Incremental Induction

Elizabeth Polgreen, Martin Brain, Martin Fraenzle +1

There is a scalability gap between probabilistic and non-probabilistic verification. Probabilistic model checking tools are based either on explicit engines or on (Multi-Terminal)…