On temporal logics with data variable quantifications: Decidability and complexity
On temporal logics with data variable quantifications: Decidability and complexity
复制标题
关于具有数据变量量化的时态逻辑：可判定性和复杂性
DOI：
10.1016/j.ic.2016.08.002
复制
发表时间：
2016-12
影响因子：
1
通讯作者：
Zhilin Wu
中科院分区：
文献类型：
--
作者：
Fu Song;Zhilin Wu
虽然几乎每个计算机系统中都有数据值，但由于数据量巨大，甚至是无限的数据域，对数据值进行推理是一项具有挑战性的任务。时序逻辑是众所周知的反应式和并发性系统的规格说明形式化。时态逻辑的各种扩展被提出来推理数据值，主要是在过去的十年里。其中，一个自然的想法是在无限的数据域上扩展具有可变量化的时态逻辑。Grumberg，Kupferman和Sheinvald最近开始了对这一主题的研究，并获得了一些有趣的结果。然而，关于时态逻辑变量外延的理论方面还缺乏系统的研究。我们在这篇论文中的目标是填补这一空白。围绕这一目标，我们做出了以下选择：1.我们考虑了两种广泛使用的时态逻辑--线性时态逻辑(LTL)和计算树逻辑(CTL)的变量扩展，允许用布尔算子和时态算子对变量量化进行任意嵌套(所得到的逻辑分别称为Variable-LTL，简称VLTL和Variable-CTL，简称VCTL)。2.研究了可满足性问题和模型检测问题在有限词(树)和无限词(树)上的可判定性和复杂性。特别地，我们得到了以下结果：存在变量量词或开头只有一个全称量词的VLTL和VCTL在有限和无限字(树)上的可满足性问题已经是不可判定的；如果在VCTL中只使用存在路径量词，那么(在有限树上)可满足性问题是可判定的，无论哪个变量可用；对于开头只有一个全称量词的VLTL公式，如果非参数原子命题的出现被量化变量的正出现所保护，那么它的可满足性问题就变成了可判定的；基于可满足性问题的这些结果，我们推导出模型检验问题的(不可判定)结果。
Although data values are available in almost every computer system, reasoning about them is a challenging task due to the huge data size or even infinite data domains. Temporal logics are the well-known specification formalisms for reactive and concurrent systems. Various extensions of temporal logics have been proposed to reason about data values, mostly in the last decade. Among them, one natural idea is to extend temporal logics with variable quantifications ranging over an infinite data domain. Grumberg, Kupferman and Sheinvald initiated the research on this topic recently and obtained several interesting results. However, there is still a lack of systematic investigation on the theoretical aspects of the variable extensions of temporal logics. Our goal in this paper is to fill this gap. Around this goal, we make the following choices: 1. We consider the variable extensions of two widely used temporal logics, Linear Temporal Logic (LTL) and Computation Tree Logic (CTL), and allow arbitrary nestings of variable quantifications with Boolean and temporal operators (the resulting logics are called respectively variable-LTL, in brief VLTL, and variable-CTL, in brief VCTL). 2. We investigate the decidability and complexity of both the satisfiability and model checking problems, over both finite and infinite words (trees). In particular, we obtain the following results: Existential variable quantifiers or one single universal quantifier in the beginning already entail the undecidability of the satisfiability problems of both VLTL and VCTL, over both finite and infinite words (trees); if only existential path quantifiers are used in VCTL, then the satisfiability problem (over finite trees) is decidable, no matter which variable quantifiers are available; for VLTL formulae with one single universal variable quantifier in the beginning, if the occurrences of the non-parameterized atomic propositions are guarded by the positive occurrences of the quantified variables, then its satisfiability problem becomes decidable, over both finite and infinite words; based on these results of the satisfiability problem, we deduce the (un)decidability results of the model checking problem.
登录
查看更多内容
DOI：
10.1016/0304-3975(86)90157-x
发表时间：
1986-11
期刊：
Theor. Comput. Sci.
影响因子：
--
作者：
A. Szałas
通讯作者：
A. Szałas
DOI：
10.1007/978-3-642-03816-7_60
发表时间：
2009-08
期刊：
Inf. Comput.
影响因子：
--
作者：
Tony Tan
通讯作者：
Tony Tan
DOI：
10.1145/2287718.2287727
发表时间：
2009-09
期刊：
--
影响因子：
--
作者：
R. Alur;Pavol Cerný;S. Weinstein
通讯作者：
R. Alur;Pavol Cerný;S. Weinstein
影响因子：
--
作者：
A. Kara;T. Schwentick;Tony Tan
通讯作者：
A. Kara;T. Schwentick;Tony Tan
DOI：
10.1145/2499937.2499940
发表时间：
2009-08
期刊：
2009 24th Annual IEEE Symposium on Logic In Computer Science
影响因子：
--
作者：
Tony Tan
通讯作者：
Tony Tan