Interactive verification of Markov chains: Two distributed protocol case studies

Johannes Hölzl, Tobias Nipkow

Probabilistic model checkers like PRISM only check probabilistic systems of a fixed size. To guarantee the desired properties for an arbitrary size, mathematical analysis is necess…