Probabilistic CEGAR

DOI10.1007/978-3-540-70545-1_16MaRDI QIDQ3512491zbMATH OpenOpenAlexFDO

Authors Holger Hermanns, Björn Wachter, Lijun 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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A counterexample-guided abstraction-refinement framework for Markov decision processes
• Abstract Counterexamples for Non-disjunctive Abstractions
• Constrained monotonic abstraction: a CEGAR for parameterized verification
• Partial predicate abstraction and counter-example guided refinement
• scientific article; zbMATH DE number 1670775

Cites work

• A logic for reasoning about time and reliability
• Abstractions from proofs
• An interpolating theorem prover
• Counterexamples in Probabilistic Model Checking
• Formal Modeling and Analysis of Timed Systems
• Generalized best-first search strategies and the optimality of A*
• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 700091 (Why is no real title available?)
• scientific article; zbMATH DE number 2090703 (Why is no real title available?)
• scientific article; zbMATH DE number 794262 (Why is no real title available?)
• Lazy abstraction
• Lazy Abstraction with Interpolants
• Magnifying-Lens Abstraction for Markov Decision Processes
• Model checking of probabilistic and nondeterministic systems
• Model Checking Software
• Optimization, approximation, and complexity classes

Cited in

(25)

• Abstract model repair for probabilistic systems
• Probabilistic verification of Herman's self-stabilisation algorithm
• Automated verification and synthesis of stochastic hybrid systems: a survey
• Partial predicate abstraction and counter-example guided refinement
• Local abstraction refinement for probabilistic timed programs
• On Abstraction of Probabilistic Systems
• A counterexample-guided abstraction-refinement framework for Markov decision processes
• Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
• A Probabilistic Learning Approach for Counterexample Guided Abstraction Refinement
• Constrained monotonic abstraction: a CEGAR for parameterized verification
• Abstract Counterexample-Based Refinement for Powerset Domains
• Abstract Counterexamples for Non-disjunctive Abstractions
• Compositional abstraction for stochastic systems
• Safety verification for probabilistic hybrid systems
• Minimal counterexamples for linear-time probabilistic verification
• Farkas certificates and minimal witnesses for probabilistic reachability constraints
• Model checking linear-time properties of probabilistic systems
• Counterexample generation for discrete-time Markov models: an introductory survey
• Constraint Markov chains
• A game-based abstraction-refinement framework for Markov decision processes
• Abstraction-Refinement for Hierarchical Probabilistic Models
• Witnessing subsystems for probabilistic systems with low tree width
• 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

Describes a project that uses

Uses Software

• CEGAR

This page was built for publication: Probabilistic CEGAR

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3512491)