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 条
  • [1] Model checking for hybrid branching-time logics
    Kernberger, Daniel
    Lange, Martin
    JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2020, 110
  • [2] Strategies, model checking and branching-time properties in Maude
    Rubio, Ruben
    Marti-Oliet, Narciso
    Pita, Isabel
    Verdejo, Alberto
    JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2021, 123
  • [3] Strategies, Model Checking and Branching-Time Properties in Maude
    Rubio, Ruben
    Marti-Oliet, Narciso
    Pita, Isabel
    Verdejo, Alberto
    REWRITING LOGIC AND ITS APPLICATIONS, WRLA 2020, 2020, 12328 : 156 - 175
  • [4] Complexity results on branching-time pushdown model checking
    Bozzelli, L
    VERIFICATION, MODEL CHECKING , AND ABSTRACT INTERPRETATION, PROCEEDINGS, 2006, 3855 : 65 - 79
  • [5] Bounded model checking for branching-time temporal logic
    Zhou Conghua
    Tao Zhihong
    Ding Decheng
    Wang Lifu
    CHINESE JOURNAL OF ELECTRONICS, 2006, 15 (04): : 675 - 678
  • [6] Complexity results on branching-time pushdown model checking
    Bozzelli, Laura
    THEORETICAL COMPUTER SCIENCE, 2007, 379 (1-2) : 286 - 297
  • [7] Branching-time model-checking of probabilistic pushdown automata
    Brazdil, Tomas
    Brozek, Vaclav
    Forejt, Vojtech
    Kucera, Antonin
    JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2014, 80 (01) : 139 - 156
  • [8] 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
  • [9] Branching-Time Model-Checking of Probabilistic Pushdown Automata
    Brazdil, Tomas
    Brozek, Vaclav
    Forejt, Vojtech
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 239 (0C) : 73 - 83
  • [10] An automata-theoretic approach to branching-time model checking
    Kupferman, O
    Vardi, MY
    Wolper, P
    JOURNAL OF THE ACM, 2000, 47 (02) : 312 - 360
12345