Verification of General Markov Decision Processes by Approximate Similarity Relations and Policy Refinement

DOI10.1137/16M1079397zbMath1367.93615MaRDI QIDQ5348126

Sadegh Esmaeil Zadeh Soudjani, Alessandro Abate, Sofie Haesaert

Publication date: 14 August 2017

Published in: SIAM Journal on Control and Optimization (Search for Journal in Brave)

zbMATH Keywords

verificationcorrect-by-constructionpolicy refinementapproximate probabilistic simulation relations

Mathematics Subject Classification ID

Discrete-time control/observation systems (93C55) Synthesis problems (93B50) Markov and semi-Markov decision processes (90C40) Specification and verification (program logics, model checking, etc.) (68Q60) Stochastic systems in control theory (general) (93E03)

Related Items (11)

Robust Control for Dynamical Systems with Non-Gaussian Noise via Formal Abstractions ⋮ Similarity quantification for linear stochastic systems: a coupling compensator approach ⋮ Compositional abstraction of large-scale stochastic systems: a relaxed dissipativity approach ⋮ Certified reinforcement learning with logic guidance ⋮ SySCoRe: Synthesis via Stochastic Coupling Relations ⋮ Compositional abstraction-based synthesis for continuous-time stochastic hybrid systems ⋮ Compositional construction of infinite abstractions for networks of stochastic control systems ⋮ Compositional abstraction-based synthesis of general MDPs via approximate probabilistic relations ⋮ Safe-visor architecture for sandboxing (AI-based) unverified controllers in stochastic cyber-physical systems ⋮ Automated verification and synthesis of stochastic hybrid systems: a survey ⋮ Automata-based controller synthesis for stochastic systems: a game framework via approximate probabilistic relations

Uses Software

• CVX
• FAUST2

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Approximation metrics based on probabilistic bisimulations for general state-space Markov processes: a survey
• Metrics for labelled Markov processes
• Markov chains and stochastic stability
• Hierarchical control system design using approximate simulation
• Stochastic optimal control. The discrete time case
• Bisimulation through probabilistic testing
• Approximating labelled Markov processes
• Verification of general Markov decision processes by approximate similarity relations and policy refinement
• The existence of probability measures with given marginals
• Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems
• On the effect of perturbation of conditional probabilities in total variation
• Bisimulation for labelled Markov processes
• Adaptive and Sequential Gridding Procedures for the Abstraction and Verification of Stochastic Processes
• Symbolic Control of Stochastic Systems via Approximately Bisimilar Finite Abstractions
• Robust PCTL model checking
• On Probabilistic Alternating Simulations
• Quantitative Approximation of the Probability Distribution of a Markov Process by Formal Abstractions
• Verification and Control of Hybrid Systems
• Semi-pullbacks and bisimulation in categories of Markov processes
• Average Optimality in Markov Control Processes via Discounted-Cost Problems and Linear Programming
• Approximations of Stochastic Hybrid Systems
• Probabilistic Model Checking of Labelled Markov Processes via Finite Approximate Bisimulations
• The Existence of Probability Measures with Given Marginals
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control

This page was built for publication: Verification of General Markov Decision Processes by Approximate Similarity Relations and Policy Refinement