Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes

DOI10.1007/S00236-016-0255-4zbMATH Open1378.68122arXiv1407.5396OpenAlexW2298024238MaRDI QIDQ2407982FDOQ2407982

Authors: Aaron Bohy, Véronique Bruyère, Jean-François Raskin, Nathalie Bertrand 

Publication date: 9 October 2017

Published in: Acta Informatica (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1407.5396

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

Mathematics Subject Classification ID

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Graph-Based Algorithms for Boolean Function Manipulation
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Symbolic model checking: \(10^{20}\) states and beyond
• STRIPS: A new approach to the application of theorem proving to problem solving
• Title not available (Why is that?)
• Title not available (Why is that?)
• Bisimulation through probabilistic testing
• A logic for reasoning about time and reliability
• Three Partition Refinement Algorithms
• Exact and ordinary lumpability in finite Markov chains
• An Analysis of Stochastic Shortest Path Problems
• Optimal state-space lumping in Markov chains
• Verifying programs with unreliable channels
• Computable fixpoints in well-structured symbolic model checking
• Comparative branching-time semantics for Markov chains
• Well-structured transition systems everywhere!
• Synthesizing efficient controllers
• Antichains: A New Algorithm for Checking Universality of Finite Automata
• On Finding Optimal Policies in Discrete Dynamic Programming with No Discounting
• Ordering by Divisibility in Abstract Algebras
• Antichains and compositional algorithms for LTL synthesis
• Improved Algorithms for the Automata-Based Approach to Model-Checking
• Title not available (Why is that?)
• Synthesis from LTL specifications with mean-payoff objectives
• Verifying nondeterministic probabilistic channel systems against ω-regular linear-time properties
• Symbolic Verification of Communicating Systems with Probabilistic Message Losses: Liveness and Fairness

Cited In (1)

• Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives

Uses Software

• PRISM
• MRMC
• Graphplan
• Antichains
• Acacia+

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)