On temporal logics with data variable quantifications: Decidability and complexity

doi:10.1016/j.ic.2016.08.002

	On temporal logics with data variable quantifications: Decidability and complexity
	Song, Fu1,2 ; Wu, Zhilin 3,4
	2016-12
发表期刊	INFORMATION AND COMPUTATION (IF:0.8[JCR-2023],0.9[5-Year])
ISSN	0890-5401
卷号	251 页码:104-139
发表状态	已发表
DOI	10.1016/j.ic.2016.08.002
摘要	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. (C) 2016 Elsevier Inc. All rights reserved.
关键词	Temporal logics Data variable quantifications Satisfiability Model checking Decidability and complexity Alternating register automata Data automata
收录类别	SCI ; EI
语种	英语
资助项目	Open Project of Shanghai Key Laboratory of Trustworthy Computing[07dz22304201404]
WOS研究方向	Computer Science ; Mathematics
WOS类目	Computer Science, Theory & Methods ; Mathematics, Applied
WOS记录号	WOS:000388548000006
出版者	ACADEMIC PRESS INC ELSEVIER SCIENCE
EI入藏号	20164803052735
EI主题词	Automata theory ; Computability and decidability ; Forestry ; Formal logic ; Model checking
WOS关键词	AUTOMATA-THEORETIC APPROACH ; FRAGMENTS
原始文献类型	Article
引用统计	正在获取...
文献类型	期刊论文
条目标识符	https://kms.shanghaitech.edu.cn/handle/2MSLDSTB/1625
专题	信息科学与技术学院_PI研究组_宋富组
通讯作者	Wu, Zhilin
作者单位	1.ShanghaiTech Univ, Sch Informat Sci & Technol, Shanghai, Peoples R China 2.East China Normal Univ, Natl Trusted Embedded Software Engn Tedmol Res Ct, Shanghai Key Lab Trustworthy Comp, Shanghai, Peoples R China 3.Chinese Acad Sci, Inst Software, State Key Lab Comp Sci, Beijing 100864, Peoples R China 4.Univ Paris Diderot, LIAFA, Paris, France
第一作者单位	信息科学与技术学院
第一作者的第一单位	信息科学与技术学院
推荐引用方式 GB/T 7714	Song, Fu,Wu, Zhilin. On temporal logics with data variable quantifications: Decidability and complexity[J]. INFORMATION AND COMPUTATION,2016,251:104-139.
APA	Song, Fu,&Wu, Zhilin.(2016).On temporal logics with data variable quantifications: Decidability and complexity.INFORMATION AND COMPUTATION,251,104-139.
MLA	Song, Fu,et al."On temporal logics with data variable quantifications: Decidability and complexity".INFORMATION AND COMPUTATION 251(2016):104-139.