On the Complexity of Model-Checking Branching and Alternating-Time Temporal Logics in One-Counter Systems

被引：5
|
作者：
Vester, Steen [1 ]
机构：
[1] Tech Univ Denmark, DK-2800 Lyngby, Denmark
来源：
AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2015 | 2015年 / 9364卷
关键词：
AUTOMATA; GAMES;
D O I：
10.1007/978-3-319-24953-7_27
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
We study the complexity of the model-checking problem for the branching-time logic CTL* and the alternating-time temporal logics ATL/ATL* in one-counter processes and one-counter games respectively. The complexity is determined for all three logics when integer weights are input in unary (non-succinct) and binary (succinct) as well as when the input formula is fixed and is a parameter. Further, we show that deciding the winner in one-counter games with LTL objectives is 2ExpSpacecomplete for both succinct and non-succinct games. We show that all the problems considered stay in the same complexity classes when we add quantitative constraints that can compare the current value of the counter with a constant.
引用
收藏
页码：361 / 377
页数：17
相关论文
共 50 条
  • [41] On the model checking problem for branching time logics and Basic Parallel Processes
    Esparza, J
    Kiehn, A
    COMPUTER AIDED VERIFICATION, 1995, 939 : 353 - 366
  • [42] Alternating-time Temporal Belief and Knowledge Logic in Multi-agent Systems
    Ning, Zhengyuan
    Lai, Xianwei
    Hu, Shanli
    Wang, Xiuli
    2008 3RD INTERNATIONAL CONFERENCE ON INTELLIGENT SYSTEM AND KNOWLEDGE ENGINEERING, VOLS 1 AND 2, 2008, : 1357 - +
  • [43] A POLYNOMIAL-TIME ALGORITHM FOR CHECKING THE INCLUSION FOR STRICT DETERMINISTIC RESTRICTED ONE-COUNTER AUTOMATA
    HIGUCHI, K
    TOMITA, E
    WAKATSUKI, M
    IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 1995, E78D (04) : 305 - 313
  • [44] Kronos: A model-checking tool for real-time systems
    Bozga, M
    Daws, C
    Maler, O
    Olivero, A
    Tripakis, S
    Yovine, S
    COMPUTER AIDED VERIFICATION, 1998, 1427 : 546 - 550
  • [45] Complexity results on branching-time pushdown model checking
    Bozzelli, L
    VERIFICATION, MODEL CHECKING , AND ABSTRACT INTERPRETATION, PROCEEDINGS, 2006, 3855 : 65 - 79
  • [46] Model-Checking Temporal Properties of Real-Time HTL Programs
    Carvalho, Andre
    Carvalho, Joel
    Pinto, Jorge Sousa
    de Sousa, Simao Melo
    LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION, AND VALIDATION, PT II, 2010, 6416 : 191 - +
  • [47] Complexity results on branching-time pushdown model checking
    Bozzelli, Laura
    THEORETICAL COMPUTER SCIENCE, 2007, 379 (1-2) : 286 - 297
  • [48] The Complexity of Epistemic Model Checking: Clock Semantics and Branching Time
    Huang, X.
    van der Meyden, R.
    ECAI 2010 - 19TH EUROPEAN CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2010, 215 : 549 - 554
  • [49] Branching-Time Temporal Logics with Minimal Model Quantifiers
    Mogavero, Fabio
    Murano, Aniello
    DEVELOPMENTS IN LANGUAGE THEORY, PROCEEDINGS, 2009, 5583 : 396 - 409
  • [50] Model-Checking Linear-Time Properties of Quantum Systems
    Ying, Mingsheng
    Li, Yangjia
    Yu, Nengkun
    Feng, Yuan
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2014, 15 (03)
12345