Verifying pCTL Model Checking

Johannes Hölzl Tobias Nipkow

Probabilistic model checkers like PRISM check the satisfiability of probabilistic CTL (pCTL) formulas against discrete-time Markov chains. We prove soundness and completeness of their underlying algorithm in Isabelle/HOL. We define Markov chains given by a transition matrix and formalize the corresponding probability measure on sets of paths. The formalization of pCTL formulas includes unbounded cumulated rewards.



author={Johannes Hölzl and Tobias Nipkow},
title={Verifying pCTL Model Checking},
booktitle={Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012)},
editor={Flanagan and König},
Isabelle theories in the Archive of Formal Proofs