Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking
From MaRDI portal
Publication:3600486
DOI10.1007/978-3-540-93900-9_29zbMath1206.68195MaRDI 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
68Q60: Specification and verification (program logics, model checking, etc.)
68Q87: Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
Related Items
Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints, Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey, 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, Out of control: reducing probabilistic models by control-state elimination, Counterexamples in Probabilistic LTL Model Checking for Markov Chains
Uses Software