Oracle circuits for branching-time model checking

被引：0
|
作者：
Schnoebelen, P
机构：
[1] ENS Cachan, Lab Specificat & Verificat, F-94235 Cachan, France
[2] CNRS, UMR 8643, F-94235 Cachan, France
来源：
AUTOMATA, LANGUAGES AND PROGRAMMING, PROCEEDINGS | 2003年 / 2719卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
A special class of oracle circuits with tree-vector form is introduced. It is shown that they can be evaluated in deterministic polynomial-time with a polylog number of adaptive queries to an NP oracle. This framework allows us to evaluate the precise computational complexity of model checking for some branching-time logics where it was known that the problem is NP-hard and coNP-hard.
引用
收藏
页码：790 / 801
页数：12
相关论文
共 50 条
  • [31] On the expressive power of hybrid branching-time logics
    Kernberger, Daniel
    Lange, Martin
    THEORETICAL COMPUTER SCIENCE, 2020, 813 : 362 - 374
  • [32] Satisfying a fragment of XQuery by branching-time reduction
    Halle, Sylvain
    Villemaire, Roger
    TIME 2008: 15TH INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING, PROCEEDINGS, 2008, : 72 - 76
  • [33] Completeness of a Branching-Time Logic with Possible Choices
    Roberto Ciuni
    Alberto Zanardo
    Studia Logica, 2010, 96 : 393 - 420
  • [34] Model checking games for branching time logics
    Lange, Martin
    Stirling, Colin
    Journal of Logic and Computation, 2002, 12 (04) : 623 - 639
  • [35] Branching-time logics repeatedly referring to states
    Weber V.
    Journal of Logic, Language and Information, 2009, 18 (4) : 593 - 624
  • [36] Completeness of a Branching-Time Logic with Possible Choices
    Ciuni, Roberto
    Zanardo, Alberto
    STUDIA LOGICA, 2010, 96 (03) : 393 - 420
  • [37] 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
  • [38] Branching-time temporal logic and tree automata
    Kupferman, O
    Grumberg, O
    INFORMATION AND COMPUTATION, 1996, 125 (01) : 62 - 69
  • [39] Which branching-time properties are effectively linear?
    Grumberg, O
    Kurshan, RP
    JOURNAL OF LOGIC AND COMPUTATION, 2001, 11 (02) : 201 - 228
  • [40] Cactus: A branching-time logic programming language
    Rondogiannis, P
    Gergatsoulis, M
    Panayiotopoulos, T
    QUALITATIVE AND QUANTITATIVE PRACTICAL REASONING, 1997, 1244 : 511 - 524
12345