Magnifying-Lens Abstraction for Markov Decision Processes

DOI10.1007/978-3-540-73368-3_38MaRDI QIDQ5429327zbMATH OpenOpenAlexFDO

Authors Luca De Alfaro, Pritam Roy

Publication date 29 November 2007

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-73368-3_38

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A game-based abstraction-refinement framework for Markov decision processes
• scientific article; zbMATH DE number 1884411
• scientific article; zbMATH DE number 2090703
• Abstraction and approximate decision-theoretic planning.
• Abstract interpretation of programs as Markov decision processes

Cited in

(12)

• Lifted model checking for relational MDPs
• Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives
• Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives
• Analyzing oscillatory behavior with formal methods
• On Abstraction of Probabilistic Systems
• Probabilistic CEGAR
• Compositional abstraction for stochastic systems
• Three-valued abstraction for probabilistic systems
• Approximating probabilistic behaviors of biological systems using abstract interpretation
• Game-Based Probabilistic Predicate Abstraction in PRISM
• A game-based abstraction-refinement framework for Markov decision processes
• A linear process-algebraic format with data for probabilistic automata

Describes a project that uses

Uses Software

• PRISM

This page was built for publication: Magnifying-Lens Abstraction for Markov Decision Processes

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