Probabilistic CEGAR
From MaRDI portal
Publication:3512491
DOI10.1007/978-3-540-70545-1_16zbMath1155.68438OpenAlexW2913788705MaRDI QIDQ3512491
Holger Hermanns, Björn Wachter, Li-jun Zhang
Publication date: 15 July 2008
Published in: Computer Aided Verification (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-70545-1_16
Related Items (17)
Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints ⋮ Model Checking Linear-Time Properties of Probabilistic Systems ⋮ A game-based abstraction-refinement framework for Markov decision processes ⋮ On Abstraction of Probabilistic Systems ⋮ Safety verification for probabilistic hybrid systems ⋮ Minimal counterexamples for linear-time probabilistic verification ⋮ Probabilistic verification of Herman's self-stabilisation algorithm ⋮ Abstract model repair for probabilistic systems ⋮ Local abstraction refinement for probabilistic timed programs ⋮ Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops ⋮ Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey ⋮ Constraint Markov chains ⋮ CEGAR for compositional analysis of qualitative properties in Markov decision processes ⋮ A linear process-algebraic format with data for probabilistic automata ⋮ Probabilistic model checking of biological systems with uncertain kinetic rates ⋮ Compositional Abstraction for Stochastic Systems ⋮ Automated verification and synthesis of stochastic hybrid systems: a survey
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Optimization, approximation, and complexity classes
- A logic for reasoning about time and reliability
- An interpolating theorem prover
- Model checking of probabilistic and nondeterministic systems
- Abstractions from proofs
- Generalized best-first search strategies and the optimality of A*
- Lazy abstraction
- Magnifying-Lens Abstraction for Markov Decision Processes
- Lazy Abstraction with Interpolants
- Counterexamples in Probabilistic Model Checking
- Formal Modeling and Analysis of Timed Systems
- Model Checking Software
This page was built for publication: Probabilistic CEGAR
