On the complexity of resource-bounded logics
On the complexity of resource-bounded logics
复制标题
关于资源有限逻辑的复杂性
DOI：
10.1016/j.tcs.2018.01.019
复制
发表时间：
2018
影响因子：
1.1
通讯作者：
Alechina N
中科院分区：
文献类型：
--
作者：
Alechina N
为了建立（可决定的）模型检验问题的复杂性特征，我们重新审视了资源边界逻辑的可决定性结果，并将决策问题应用于有状态向量相加系统（VASS）。我们利用最近在交替VASS上的结果证明了逻辑RB±ATL的模型检查问题是2exptime-complete的（当资源数量有限时是inexptime）。此外，我们还证明了RBTL的模型检验问题是空间完备的。该问题是可决定的，并且对于RBTL具有相同的复杂性，证明了该方法的副产品是一个新的可决定性结果。当资源数量有限时，问题就在空间上。我们还建立了RB±ATL的模型检验问题，即RB±ATL的任意路径公式的扩展，可以通过对单侧VASS（交替VASS的一种变体）的奇偶对策的约简来确定。此外，我们能够合成资源参数的值。因此，本文建立了人工智能文献中所倡导的资源有界逻辑的模型检验问题与交替VASS的决策问题之间的形式对应关系，为更多的应用和相互融合铺平了道路。
We revisit decidability results for resource-bounded logics and use decision problems on vector addition systems with states (VASS) in order to establish complexity characterisations of (decidable) model checking problems. We show that the model checking problem for the logic RB±ATL is 2exptime-complete by using recent results on alternating VASS (and inexptimewhen the number of resources is bounded). Moreover, we establish that the model checking problem for RBTL isexpspace-complete. The problem is decidable and of the same complexity for RBTL⁎, proving a new decidability result as a by-product of the approach. When the number of resources is bounded, the problem is inpspace. We also establish that the model checking problem for RB±ATL⁎, the extension of RB±ATL with arbitrary path formulae, is decidable by a reduction to parity games for single-sided VASS (a variant of alternating VASS). Furthermore, we are able to synthesise values for resource parameters. Hence, the paper establishes formal correspondences between model checking problems for resource-bounded logics advocated in the AI literature and decision problems on alternating VASS, paving the way for more applications and cross-fertilizations.