Oracle Circuits for Branching-Time Model Checking

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.

• Type: Conference
• Year: 2003
• Where: ICALP
• Authors: Ph. Schnoebelen
• Keywords: Deterministic Polynomial-time, ICALP 2003, Oracle Circuits, Precise Computational Complexity, Theoretical Computer Science