Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1007/978-3-642-28756-5_24 | TACAS |
Keywords | Field | DocType |
pctl model checking,corresponding probability measure,probabilistic ctl,pctl formula,cumulated reward,probabilistic model checker,markov chain,underlying algorithm,transition matrix,discrete-time markov chain | HOL,Discrete mathematics,Model checking,Stochastic matrix,Computer science,Markov chain,Probability measure,Probabilistic CTL,Theoretical computer science,Soundness,Completeness (statistics) | Conference |
Volume | ISSN | Citations |
7214 | 0302-9743 | 2 |
PageRank | References | Authors |
0.39 | 15 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Johannes Hölzl | 1 | 116 | 13.23 |
| Tobias Nipkow | 2 | 3056 | 232.28 |