Branching-time model-checking of probabilistic pushdown automata

被引：6
|
作者：
Brazdil, Tomas [1 ]
Brozek, Vaclav [1 ]
Forejt, Vojtech [2 ]
Kucera, Antonin [1 ]
机构：
[1] Masaryk Univ, Fac Informat, CS-60177 Brno, Czech Republic
[2] Univ Oxford, Dept Comp Sci, Oxford OX1 2JD, England
来源：
JOURNAL OF COMPUTER AND SYSTEM SCIENCES | 2014年 / 80卷 / 01期
关键词：
Probabilistic systems; Pushdown automata; Branching-time logics; Model-checking; REACHABILITY;
D O I：
10.1016/j.jcss.2013.07.001
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
In this paper we study the model-checking problem for probabilistic pushdown automata (pPDA) and branching-time probabilistic logics PCTL and PCTL*. We show that model-checking pPDA against general PCTL formulae is undecidable, but we yield positive decidability results for the qualitative fragments of PCTL and PCTL*. For these fragments, we also give a complete complexity classification. (C) 2013 Elsevier Inc. All rights reserved.
引用
收藏
页码：139 / 156
页数：18
相关论文
共 50 条
  • [31] Branching-Time Model Checking Gap-Order Constraint Systems
    Mayr, Richard
    Totzke, Patrick
    REACHABILITY PROBLEMS, 2013, 8169 : 171 - 182
  • [32] Branching-Time Model Checking Gap-Order Constraint Systems
    Mayr, Richard
    Totzke, Patrick
    FUNDAMENTA INFORMATICAE, 2016, 143 (3-4) : 339 - 353
  • [33] Robust model-checking of linear-time properties in timed automata
    Bouyer, P
    Markey, N
    Reynier, PA
    LATIN 2006: THEORETICAL INFORMATICS, 2006, 3887 : 238 - 249
  • [34] Probabilistic model-checking support for FMEA
    Grunske, Lars
    Colvin, Robert
    Winter, Kirsten
    FOURTH INTERNATIONAL CONFERENCE ON THE QUANTITATIVE EVALUATION OF SYSTEMS, 2007, : 119 - +
  • [35] On probabilistic pushdown automata
    Hromkovic, Juraj
    Schnitger, Georg
    INFORMATION AND COMPUTATION, 2010, 208 (08) : 982 - 995
  • [36] A linear-time branching-time perspective on interface automata
    Walter Vogler
    Gerald Lüttgen
    Acta Informatica, 2020, 57 : 513 - 550
  • [37] A linear-time branching-time perspective on interface automata
    Vogler, Walter
    Luettgen, Gerald
    ACTA INFORMATICA, 2020, 57 (3-5) : 513 - 550
  • [38] Parallel computational tree logic model-checking on pushdown systems
    Ye, Xin
    Shi, Jianqi
    Huang, Yanhong
    Li, Qin
    Wei, Hansheng
    Chen, Xinyu
    CONCURRENCY AND COMPUTATION-PRACTICE & EXPERIENCE, 2022, 34 (23):
  • [39] Model checking for a probabilistic branching time logic with fairness
    Baier, C
    Kwiatkowska, M
    DISTRIBUTED COMPUTING, 1998, 11 (03) : 125 - 155
  • [40] Model-checking timed automata with deadlines with Uppaal
    Gomez, Rodolfo
    FORMAL ASPECTS OF COMPUTING, 2013, 25 (02) : 289 - 318
12345