Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking

DOI10.1007/978-3-540-93900-9_29MaRDI QIDQ3600486zbMATH OpenOpenAlexFDO

Authors Ralf Wimmer, Bettina Braitling, Bernd Becker

Publication date 10 February 2009

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-93900-9_29

Mathematics Subject Classification ID

Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Counterexample generation for discrete-time Markov models: an introductory survey
• Hierarchical counterexamples for discrete-time Markov chains
• Counterexamples revisited: principles, algorithms, applications
• Constraint-based debugging in probabilistic model checking
• Providing Evidence of Likely Being on Time: Counterexample Generation for CTMC Model Checking

Cited in

(7)

• Latticed \(k\)-induction with an application to probabilistic programs
• Model checking finite-horizon Markov chains with probabilistic inference
• Minimal counterexamples for linear-time probabilistic verification
• Out of control: reducing probabilistic models by control-state elimination
• Counterexamples in Probabilistic LTL Model Checking for Markov Chains
• Counterexample generation for discrete-time Markov models: an introductory survey
• Farkas certificates and minimal witnesses for probabilistic reachability constraints

Describes a project that uses

Uses Software

• MiniSat

This page was built for publication: Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking

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