Cover Image

Learning Algorithms for Verification of Markov Decision Processes

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Brázdil, Tomáš, Chatterjee, Krishnendu, Chmelik, Martin, Forejt, Vojtěch, Křetínský, Jan, Kwiatkowska, Marta, Meggendorfer, Tobias, Parker, David, Ujma, Mateusz
Format:	Preprint
Published:	2024
Subjects:	Systems and Control Artificial Intelligence Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Certified Policy Verification and Synthesis for MDPs under Distributional Reach-avoidance Properties
by: Akshay, S., et al.
Published: (2024)

SemML 2.0: Synthesizing Controllers for LTL
by: Křetínský, Jan, et al.
Published: (2026)

Multiplicative Rewards in Markovian Models
by: Baier, Christel, et al.
Published: (2025)

1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization
by: Azeem, Muqsit, et al.
Published: (2024)

Risk-aware Markov Decision Processes Using Cumulative Prospect Theory
by: Brihaye, Thomas, et al.
Published: (2025)

Probabilistic Model Checking: Applications and Trends
by: Kwiatkowska, Marta, et al.
Published: (2025)

Learning Robust Policies for Uncertain Parametric Markov Decision Processes
by: Rickard, Luke, et al.
Published: (2023)

Sound Value Iteration for Simple Stochastic Games
by: Azeem, Muqsit, et al.
Published: (2024)

IntervalMDP.jl: Accelerated Value Iteration for Interval Markov Decision Processes
by: Mathiesen, Frederik Baymler, et al.
Published: (2024)

SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning
by: Kretinsky, Jan, et al.
Published: (2025)

Fixed Point Certificates for Reachability and Expected Rewards in MDPs
by: Chatterjee, Krishnendu, et al.
Published: (2025)

Stochastic Processes with Expected Stopping Time
by: Chatterjee, Krishnendu, et al.
Published: (2021)

Tools at the Frontiers of Quantitative Verification
by: Andriushchenko, Roman, et al.
Published: (2024)

Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games
by: Grobelna, Marta, et al.
Published: (2025)

Learning Probabilistic Temporal Logic Specifications for Stochastic Systems
by: Roy, Rajarshi, et al.
Published: (2025)

A Lazy Abstraction Algorithm for Markov Decision Processes: Theory and Initial Evaluation
by: Szekeres, Dániel, et al.
Published: (2024)

Logic of Fuzzy Paths
by: Grover, Kush, et al.
Published: (2026)

Stochastic Omega-Regular Verification and Control with Supermartingales
by: Abate, Alessandro, et al.
Published: (2024)

Supermartingale Certificates for Quantitative Omega-regular Verification and Control
by: Henzinger, Thomas A., et al.
Published: (2025)

Projective Fraïssé limits and generalized Ważewski dendrites
by: Codenotti, Alessandro, et al.
Published: (2022)

Strategy Synthesis for Zero-Sum Neuro-Symbolic Concurrent Stochastic Games
by: Yan, Rui, et al.
Published: (2022)

About Time: Model-free Reinforcement Learning with Timed Reward Machines
by: Roy, Rajarshi, et al.
Published: (2025)

Verification of Nonblockingness in Bounded Petri Nets With Minimax Basis Reachability Graphs
by: Gu, Chao, et al.
Published: (2020)

Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs
by: Chatterjee, Krishnendu, et al.
Published: (2024)

Formal Quality Measures for Predictors in Markov Decision Processes
by: Baier, Christel, et al.
Published: (2024)

On the Complexity of Robust Markov Decision Processes and Bisimulation Metrics
by: Suilen, Marnix, et al.
Published: (2026)

HyperCertificates: Verification of Discrete-time Dynamical Systems against HyperLTL Specifications
by: Murali, Vishnu, et al.
Published: (2026)

Sound Statistical Model Checking for Probabilities and Expected Rewards (extended version)
by: Budde, Carlos E., et al.
Published: (2024)

Formal Verification of Linear Temporal Logic Specifications Using Hybrid Zonotope-Based Reachability Analysis
by: Hadjiloizou, Loizos, et al.
Published: (2024)

Certificates and Witnesses for Multi-Objective Queries in Markov Decision Processes
by: Baier, Christel, et al.
Published: (2024)

Robust Conformal Prediction for STL Runtime Verification under Distribution Shift
by: Zhao, Yiqi, et al.
Published: (2023)

Distributionally Robust Predictive Runtime Verification under Spatio-Temporal Logic Specifications
by: Zhao, Yiqi, et al.
Published: (2025)

MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints
by: Bals, Severin, et al.
Published: (2023)

Robust Verification of Concurrent Stochastic Games
by: He, Angel Y., et al.
Published: (2026)

TIUP: Effective Processor Verification with Tautology-Induced Universal Properties
by: Li, Yufeng, et al.
Published: (2024)

Verification of Quantum Circuits through Discrete-Time Barrier Certificates
by: Lewis, Marco, et al.
Published: (2024)

Best-Effort Policies for Robust Markov Decision Processes
by: Abate, Alessandro, et al.
Published: (2025)

Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems
by: Zhou, Yuhao, et al.
Published: (2023)

Certificates and Witnesses for Multi-objective ω-regular Queries in Markov Decision Processes
by: Baier, Christel, et al.
Published: (2025)

Inferentialist Resource Semantics
by: Gheorghiu, Alexander V., et al.
Published: (2024)