Oracle Circuits for Branching-Time Model Checking
Oracle Circuits for Branching-Time Model Checking
复制标题
用于分支时间模型检查的 Oracle 电路
DOI：
--
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
P. Schnoebelen
中科院分区：
文献类型：
--
作者：
P. Schnoebelen
介绍了一类特殊的树向量形式的预言电路。结果表明，它们可以通过对 NP 预言机的自适应查询的多对数数量在确定性多项式时间内进行评估。该框架使我们能够评估某些分支时间逻辑的模型检查的精确计算复杂性，其中已知问题是 NP 困难和 coNP 困难。
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.