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). |
个性服务 |
查看访问统计 |
相关权益政策 |
暂无数据 |
收藏/分享 |
除非特别说明,本系统中所有内容都受版权保护,并保留所有权利。
修改评论