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

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

Recommendations

• scientific article; zbMATH DE number 1507207
• Model checking probabilistic systems
• Symbolic model checking for probabilistic processes
• scientific article; zbMATH DE number 2080040
• Model checking of probabilistic and nondeterministic systems

Cited in

(5)

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

Describes a project that uses

Uses Software

• Isabelle/HOL
• PRISM

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)