A game-based abstraction-refinement framework for Markov decision processes

DOI10.1007/s10703-010-0097-6zbMath1233.90276OpenAlexW2052092737MaRDI QIDQ600979

Sumit K. Garg

Publication date: 3 November 2010

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://ora.ox.ac.uk/objects/uuid:f7858593-ff60-4ffa-b066-e49fec7c5b1d

zbMATH Keywords

Markov decision processesabstractionabstraction refinementprobabilistic verification

Mathematics Subject Classification ID

Stochastic programming (90C15) Stochastic games, stochastic differential games (91A15) Markov and semi-Markov decision processes (90C40)

Related Items (25)

Model checking finite-horizon Markov chains with probabilistic inference ⋮ Reachability in MDPs: Refining Convergence of Value Iteration ⋮ Parameter Synthesis for Probabilistic Timed Automata Using Stochastic Game Abstractions ⋮ Model Checking Probabilistic Systems ⋮ Parameter synthesis for probabilistic timed automata using stochastic game abstractions ⋮ Interval iteration algorithm for MDPs and IMDPs ⋮ Out of control: reducing probabilistic models by control-state elimination ⋮ On Abstraction of Probabilistic Systems ⋮ Value iteration for simple stochastic games: stopping criterion and learning algorithm ⋮ k-Inductive Barrier Certificates for Stochastic Systems ⋮ Compositional synthesis of control barrier certificates for networks of stochastic systems against \(\omega\)-regular specifications ⋮ Probabilistic verification of Herman's self-stabilisation algorithm ⋮ Collaborative models for autonomous systems controller synthesis ⋮ Abstract model repair for probabilistic systems ⋮ Unnamed Item ⋮ Local abstraction refinement for probabilistic timed programs ⋮ Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops ⋮ The complexity of synchronizing Markov decision processes ⋮ Model checking for probabilistic timed automata ⋮ Probabilistic guarantees for safe deep reinforcement learning ⋮ Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games ⋮ A linear process-algebraic format with data for probabilistic automata ⋮ Stochastic Games for Verification of Probabilistic Timed Automata ⋮ Automata-based controller synthesis for stochastic systems: a game framework via approximate probabilistic relations ⋮ Comparison of algorithms for simple stochastic games

Uses Software

• PRISM
• PASS
• CEGAR

Cites Work

• Performance analysis of probabilistic timed automata using digital clocks
• Bisimulation through probabilistic testing
• The complexity of stochastic games
• Approximating labelled Markov processes
• Concurrent reachability games
• Abstract interpretation of programs as Markov decision processes
• Probabilistic guarded commands mechanized in HOL
• A counterexample-guided abstraction-refinement framework for markov decision processes
• Probabilistic CEGAR
• Abstraction Refinement for Probabilistic Software
• Stochastic Games for Verification of Probabilistic Timed Automata
• Best Probabilistic Transformers
• An Analysis of Stochastic Shortest Path Problems
• Validation of Stochastic Systems
• Validation of Stochastic Systems
• Game-Based Probabilistic Predicate Abstraction in PRISM
• Probabilistic Abstract Interpretation of Imperative Programs using Truncated Normal Distributions
• Magnifying-Lens Abstraction for Markov Decision Processes
• Stochastic Games
• Model Checking Software
• Tools and Algorithms for the Construction and Analysis of Systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A game-based abstraction-refinement framework for Markov decision processes