CTL model checking of MDPs over distribution spaces: algorithms and sampling-based computations

DOI10.1145/3641513.3651397MaRDI QIDQ6993491zbMATH OpenFDO

Authors Yulong Gao, Karl Henrik Johansson, Alessandro Abate

Publication date 25 April 2025

Full work available at URL https://doi.org/10.1145/3641513.3651397

zbMATH Keywords

Markov decision processescomputation tree logicreachability analysistransient probability distributions

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30)

Cites work

• scientific article; zbMATH DE number 438994 (Why is no real title available?)
• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 1348599 (Why is no real title available?)
• scientific article; zbMATH DE number 1948170 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• A logic for reasoning about time and reliability
• An algorithm for multi-parametric quadratic programming and explicit MPC solutions
• An extension of Karmarkar's projective algorithm for convex quadratic programming
• Approximate verification of the symbolic dynamics of Markov chains
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Characterization and computation of infinite-horizon specifications over Markov processes
• Complexity estimates for Fourier-Motzkin elimination
• Computing Probabilistic Controlled Invariant Sets
• Distribution-based objectives for Markov decision processes
• Equivalence between polyhedral projection, multiple objective linear programming and vector linear programming
• Formal methods for discrete-time dynamical systems
• MDPs as distribution transformers: affine invariant synthesis for safety objectives
• Practical polytope volume approximation
• Probabilistic Bisimulation: Naturally on Distributions
• Reachability problems for Markov chains
• Stochastic model checking
• The probabilistic model checking landscape
• The quickhull algorithm for convex hulls

This page was built for publication: CTL model checking of MDPs over distribution spaces: algorithms and sampling-based computations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6993491)