Hierarchical Counterexamples for Discrete-Time Markov Chains

DOI10.1007/978-3-642-24372-1_33zbMath1348.68139OpenAlexW1529165591WikidataQ57801248 ScholiaQ57801248MaRDI QIDQ3172933

Erika Ábrahám, Bernd Becker, Jens Katelaan, Ralf Wimmer, Nils Jansen, Joost-Pieter Katoen

Publication date: 7 October 2011

Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-24372-1_33

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

Related Items

Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints ⋮ On Abstraction of Probabilistic Systems ⋮ Minimal counterexamples for linear-time probabilistic verification ⋮ Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey

Uses Software

• PRISM
• MRMC