MDPs as distribution transformers: affine invariant synthesis for safety objectives
type: Item
instance of: scholarly article
title: MDPs as distribution transformers: affine invariant synthesis for safety objectives
zbMATH Open document ID: 1547.68401
DOI: 10.1007/978-3-031-37709-9_5
author: S. Akshay
author: Krishnendu Chatterjee
author: Tobias Meggendorfer
author: Đorđe Žikelić
publication date: 2024-02-01T00:00:00Z
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 90C40
zbMATH DE Number: 7798094
zbMATH Keywords: Markov decision processes
zbMATH Keywords: invariant synthesis
zbMATH Keywords: distribution transformers
zbMATH Keywords: Skolem hardness
MaRDI profile type: Publication
cites work: Approximate Verification of the Symbolic Dynamics of Markov Chains
cites work: Reachability problems for Markov chains
cites work: Distribution-based objectives for Markov Decision Processes
cites work: Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs
cites work: Q5322945
cites work: Probabilistic program verification via inductive synthesis of inductive invariants
cites work: Latticed \(k\)-induction with an application to probabilistic programs
cites work: A Logic of Probability with Decidable Model Checking
cites work: Q4836494
cites work: Computer Aided Verification
cites work: Termination Analysis of Probabilistic Programs Through Positivstellensatz’s
cites work: Non-polynomial worst-case analysis of recursive programs
cites work: Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs
cites work: Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs
cites work: On Lexicographic Proof Rules for Probabilistic Termination
cites work: Stochastic invariants for probabilistic termination
cites work: The MathSAT5 SMT Solver
cites work: Q2769578
cites work: Q4414726
cites work: Theorie der einfachen Ungleichungen.
cites work: Understanding and using linear programming
cites work: Representing polynomials by positive linear functions on compact convex polyhedra
cites work: Multivariate amortized resource analysis
cites work: Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms
cites work: Principles of systems design. Essays dedicated to Thomas A. Henzinger on the occasion of his 60th birthday
cites work: Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes
cites work: Abstraction, Refinement and Proof for Probabilistic Systems
cites work: Performance Analysis of Communications Networks and Systems
cites work: Decision Problems for Linear Recurrence Sequences
cites work: Positivity Problems for Low-Order Linear Recurrence Sequences
cites work: Verification, Model Checking, and Abstract Interpretation
cites work: Q4315289
cites work: Q4285035
cites work: Automatic generation of polynomial invariants of bounded degree using abstract interpretation
description: scientific article; zbMATH DE number 7798094