Cover Image

Certified Policy Verification and Synthesis for MDPs under Distributional Reach-avoidance Properties

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Akshay, S., Chatterjee, Krishnendu, Meggendorfer, Tobias, Žikelić, Đorđe
Format:	Preprint
Published:	2024
Subjects:	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

Omega-regular Verification and Control for Distributional Specifications in MDPs
by: Akshay, S., et al.
Published: (2025)

Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization
by: Chatterjee, Krishnendu, et al.
Published: (2024)

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

Learning Algorithms for Verification of Markov Decision Processes
by: Brázdil, Tomáš, et al.
Published: (2024)

SuperDP: Differential Privacy Refutation via Supermartingales
by: Chatterjee, Krishnendu, et al.
Published: (2026)

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

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

Accelerating Policy Synthesis in Large-Scale MDPs via Hierarchical Adaptive Refinement
by: Evangelidis, Alexandros, et al.
Published: (2025)

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

Shields to Guarantee Probabilistic Safety in MDPs
by: Heck, Linus, et al.
Published: (2026)

Order-Sorted Intensional Logic: Expressing Subtyping Polymorphism with Typing Assertions and Quantification over Concepts
by: Marković, Đorđe, et al.
Published: (2025)

The Value Problem for Multiple-Environment MDPs with Parity Objective
by: Chatterjee, Krishnendu, et al.
Published: (2025)

PolyQEnt: A Polynomial Quantified Entailment Solver
by: Chatterjee, Krishnendu, et al.
Published: (2024)

A Certified Proof Checker for Deep Neural Network Verification in Imandra
by: Desmartin, Remi, et al.
Published: (2024)

Presburger Functional Synthesis: Complexity and Tractable Normal Forms
by: Akshay, S., et al.
Published: (2025)

Automated Approach for Solving Infinite-state Polynomial Reachability Games
by: Chatterjee, Krishnendu, et al.
Published: (2026)

Formal Ethical Obligations in Reinforcement Learning Agents: Verification and Policy Updates
by: Shea-Blymyer, Colin, et al.
Published: (2024)

Solving Long-run Average Reward Robust MDPs via Stochastic Games
by: Chatterjee, Krishnendu, et al.
Published: (2023)

Automated Verification of Equivalence Properties in Advanced Logic Programs -- Bachelor Thesis
by: Heuer, Jan
Published: (2023)

Multi-Property Synthesis
by: Weinhuber, Christoph, et al.
Published: (2026)

Abstraction-Based Proof Production in Formal Verification of Neural Networks
by: Elboher, Yizhak Yisrael, et al.
Published: (2025)

Formally Certified Approximate Model Counting
by: Tan, Yong Kiam, et al.
Published: (2024)

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

Towards Neuro-symbolic Causal Rule Synthesis, Verification, and Evaluation Grounded in Legal and Safety Principles
by: Rehan, Zainab, et al.
Published: (2026)

Formal Reasoning About Confidence and Automated Verification of Neural Networks
by: Afzal, Mohammad, et al.
Published: (2025)

Faster Certified Symmetry Breaking Using Orders With Auxiliary Variables
by: Anders, Markus, et al.
Published: (2025)

Constrained and Robust Policy Synthesis with Satisfiability-Modulo-Probabilistic-Model-Checking
by: Heck, Linus, et al.
Published: (2025)

NLP Verification: Towards a General Methodology for Certifying Robustness
by: Casadio, Marco, et al.
Published: (2024)

Policy-Adaptable Methods For Resolving Normative Conflicts Through Argumentation and Graph Colouring
by: Joyce, Johnny
Published: (2025)

Laurel: Unblocking Automated Verification with Large Language Models
by: Mugnier, Eric, et al.
Published: (2024)

Incremental Neural Network Verification via Learned Conflicts
by: Elsaleh, Raya, et al.
Published: (2026)

Entailment vs. Verification for Partial-assignment Satisfiability and Enumeration
by: Sebastiani, Roberto
Published: (2025)

An Information-Flow Perspective on Explainability Requirements: Specification and Verification
by: Finkbeiner, Bernd, et al.
Published: (2025)

Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows
by: Bollig, Benedikt
Published: (2026)

Neural Network Verification using Partial Multi-Neuron Relaxation
by: Shmuel, Ido, et al.
Published: (2026)

BayesL: a Logical Framework for the Verification of Bayesian Networks
by: Nicoletti, Stefano M., et al.
Published: (2025)

Efficient Certified Reasoning for Binarized Neural Networks
by: Yang, Jiong, et al.
Published: (2025)

interwhen: A Generalizable Framework for Steering Reasoning Models with Test-time Verification
by: Bhat, Vishak K, et al.
Published: (2026)

ReVEAL: GNN-Guided Reverse Engineering for Formal Verification of Optimized Multipliers
by: Chen, Chen, et al.
Published: (2025)

VeriFlow: Modeling Distributions for Neural Network Verification
by: Zaid, Faried Abu, et al.
Published: (2024)