Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking
DOI10.1007/978-3-540-93900-9_29zbMATH Open1206.68195OpenAlexW1504403751MaRDI QIDQ3600486FDOQ3600486
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
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
Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60)
Cited In (7)
- Minimal counterexamples for linear-time probabilistic verification
- Latticed \(k\)-induction with an application to probabilistic programs
- Model checking finite-horizon Markov chains with probabilistic inference
- Counterexample generation for discrete-time Markov models: an introductory survey
- Farkas certificates and minimal witnesses for probabilistic reachability constraints
- Out of control: reducing probabilistic models by control-state elimination
- Counterexamples in Probabilistic LTL Model Checking for Markov Chains
Uses Software
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)
