Verifying pCTL Model Checking

DOI10.1007/978-3-642-28756-5_24zbMath1352.68154OpenAlexW134281090MaRDI QIDQ2894281

Tobias Nipkow, Johannes Hölzl

Publication date: 29 June 2012

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-28756-5_24

Mathematics Subject Classification ID

Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.) (60J20) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (2)

Formalizing Probabilistic Noninterference ⋮ Markov chains and Markov decision processes in Isabelle/HOL

Uses Software

• PRISM
• Isabelle/HOL

This page was built for publication: Verifying pCTL Model Checking