Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives.

Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives.

We show that the controller synthesis and verification problems for Markov decision processes with qualitative PECTL* objectives are 2-EXPTIME complete. More precisely, the algorithms are polynomial in the size of a given Markov decision process and doubly exponential in the size of a given qualitat...

Πλήρης περιγραφή

Λεπτομέρειες βιβλιογραφικής εγγραφής
Κύριοι συγγραφείς:	Brázdil, T, Forejt, V, Kucera, A
Άλλοι συγγραφείς:	Aceto, L
Μορφή:	Journal article
Γλώσσα:	English
Έκδοση:	Springer 2008

Παρόμοια τεκμήρια

Markov Decision Processes with Multiple Long-run Average Objectives
ανά: Brázdil, T, κ.ά.
Έκδοση: (2011)

Reachability in recursive Markov decision processes.
ανά: Brázdil, T, κ.ά.
Έκδοση: (2008)

Markov Decision Processes with Multiple Long-run Average Objectives
ανά: Tomáš Brázdil, κ.ά.
Έκδοση: (2014-02-01)

Trading Performance for Stability in Markov Decision Processes
ανά: Brázdil, T, κ.ά.
Έκδοση: (2013)

Trading performance for stability in Markov decision processes
ανά: Brazdil, T, κ.ά.
Έκδοση: (2016)

Branching-Time Model-Checking of Probabilistic Pushdown Automata.
ανά: Brázdil, T, κ.ά.
Έκδοση: (2009)

Continuous-Time Stochastic Games with Time-Bounded Reachability.
ανά: Brázdil, T, κ.ά.
Έκδοση: (2009)

Multi-objective robust strategy synthesis for Interval Markov decision processes
ανά: Hahn, E, κ.ά.
Έκδοση: (2017)

Life is Random, Time is Not: Markov Decision Processes with Window Objectives
ανά: Thomas Brihaye, κ.ά.
Έκδοση: (2020-12-01)

Synchronizing Objectives for Markov Decision Processes
ανά: Mahsa Shirmohammadi, κ.ά.
Έκδοση: (2011-02-01)

The Satisfiability Problem for Probabilistic CTL.
ανά: Brázdil, T, κ.ά.
Έκδοση: (2008)

Stability in graphs and games
ανά: Brázdil, T, κ.ά.
Έκδοση: (2016)

Quantitative Multi-objective Verification for Probabilistic Systems.
ανά: Forejt, V, κ.ά.
Έκδοση: (2011)

MULTI-OBJECTIVE MODEL CHECKING OF MARKOV DECISION PROCESSES
ανά: Etessami, K, κ.ά.
Έκδοση: (2008)

Multi-Objective Model Checking of Markov Decision Processes
ανά: Kousha Etessami, κ.ά.
Έκδοση: (2008-11-01)

Multi-weighted Markov Decision Processes with Reachability Objectives
ανά: Patricia Bouyer, κ.ά.
Έκδοση: (2018-09-01)

Verification of general Markov decision processes by approximate similarity relations and policy refinement
ανά: Haesaert, S, κ.ά.
Έκδοση: (2017)

Faster Convergence of Modified Policy Iteration for Quantitative Verification of Markov Decision Processes
ανά: M.S. Mohagheghi
Έκδοση: (2018-12-01)

Geometric branching reproduction Markov processes
ανά: Assen Tchorbadjieff, κ.ά.
Έκδοση: (2020-09-01)

Nonlinear Markov branching processes with immigration and resurrection
ανά: Zhang Lina, κ.ά.
Έκδοση: (2024-10-01)

Markov decision processes /
ανά: 352167 White, D. J.
Έκδοση: (1993)

Controllable Summarization with Constrained Markov Decision Process
ανά: Hou Pong Chan, κ.ά.
Έκδοση: (2021-01-01)

Bounds for Markov Decision Processes
ανά: Desai, Vijay V., κ.ά.
Έκδοση: (2019)

Framework for solving time-delayed Markov Decision Processes
ανά: Yorgo Sawaya, κ.ά.
Έκδοση: (2023-07-01)

Quantum logic gate synthesis as a Markov decision process
ανά: M. Sohaib Alam, κ.ά.
Έκδοση: (2023-10-01)

Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes
ανά: Krishnendu Chatterjee, κ.ά.
Έκδοση: (2017-07-01)

The complexity of Markov decision processes
Έκδοση: (2003)

Markov decision processes approximation with coupled dynamics via Markov deterministic control systems
ανά: Portillo-Ramírez Gustavo, κ.ά.
Έκδοση: (2023-10-01)

Symblicit algorithms for optimal strategy synthesis in monotonic Markov decision processes
ανά: Aaron Bohy, κ.ά.
Έκδοση: (2014-07-01)

Safety Verification of Continuous-Space Pure Jump Markov Processes
ανά: Esmaeil Zadeh Soudjani, S, κ.ά.
Έκδοση: (2016)

Convergence Rates and Limit Theorems for the Dual Markov Branching Process
ανά: Anthony G. Pakes
Έκδοση: (2017-01-01)

The multiple birth properties of multi-type Markov branching processes
ανά: Junping Li, κ.ά.
Έκδοση: (2024-09-01)

Verification of Linear Duration Properties over Continuous Time Markov Chains
ανά: Chen, T, κ.ά.
Έκδοση: (2012)

Verification of Linear Duration Properties over Continuous−Time Markov Chains
ανά: Chen, T, κ.ά.
Έκδοση: (2012)

Monotone optimal control for a class of Markov decision processes
ανά: Li, Michael Z. F., κ.ά.
Έκδοση: (2013)

Polynomial time algorithms for finite horizon, stationary Markov decision processes
Έκδοση: (2003)

Comparing labelled Markov decision processes
ανά: Kiefer, S, κ.ά.
Έκδοση: (2020)

Communicating via Markov decision processes
ανά: Sokota, S, κ.ά.
Έκδοση: (2022)

Entropic Regularization of Markov Decision Processes
ανά: Boris Belousov, κ.ά.
Έκδοση: (2019-07-01)

Markov abstractions for PAC reinforcement learning in non-Markov decision processes
ανά: Ronca, A, κ.ά.
Έκδοση: (2022)