Verifying pCTL model checking

DOI10.1007/978-3-642-28756-5_24MaRDI QIDQ2894281zbMATH OpenOpenAlexFDO

Authors Johannes Hölzl, Tobias Nipkow

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

Temporal logic (03B44) 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) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Recommendations

• Probabilistic model checking: Formalisms and algorithms for discrete and real-time systems
• Model checking probabilistic systems
• Symbolic model checking for probabilistic processes
• Probabilistic symbolic model checking with PRISM: A hybrid approach
• Model checking of probabilistic and nondeterministic systems

Cited in

(6)

• Partitioned PLTL model-checking for refined transition systems
• Markov chains and Markov decision processes in Isabelle/HOL
• Formalizing probabilistic noninterference
• Markov Models
• Evaluating probabilistic model checking tools for verification of robot control policies
• Bounded satisfiability for PCTL

Describes a project that uses

Uses Software

• PRISM
• Isabelle/HOL

This page was built for publication: Verifying pCTL model checking

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2894281)