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 条

[21] BRANCHING-TIME MODEL CHECKING OF ONE-COUNTER PROCESSES
Goeller, Stefan
Lohrey, Markus
27TH INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF COMPUTER SCIENCE (STACS 2010), 2010, 5 : 405 - 416
[22] MODEL-CHECKING FOR PROBABILISTIC REAL-TIME SYSTEMS
ALUR, R
COURCOUBETIS, C
DILL, D
LECTURE NOTES IN COMPUTER SCIENCE, 1991, 510 : 115 - 126
[23] Branching-time temporal logic and tree automata
Kupferman, O
Grumberg, O
INFORMATION AND COMPUTATION, 1996, 125 (01) : 62 - 69
[24] Extending Co-logic Programs for Branching-Time Model Checking
Seki, Hirohisa
LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION, LOPSTR 2013, 2014, 8901 : 127 - 144
[25] Budget-bounded model-checking pushdown systems
Parosh Aziz Abdulla
Mohamed Faouzi Atig
Othmane Rezine
Jari Stenman
Formal Methods in System Design, 2014, 45 : 273 - 301
[26] Budget-bounded model-checking pushdown systems
Abdulla, Parosh Aziz
Atig, Mohamed Faouzi
Rezine, Othmane
Stenman, Jari
FORMAL METHODS IN SYSTEM DESIGN, 2014, 45 (02) : 273 - 301
[27] Efficient Parallel CTL Model-Checking for Pushdown Systems
Chen, Xinyu
Wei, Hansheng
Ye, Xin
Hao, Li
Huang, Yanhong
Shi, Jianqi
2018 IEEE INT CONF ON PARALLEL & DISTRIBUTED PROCESSING WITH APPLICATIONS, UBIQUITOUS COMPUTING & COMMUNICATIONS, BIG DATA & CLOUD COMPUTING, SOCIAL COMPUTING & NETWORKING, SUSTAINABLE COMPUTING & COMMUNICATIONS, 2018, : 23 - 30
[28] Model-checking for weighted timed automata
Brihaye, T
Bruyère, V
Raskin, JF
FORMAL TECHNIQUES, MODELLING AND ANALYSIS OF TIMED AND FAULT-TOLERANT SYSTEMS, PROCEEDINGS, 2004, 3253 : 277 - 292
[29] Efficient Model Checking for Duration Calculus Based on Branching-Time Approximations
Fraenzle, Martin
Hansen, Michael R.
SEFM 2008: SIXTH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, PROCEEDINGS, 2008, : 63 - +
[30] Model Checking Games for a Fair Branching-Time Temporal Epistemic Logic
Huang, Xiaowei
van der Meyden, Ron
AI 2009: ADVANCES IN ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2009, 5866 : 11 - 20

← 1 2 3 4 5 →