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)