On the Complexity of Temporal-Logic Path Checking
On the Complexity of Temporal-Logic Path Checking
复制标题
论时间逻辑路径检查的复杂性
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Joël Ouaknine
中科院分区：
文献类型：
--
作者：
Daniel Bundala;Joël Ouaknine
在LTL或MTL等时态逻辑中，给定一个公式，一个基本问题是在给定的有限字上计算公式的复杂性。对于LTL，该任务的复杂性最近被证明是（mathsf{NC}^{}）[9]。本文给出了LTL的一个定量（或度量）扩展MTL的（mathsf{NC}^{}）算法和LTL的一元片段UTL的（mathsf{AC}^{1}）算法。在撰写本文时，MTL是具有（mathsf{NC}^{}）路径检查算法的最具表达力的逻辑，UTL是LTL的最具表达力的片段，其路径检查算法比完整的LTL更有效（服从标准复杂性理论假设）。然后，我们建立LTL路径检查和平面电路之间的连接，我们利用它来表明，在确定LTL路径检查的精确复杂性的任何进一步的进展将立即需要更有效的评估算法比已知的某一类平面电路。这种连接进一步暗示了LTL路径检查的复杂性取决于所允许的布尔连接词：添加布尔异或产生一个具有P-完全路径检查问题的时态逻辑。
Given a formula in a temporal logic such as LTL or MTL, a fundamental problem is the complexity of evaluating the formula on a given finite word. For LTL, the complexity of this task was recently shown to be in (mathsf{NC}^{} ) [9]. In this paper, we present an (mathsf{NC}^{} ) algorithm for MTL, a quantitative (or metric) extension of LTL, and give an (mathsf{AC}^{1} ) algorithm for UTL, the unary fragment of LTL. At the time of writing, MTL is the most expressive logic with an (mathsf{NC}^{} ) path-checking algorithm, and UTL is the most expressive fragment of LTL with a more efficient path-checking algorithm than for full LTL (subject to standard complexity-theoretic assumptions). We then establish a connection between LTL path checking and planar circuits, which we exploit to show that any further progress in determining the precise complexity of LTL path checking would immediately entail more efficient evaluation algorithms than are known for a certain class of planar circuits. The connection further implies that the complexity of LTL path checking depends on the Boolean connectives allowed: adding Boolean exclusive or yields a temporal logic with P-complete path-checking problem.
LTL 路径检查可高效并行化
DOI：
10.1007/978-3-642-02930-1_20
发表时间：
2009
期刊：
影响因子：
--
作者：
Lars Kuhtz;Bernd Finkbeiner
通讯作者：
Bernd Finkbeiner