Model checking computation tree logic over finite lattices

doi:10.1016/j.tcs.2015.10.014

CORC > 北京大学 > 信息科学技术学院

	Model checking computation tree logic over finite lattices
	Pan, Haiyu ; Li, Yongming ; Cao, Yongzhi ; Ma, Zhanyou
刊名	THEORETICAL COMPUTER SCIENCE
	2016
关键词	Model checking Computation tree logic Lattice Weighted automata QUANTUM LOGIC MULTIVALUED LOGICS AUTOMATA TIME
DOI	10.1016/j.tcs.2015.10.014
英文摘要	Multi-valued model-checking is an extension of classical model-checking used to verify the properties of systems with uncertain information content. It is used in systems where the semantic domain of both the models of the systems and the specification is a De Morgan algebra or more abstract structure such as semirings. A common feature of De Morgan algebras and semirings is that they satisfy the distributive law, which is crucial for all of the multi-valued model-checking algorithms developed so far. In this paper, we study computation tree logic with membership values in a finite lattice, which are called multi-valued computation tree logic (MCTL). We introduce three semantics for MCTL over the multi-valued Kripke structure: path semantics, fixpoint semantics, and algebraic semantics, and prove that they coincide if and only if the underlying lattice is distributive. Furthermore, we provide model-checking algorithms with respect to the three semantics. Our algorithms show that MCTL model-checking problems with respect to the fixpoint and algebraic semantics can be solved in polynomial time in the size of the state space of the multi-valued Kripke structure, the size of the lattice, and the length of the formula, while MCTL model-checking problem with respect to the path semantics is in PSPACE. We also provide a lower bound for the MCTL model-checking problem with respect to the path semantics. (C) 2015 Elsevier B.V. All rights reserved.; National Natural Science Foundation of China [11271237, 61228305, 61370053, 11401361]; Higher School Doctoral Subject Foundation of Ministry of Education of the People's Republic of China [20130202110001]; China Postdoctoral Science Foundation [2014M552408]; SCI(E); EI; ARTICLE; phyu76@126.com; liyongm@snnu.edu.cn; caoyz@pku.edu.cn; mazhany@126.com; 45-62; 612
语种	英语
内容类型	期刊论文
源URL	[http://ir.pku.edu.cn/handle/20.500.11897/437793]
专题	信息科学技术学院
推荐引用方式 GB/T 7714	Pan, Haiyu,Li, Yongming,Cao, Yongzhi,et al. Model checking computation tree logic over finite lattices[J]. THEORETICAL COMPUTER SCIENCE,2016.
APA	Pan, Haiyu,Li, Yongming,Cao, Yongzhi,&Ma, Zhanyou.(2016).Model checking computation tree logic over finite lattices.THEORETICAL COMPUTER SCIENCE.
MLA	Pan, Haiyu,et al."Model checking computation tree logic over finite lattices".THEORETICAL COMPUTER SCIENCE (2016).