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 条

[41] Model-checking hierarchical structures
Lohrey, Markus
JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2012, 78 (02) : 461 - 490
[42] Model-checking algorithms for continuous-time Markov chains
Baier, C
Haverkort, B
Hermanns, H
Katoen, JP
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2003, 29 (06) : 524 - 541
[43] On the expressive power of hybrid branching-time logics
Kernberger, Daniel
Lange, Martin
THEORETICAL COMPUTER SCIENCE, 2020, 813 : 362 - 374
[44] Model checking dynamic pushdown networks
Song, Fu
Touili, Tayssir
FORMAL ASPECTS OF COMPUTING, 2015, 27 (02) : 397 - 421
[45] Model-Checking Linear-Time Properties of Quantum Systems
Ying, Mingsheng
Li, Yangjia
Yu, Nengkun
Feng, Yuan
ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2014, 15 (03)
[46] Model Checking of Recursive Probabilistic Systems
Etessami, Kousha
Yannakakis, Mihalis
ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2012, 13 (02)
[47] Probabilistic Model Checking
Baier, Christel
DEPENDABLE SOFTWARE SYSTEMS ENGINEERING, 2016, 45 : 1 - 23
[48] Verifying Business Rules Using Model-Checking Techniques for Non-specialist in Model-Checking
Aoki, Yoshitaka
Matsuura, Saeko
IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 2014, E97D (05) : 1097 - 1108
[49] Pushdown model checking for malware detection
Song, Fu
Touili, Tayssir
INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2014, 16 (02) : 147 - 173
[50] Reduction from Branching-Time Property Verification of Higher-Order Programs to HFL Validity Checking
Watanabe, Keiichi
Tsukada, Takeshi
Oshikawa, Hiroki
Kobayashi, Naoki
PROCEEDINGS OF THE 2019 ACM SIGPLAN WORKSHOP ON PARTIAL EVALUATION AND PROGRAM MANIPULATION (PEPM '19), 2019, : 22 - 34

← 1 2 3 4 5 →