A counterexample-guided abstraction-refinement framework for markov decision processes
From MaRDI portal
Publication:2946618
DOI10.1145/1838552.1838553zbMath1351.68154arXiv0807.1173OpenAlexW2088501121WikidataQ124971478 ScholiaQ124971478MaRDI QIDQ2946618
Mahesh Viswanathan, Rohit Chadha
Publication date: 17 September 2015
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/0807.1173
Markov and semi-Markov decision processes (90C40) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)
Related Items (9)
Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints ⋮ Latticed \(k\)-induction with an application to probabilistic programs ⋮ A game-based abstraction-refinement framework for Markov decision processes ⋮ On Abstraction of Probabilistic Systems ⋮ Minimal counterexamples for linear-time probabilistic verification ⋮ Abstract model repair for probabilistic systems ⋮ Bayesian statistical model checking with application to Stateflow/Simulink verification ⋮ Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey ⋮ CEGAR for compositional analysis of qualitative properties in Markov decision processes
This page was built for publication: A counterexample-guided abstraction-refinement framework for markov decision processes