Multi-objective Model Checking of Markov Decision Processes

DOI10.1007/978-3-540-71209-1_6MaRDI QIDQ5758101zbMATH OpenOpenAlexFDO

Authors Kousha Etessami, Marta Kwiatkowska, Moshe Y. Vardi, Mihalis Yannakakis

Publication date 3 September 2007

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-71209-1_6

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Recommendations

• Multi-Objective Model Checking of Markov Decision Processes
• Markov Decision Processes with Multiple Objectives
• Markov Decision Processes with Multiple Long-Run Average Objectives
• Markov decision processes with multiple long-run average objectives
• Multi-cost bounded tradeoff analysis in MDP

Cited in

(33)

• Model checking hyperproperties for Markov decision processes
• An STL-based formulation of resilience in cyber-physical systems
• Multi-cost bounded tradeoff analysis in MDP
• Multi-cost bounded reachability in MDP
• Deniable Functional Encryption
• Multi-objective discounted reward verification in graphs and MDPs
• Compositional reasoning for Markov decision processes (extended abstract)
• Multiple-environment Markov decision processes
• Quantitative multi-objective verification for probabilistic systems
• Synthesizing efficient systems in probabilistic environments
• Sequential convex programming for the efficient verification of parametric MDPs
• Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives
• Multi-Objective Model Checking of Markov Decision Processes
• Probabilistic Systems with LimSup and LimInf Objectives
• Compositional probabilistic verification through multi-objective model checking
• Model and objective separation with conditional lower bounds: disjunction is harder than conjunction
• Pareto curves for probabilistic model checking
• Simple strategies in multi-objective MDPs
• Life is random, time is not: Markov decision processes with window objectives
• Distribution-based objectives for Markov decision processes
• Mixing probabilistic and non-probabilistic objectives in Markov decision processes
• Markov Decision Processes with Multiple Objectives
• Markov Decision Processes with Multiple Long-Run Average Objectives
• Combinations of Qualitative Winning for Stochastic Parity Games
• Percentile queries in multi-dimensional Markov decision processes
• An extended ϵ‐constraint method for a multiobjective finite‐horizon Markov decision process
• Model-Free Reinforcement Learning for Lexicographic Omega-Regular Objectives
• Extended beam search for non-exhaustive state space analysis
• Compositional probabilistic model checking with string diagrams of MDPs
• Interval Markov decision processes with multiple objectives: from robust strategies to Pareto curves
• Multi-objective -regular reinforcement learning
• Average reward reinforcement learning for omega-regular and mean-payoff objectives
• CEGAR for compositional analysis of qualitative properties in Markov decision processes

This page was built for publication: Multi-objective Model Checking of Markov Decision Processes

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