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
关键词
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 条
  • [41] A decidable dense branching-time temporal logic
    La Torre, S
    Napoli, M
    FST TCS 2000: FOUNDATIONS OF SOFTWARE TECHNOLOGY AND THEORETICAL COMPUTER SCIENCE, PROCEEDINGS, 2000, 1974 : 139 - 150
  • [42] An extended branching-time ockhamist temporal logic
    Brown M.
    Goranko V.
    Journal of Logic, Language and Information, 1999, 8 (2) : 143 - 166
  • [43] Stochastic games with branching-time winning objectives
    Brazdil, Tomas
    Brozek, Vaclav
    Forejt, Vojtech
    Kucera, Antonin
    21ST ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2006, : 349 - +
  • [44] Comparative branching-time semantics for Markov chains
    Baier, C
    Katoen, JP
    Hermanns, H
    Wolf, V
    INFORMATION AND COMPUTATION, 2005, 200 (02) : 149 - 214
  • [45] Undivided and indistinguishable histories in branching-time logics
    Zanardo A.
    Journal of Logic, Language and Information, 1998, 7 (3) : 297 - 315
  • [46] ON THE WEAK ADEQUACY OF BRANCHING-TIME TEMPORAL LOGIC
    SCHNOEBELEN, P
    PINCHINAT, S
    LECTURE NOTES IN COMPUTER SCIENCE, 1990, 432 : 377 - 388
  • [47] The existence of finite abstractions for branching time model checking
    Dams, D
    Namjoshi, KS
    19TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2004, : 335 - 344
  • [48] Model checking for a probabilistic branching time logic with fairness
    Baier, C
    Kwiatkowska, M
    DISTRIBUTED COMPUTING, 1998, 11 (03) : 125 - 155
  • [49] Update and abstraction in model checking of knowledge and branching time
    Shilov, N. V.
    Garanina, N. O.
    Choe, K. -M.
    FUNDAMENTA INFORMATICAE, 2006, 72 (1-3) : 347 - 361
  • [50] EXPRESSIBILITY RESULTS FOR LINEAR-TIME AND BRANCHING-TIME LOGICS
    CLARKE, EM
    DRAGHICESCU, IA
    LECTURE NOTES IN COMPUTER SCIENCE, 1989, 354 : 428 - 437