Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking
From MaRDI portal
Publication:3600486
DOI10.1007/978-3-540-93900-9_29zbMath1206.68195OpenAlexW1504403751MaRDI QIDQ3600486
Bernd Becker, Ralf Wimmer, Bettina Braitling
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
Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)
Related Items (7)
Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints ⋮ Latticed \(k\)-induction with an application to probabilistic programs ⋮ Model checking finite-horizon Markov chains with probabilistic inference ⋮ Counterexamples in Probabilistic LTL Model Checking for Markov Chains ⋮ Out of control: reducing probabilistic models by control-state elimination ⋮ Minimal counterexamples for linear-time probabilistic verification ⋮ Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey
Uses Software
This page was built for publication: Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking