Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes
From MaRDI portal
Publication:2407982
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60) Markov and semi-Markov decision processes (90C40)
Abstract: When treating Markov decision processes (MDPs) with large state spaces, using explicit representations quickly becomes unfeasible. Lately, Wimmer et al. have proposed a so-called symblicit algorithm for the synthesis of optimal strategies in MDPs, in the quantitative setting of expected mean-payoff. This algorithm, based on the strategy iteration algorithm of Howard and Veinott, efficiently combines symbolic and explicit data structures, and uses binary decision diagrams as symbolic representation. The aim of this paper is to show that the new data structure of pseudo-antichains (an extension of antichains) provides another interesting alternative, especially for the class of monotonic MDPs. We design efficient pseudo-antichain based symblicit algorithms (with open source implementations) for two quantitative settings: the expected mean-payoff and the stochastic shortest path. For two practical applications coming from automated planning and LTL synthesis, we report promising experimental results w.r.t. both the run time and the memory consumption.
Recommendations
- Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives
- Efficient strategy iteration for mean payoff in Markov decision processes
- Stochastic shortest paths and weight-bounded properties in Markov decision processes
- The complexity of synchronizing Markov decision processes
- Symbolic algorithms for graphs and Markov decision processes with fairness objectives
Cites work
- scientific article; zbMATH DE number 3145626 (Why is no real title available?)
- scientific article; zbMATH DE number 3148886 (Why is no real title available?)
- scientific article; zbMATH DE number 1321699 (Why is no real title available?)
- scientific article; zbMATH DE number 1361118 (Why is no real title available?)
- scientific article; zbMATH DE number 700091 (Why is no real title available?)
- scientific article; zbMATH DE number 1134975 (Why is no real title available?)
- scientific article; zbMATH DE number 783783 (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 Analysis of Stochastic Shortest Path Problems
- Antichains and compositional algorithms for LTL synthesis
- Antichains: A New Algorithm for Checking Universality of Finite Automata
- Bisimulation through probabilistic testing
- Comparative branching-time semantics for Markov chains
- Computable fixpoints in well-structured symbolic model checking
- Exact and ordinary lumpability in finite Markov chains
- Graph-Based Algorithms for Boolean Function Manipulation
- Improved Algorithms for the Automata-Based Approach to Model-Checking
- On Finding Optimal Policies in Discrete Dynamic Programming with No Discounting
- Optimal state-space lumping in Markov chains
- Ordering by Divisibility in Abstract Algebras
- STRIPS: A new approach to the application of theorem proving to problem solving
- Symbolic Verification of Communicating Systems with Probabilistic Message Losses: Liveness and Fairness
- Symbolic model checking: \(10^{20}\) states and beyond
- Synthesis from LTL specifications with mean-payoff objectives
- Synthesizing efficient controllers
- Three Partition Refinement Algorithms
- Verifying nondeterministic probabilistic channel systems against ω-regular linear-time properties
- Verifying programs with unreliable channels
- Well-structured transition systems everywhere!
Cited in
(1)
This page was built for publication: Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2407982)
