The complexity of reachability in parametric Markov decision processes

被引：11
|
作者：
Junges, Sebastian [1 ]
Katoen, Joost-Pieter [2 ]
Perez, Guillermo A. [3 ]
Winkler, Tobias [2 ]
机构：
[1] Univ Calif Berkeley, Berkeley, CA 94720 USA
[2] Rhein Westfal TH Aachen, Aachen, Germany
[3] Univ Antwerp, Antwerp, Belgium
来源：
JOURNAL OF COMPUTER AND SYSTEM SCIENCES | 2021年 / 119卷
基金：
欧洲研究理事会;
关键词：
Parametric Markov decision processes; Formal verification; Existential theory of the reals; Computational complexity; Parameter synthesis; SYSTEMS; MODELS;
D O I：
10.1016/j.jcss.2021.02.006
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
This article presents the complexity of reachability decision problems for parametric Markov decision processes (pMDPs), an extension to Markov decision processes (MDPs) where transitions probabilities are described by polynomials over a finite set of parameters. In particular, we study the complexity of finding values for these parameters such that the induced MDP satisfies some maximal or minimal reachability probability constraints. We discuss different variants depending on the comparison operator in the constraints and the domain of the parameter values. We improve all known lower bounds for this problem, and notably provide ETR-completeness results for distinct variants of this problem. (C) 2021 Elsevier Inc. All rights reserved.
引用
收藏
页码：183 / 210
页数：28
相关论文
共 50 条
  • [1] The Complexity of Graph-Based Reductions for Reachability in Markov Decision Processes
    Le Roux, Stephane
    Perez, Guillermo A.
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, FOSSACS 2018, 2018, 10803 : 367 - 383
  • [2] Reachability in recursive Markov decision processes
    Brazdil, Tomas
    Brozek, Vaclav
    Forejt, Vojtech
    Kucera, Antonin
    INFORMATION AND COMPUTATION, 2008, 206 (05) : 520 - 537
  • [3] Reachability in recursive Markov decision processes
    Brazdil, Tomas
    Brozek, Vaclav
    Forejt, Vojtech
    Kucera, Antonin
    CONCUR 2006 - CONCURRENCY THEORY, PROCEEDINGS, 2006, 4137 : 358 - 374
  • [4] Reachability analysis of quantum Markov decision processes
    Ying, Shenggang
    Ying, Mingsheng
    INFORMATION AND COMPUTATION, 2018, 263 : 31 - 51
  • [5] Anytime Guarantees for Reachability in Uncountable Markov Decision Processes
    Technische Universität München, Germany
    不详
    Leibniz Int. Proc. Informatics, LIPIcs,
  • [6] On a Notion of Resilience for Markov Decision Processes with Reachability Objectives
    Duan, Xiaoming
    Baharisangari, Nasim
    Yan, Rui
    Xu, Zhe
    Ornik, Melkior
    IFAC PAPERSONLINE, 2023, 56 (02): : 11261 - 11266
  • [7] Distributional Reachability for Markov Decision Processes: Theory and Applications
    Gao, Yulong
    Abate, Alessandro
    Xie, Lihua
    Johansson, Karl Henrik
    IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2024, 69 (07) : 4598 - 4613
  • [8] Complexity issues in Markov decision processes
    Goldsmith, J
    Mundhenk, M
    THIRTEENTH ANNUAL IEEE CONFERENCE ON COMPUTATIONAL COMPLEXITY - PROCEEDINGS, 1998, : 272 - 280
  • [9] THE COMPLEXITY OF MARKOV DECISION-PROCESSES
    PAPADIMITRIOU, CH
    TSITSIKLIS, JN
    MATHEMATICS OF OPERATIONS RESEARCH, 1987, 12 (03) : 441 - 450
  • [10] The complexity of synchronizing Markov decision processes
    Doyen, Laurent
    Massart, Thierry
    Shirmohammadi, Mahsa
    JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2019, 100 : 96 - 129
12345