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 条
  • [1] Branching-Time Model-Checking of Probabilistic Pushdown Automata
    Brazdil, Tomas
    Brozek, Vaclav
    Forejt, Vojtech
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 239 (0C) : 73 - 83
  • [2] Complexity results on branching-time pushdown model checking
    Bozzelli, Laura
    THEORETICAL COMPUTER SCIENCE, 2007, 379 (1-2) : 286 - 297
  • [3] Complexity results on branching-time pushdown model checking
    Bozzelli, L
    VERIFICATION, MODEL CHECKING , AND ABSTRACT INTERPRETATION, PROCEEDINGS, 2006, 3855 : 65 - 79
  • [4] Model checking probabilistic pushdown automata
    Esparza, J
    Kucera, A
    Mayr, R
    19TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2004, : 12 - 21
  • [5] MODEL CHECKING PROBABILISTIC PUSHDOWN AUTOMATA
    Esparza, Javier
    Kucera, Antonin
    Mayr, Richard
    LOGICAL METHODS IN COMPUTER SCIENCE, 2006, 2 (01)
  • [6] An automata-theoretic approach to branching-time model checking
    Kupferman, O
    Vardi, MY
    Wolper, P
    JOURNAL OF THE ACM, 2000, 47 (02) : 312 - 360
  • [7] MODEL-CHECKING OF ORDERED MULTI-PUSHDOWN AUTOMATA
    Atig, Mohamed Faouzi
    LOGICAL METHODS IN COMPUTER SCIENCE, 2012, 8 (03)
  • [8] Reachability analysis of pushdown automata: Application to model-checking
    Bouajjani, A
    Esparza, J
    Maler, O
    CONCUR'97 : CONCURRENCY THEORY, 1997, 1243 : 135 - 150
  • [9] Branching-Time Model Checking of Parametric One-Counter Automata
    Goeller, Stefan
    Haase, Christoph
    Ouaknine, Joel
    Worrell, James
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATIONAL STRUCTURES, FOSSACS 2012, 2012, 7213 : 406 - 420
  • [10] BRANCHING-TIME MODEL CHECKING OF ONE-COUNTER PROCESSES AND TIMED AUTOMATA
    Goeller, Stefan
    Lohrey, Markus
    SIAM JOURNAL ON COMPUTING, 2013, 42 (03) : 884 - 923
12345