Cover Image

J-P: MDP. FP. PP.: Characterizing Total Expected Rewards in Markov Decision Processes as Least Fixed Points with an Application to Operational Semantics of Probabilistic Programs (Technical Report)

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Batz, Kevin, Kaminski, Benjamin Lucien, Matheja, Christoph, Winkler, Tobias
Format:	Preprint
Published:	2024
Subjects:	Logic in Computer Science Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Programming and Reasoning in Partially Observable Probabilistic Environments
by: Gürtler, Tobias, et al.
Published: (2025)

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

noDice: Inference for Discrete Probabilistic Programs with Nondeterminism and Conditioning
by: Gürtler, Tobias, et al.
Published: (2026)

Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
by: Batz, Kevin, et al.
Published: (2025)

CTL* Model Checking on Infinite Families of Finite-State Labeled Transition Systems (Technical Report)
by: Pettinau, Roberto, et al.
Published: (2026)

Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains
by: Mertens, Hannah, et al.
Published: (2024)

The Algebra of Iterative Constructions
by: Batz, Kevin, et al.
Published: (2026)

Verifying Sampling Algorithms via Distributional Invariants
by: Zilken, Daniel, et al.
Published: (2025)

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

Model Checking Temporal Properties of Recursive Probabilistic Programs
by: Winkler, Tobias, et al.
Published: (2021)

Caesar: A Deductive Verifier for Probabilistic Programs
by: Schröer, Philipp, et al.
Published: (2026)

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

A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests
by: Verscht, Lena, et al.
Published: (2024)

Strong Nominal Semantics for Fixed-Point Constraints
by: Caires-Santos, Ali K., et al.
Published: (2024)

Fixed Point Theorems in Computability Theory
by: Terwijn, Sebastiaan A.
Published: (2024)

Efficient Probabilistic Model Checking for Relational Reachability (Extended Version)
by: Gerlach, Lina, et al.
Published: (2025)

Diagonalizing Through the $ω$-Chain: Iterated Self-Certification on Bounded Turing Machines and its Least Fixed Point
by: Sung, Miara
Published: (2026)

A Translation of Probabilistic Event Calculus into Markov Decision Processes
by: Xu, Lyris, et al.
Published: (2025)

Denotational Semantics for Probabilistic and Concurrent Programs
by: Zilberstein, Noam, et al.
Published: (2025)

Partial Incorrectness Logic
by: Verscht, Lena, et al.
Published: (2025)

On Explicit Solutions to Fixed-Point Equations in Propositional Dynamic Logic
by: Lyon, Tim S.
Published: (2024)

Witnessed Symmetric Choice and Interpretations in Fixed-Point Logic with Counting
by: Lichter, Moritz
Published: (2022)

Definable sets in Skolem arithmetic
by: Kamiński, Łukasz
Published: (2025)

On Probabilistic and Causal Reasoning with Summation Operators
by: Ibeling, Duligur, et al.
Published: (2024)

Functional variant of Polynomial Analogue of Gandy's Fixed Point Theorem
by: Nechesov, Andrey
Published: (2024)

Solving Decision Theory Problems with Probabilistic Answer Set Programming
by: Azzolini, Damiano, et al.
Published: (2024)

Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains
by: Spork, Timm, et al.
Published: (2025)

Dependency Pairs for Expected Innermost Runtime Complexity and Strong Almost-Sure Termination of Probabilistic Term Rewriting
by: Kassing, Jan-Christoph, et al.
Published: (2025)

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

Quantifier Elimination and Craig Interpolation, Quantitatively
by: Batz, Kevin, et al.
Published: (2025)

Automated Expected Amortised Cost Analysis of Probabilistic Data Structures
by: Leutgeb, Lorenz, et al.
Published: (2022)

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)

Inapproximability of Unique Games in Fixed-Point Logic with Counting
by: Tucker-Foltz, Jamie
Published: (2021)

Evidence-Tracked Tape Semantics for Probabilistic Computation
by: Cohen, Liron, et al.
Published: (2026)

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

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

To Zip Through the Cost Analysis of Probabilistic Programs
by: Hetzenberger, Matthias, et al.
Published: (2025)

Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics
by: Kaye, George
Published: (2025)

A Sequent Calculus Perspective on Base-Extension Semantics (Technical Report)
by: Barroso-Nascimento, Victor, et al.
Published: (2025)