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.

pdf

BibTeX:

@inproceedings{HoelzlN-TACAS12,
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},
publisher={Springer},series={LNCS},volume={7214},pages={347-361},year=2012}
Isabelle theories in the Archive of Formal Proofs