Temporal logics over linear time domains are in PSPACE

被引:2
|
作者
Rabinovich, Alexander [1 ]
机构
[1] Tel Aviv Univ, Blavatnik Sch Comp Sci, IL-69978 Tel Aviv, Israel
关键词
COMPLEXITY; ORDERINGS; AUTOMATA; WORDS;
D O I
10.1016/j.ic.2011.11.002
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We investigate the complexity of the satisfiability problem of temporal logics with a finite set of modalities definable in the existential fragment of monadic second-order logic. We show that the problem is in PSPACE over the class of all linear orders. The same techniques show that the problem is in PSPACE over many interesting classes of linear orders. (C) 2011 Elsevier Inc. All rights reserved.
引用
收藏
页码:40 / 67
页数:28
相关论文
共 50 条
  • [1] Temporal Logics over Linear Time Domains Are in PSPACE
    Rabinovich, Alexander
    [J]. REACHABILITY PROBLEMS, 2010, 6227 : 29 - 50
  • [2] Quantitative temporal logics over the reals: PSPACE and below
    Lutz, Carsten
    Walther, Dirk
    Wolter, Frank
    [J]. INFORMATION AND COMPUTATION, 2007, 205 (01) : 99 - 123
  • [3] Linear time Temporal Logics over Mazurkiewicz traces
    Mukund, M
    Thiagarajan, PS
    [J]. MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 1996, 1996, 1113 : 62 - 92
  • [4] Uniform satistiability in PSPACE for local temporal logics over Mazurkiewicz traces
    Gastin, Paul
    Kuske, Dietrich
    [J]. FUNDAMENTA INFORMATICAE, 2007, 80 (1-3) : 169 - 197
  • [5] Quantitative temporal logics: PSPACE and below
    Lutz, C
    Walther, D
    Wolter, F
    [J]. 12TH INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING, PROCEEDINGS, 2005, : 138 - 146
  • [6] Complete and tractable local linear time temporal logics over traces
    Adsul, B
    Sohoni, M
    [J]. AUTOMATA, LANGUAGES AND PROGRAMMING, 2002, 2380 : 926 - 937
  • [7] COMPARING LINEAR AND BRANCHING TIME TEMPORAL LOGICS
    STIRLING, C
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1989, 398 : 1 - 20
  • [8] COMPARING LINEAR AND BRANCHING TIME TEMPORAL LOGICS
    STIRLING, C
    [J]. TEMPORAL LOGIC IN SPECIFICATION, 1989, 398 : 1 - 20
  • [9] Satisfiability and model checking for MSO-definable temporal logics are in PSPACE
    Gastin, P
    Kuske, D
    [J]. CONCUR 2003 - CONCURRENCY THEORY, 2003, 2761 : 222 - 236
  • [10] Alternating-time temporal logics with linear past
    Bozzelli, Laura
    Murano, Aniello
    Sorrentino, Loredana
    [J]. THEORETICAL COMPUTER SCIENCE, 2020, 813 : 199 - 217