导读:本文包含了计算树逻辑论文开题报告文献综述及选题提纲参考文献，主要关键词:模型检测,计算树逻辑,DNA分子,分子计算
计算树逻辑论文文献综述
韩英杰,周清雷,朱维军[1]（2019）在《基于DNA计算的计算树逻辑模型检测方法研究进展》一文中研究指出计算树逻辑(CTL)模型检测是保证系统正确性和可靠性的重要手段,但严峻的时空复杂性问题制约着CTL模型检测在工业界的应用。DNA计算的大规模并行性和DNA分子巨大的存储密度为解决CTL模型检测的时空复杂性问题提供了新思路。文中介绍了基于DNA计算的CTL模型检测的背景,并概述了基于DNA计算的CTL模型检测方法的基本原理。从检测能力的提升、自治化程度的提升和相关问题的解决这3个方面综述了方法的研究进展。在方法检测能力的提升方面,分3个层次综述了研究进展,即从只能检测单个CTL基本公式到能够检测一般公式,从只能检测带未来时间算子的CTL公式到能够检测带过去时间算子的CTL公式,从只能检测CTL公式到能够检测线性时序逻辑、投影时序逻辑和区间时序逻辑公式,表明了方法的检测能力在公式数量和种类上均有大幅提升;在方法自治化程度的提升方面,综述了从基于无记忆过滤模型的人工操作的非自治方法到基于粘贴自动机的分子自治下的自治方法的研究进展,表明基于DNA计算的CTL模型检测方法已实现高度自治化;在相关问题的解决方面,阐述了提升DNA分子特异性杂交有效性预测的效率和构建CTL公式的DNA表示等的研究进展。最后,指出了基于DNA计算的CTL模型检测在研究新方法、构建专用的DNA计算模型和扩展应用领域等方面的研究趋势。(本文来源于《计算机科学》期刊2019年11期）
袁申,魏杰林,李永明[2]（2019）在《具有多值决策过程的广义可能性计算树逻辑模型检测》一文中研究指出模型检测是一种自动验证软硬件系统行为的有效技术。为了对包含非确定性信息、不一致信息的并发系统进行形式化验证,在可能性理论、多值逻辑的基础上,研究了具有多值决策过程的广义可能性多值计算树逻辑模型检测算法,及其在检验非确定性系统中的具体应用。首先构造了多值决策过程作为系统模型,用多值计算树逻辑描述系统属性。然后给出具有多值决策过程的广义可能性多值计算树逻辑的模型检测算法,该算法将模型检测的具体问题转换为多项式时间内的模糊矩阵运算。最后就包含非确定性选择的多值系统的模型检测问题,给出一个具体的应用实例。(本文来源于《计算机工程与科学》期刊2019年01期）
范艳焕,李永明,潘海玉[3]（2018）在《不确定型模糊Kripke结构的计算树逻辑模型检测》一文中研究指出本文研究了不确定型模糊Kripke结构的计算树逻辑的模型检测问题,并说明了该问题可以在对数多形式时间内解决.首先给出了不确定型模糊Kripke结构的定义,引入了模糊计算树逻辑的语法和语义.为了刻画存在量词?和任意量词在不确定型模糊Kripke结构中的两种语义解释,在模糊计算树逻辑语法中引入了路径量词?_(sup),?_(inf)和_(sup),_(inf),分别用于替换存在量词?和任意量词.其次讨论了基于不确定型模糊Kripke结构的计算树逻辑模型检测算法,特别地对于模糊计算树逻辑公式?_(sup)pUq,_(sup)pUq,?_(inf)pUq和_(inf)pUq分别给出时间复杂度为对数多项式时间的改进算法.(本文来源于《电子学报》期刊2018年01期）
梁常建,李永明[4]（2017）在《广义可能性计算树逻辑的模型检测问题》一文中研究指出本文首先分别给出了"约束可达","总是可达"这两个公式在广义可能性计算树逻辑(GPo CTL)中的另外两种等价形式;其次讨论了基于广义可能性测度的计算树逻辑的模型检测问题,将GPo CTL的模型检测问题规约为经典的CTL模型检测问题,利用截集的方法,给出了计算GPo CTL的模型检测问题的算法及其复杂度,并通过实例分析说明了这种算法的可行性;最后,研究了具有公平性假设的GPo CTL模型检测问题的计算复杂度,得到了与上面相似的结论.(本文来源于《电子学报》期刊2017年11期）
李丹[5]（2017）在《广义可能性计算树逻辑表达能力的研究》一文中研究指出为了解决复杂计算机系统的验证问题,确保系统的正确性与可靠性,人们提出了模型检测方法.该方法于1981年首次被Clark和Emerson提出,是一种形式化的自动验证技术,其验证能够贯穿系统开发的整个过程,此方法主要分为以下叁个过程:首先,抽象出系统的数学模型;其次,形式化描述需要验证的属性;最后,通过模型检测算法验证系统是否满足该属性,若满足将返回是;若不满足将给出一个反例.经典的模型检测只是针对完全确定的系统,但现实中却很少存在这样的系统.于是,人们开始考虑将量化信息引入到状态迁移模型中,比如:概率、多值、时间和可能性等.为了解决具有模糊性系统的验证问题,李永明将可能性测度和模型检测相结合,提出了基于可能性测度的模型检测理论.为了处理更一般的不确定性问题,李永明将可能性测度拓展为广义可能性测度,并结合模型检测,提出了基于广义可能性测度的模型检测理论.由于研究逻辑公式间的表达能力对拓广模型检测的适用范围具有重要意义,但目前对广义可能性计算树逻辑的表达能力还尚未研究全面.本文是在前面工作的基础上,以有限的广义可能性Kripke结构为模型,研究广义可能性计算树逻辑与计算树逻辑表达能力的关系,并以有限的强广义可能性Kripke结构为模型,研究广义可能性计算树逻辑与可能性计算树逻辑表达能力的关系.本文主要工作如下:1.定义了区间广义可能性计算树逻辑的语构和语义.2.以有限的广义可能性Kripke结构为模型,给出区间广义可能性计算树逻辑公式和计算树逻辑公式等价关系的定义,通过归纳法和反证法得出:计算树逻辑是区间广义可能性计算树逻辑的一个真子类,然后得出计算树逻辑公式转化为区间广义可能性计算树逻辑公式的算法.3.定义了强广义可能性Kripke结构,并以有限的强广义可能性Kripke结构为模型,给出区间广义可能性计算树逻辑公式和可能性计算树逻辑公式等价关系的定义,通过归纳法和反证法得出:可能性计算树逻辑是区间广义可能性计算树逻辑的一个真子类,然后得出可能性计算树逻辑公式转化为区间广义可能性计算树逻辑公式的算法.4.对前面等价关系的定义进行拓展,给出相应公式间等价关系的另一种定义.(本文来源于《陕西师范大学》期刊2017-05-01）
马占有,李永明[6]（2016）在《基于决策过程的广义可能性计算树逻辑模型检测》一文中研究指出本文研究了广义可能性计算树逻辑模型检测算法及其在系统验证中的应用,特别是在非确定性系统验证中的应用.首先引入作为系统模型的广义可能性决策过程和描述系统属性的广义可能性计算树逻辑,然后给出基于广义可能性决策过程的广义可能性计算树逻辑模型检测算法.该算法最大的优点是利用决策过程中的调度,将模型检测问题转换为多项式时间内模糊矩阵的运算或模糊矩阵不动点的计算.最后通过一个实例说明了广义可能性计算树逻辑模型检测在非确定性系统中的应用.(本文来源于《中国科学:信息科学》期刊2016年11期）
赵杰[7]（2016）在《广义可能性计算树逻辑的范式研究》一文中研究指出自从1981年Clark和Emerson提出了模型检测,其作为一种形式化的自动化验证技术有效的弥补了传统测试方案所遗留的问题,因此受到了人们的普遍的关注。模型检测的一般过程是这样的:首先对需要被检测的系统和被验证的性质进行抽象建模,再通过模型检测算法对模型进行形式化验证来判断系统是否满足对应的性质。在经典的模型检测理论中,由于无法正确的处理系统的中不确定性问题,因此一些学者提出了多种状态迁移的量化扩展,基于广义可能性Kripke结构的广义可能性计算树逻辑的模型检测就是其中的一个代表。由于时序逻辑的范式在模型检测中有着重要的应用,但是在广义可能性计算树逻辑中还没有对范式进行过系统的研究,因此本文的主要工作就是在此背景下进行的。本文的主要内容如下:1.本文给出了广义可能性计算树逻辑的两种不同的范式——正态范式(Positive Normal Form,简记为 PNF)和存在范式(Existential Normal Form,简记为ENF),并且给出了对应范式的语构和语义解释。2.通过归纳假设法证明了对于任意的一个广义可能性计算树逻辑的公式都存在与之等价的PNF和ENF的公式。3.给出了一个将任意的广义可能性计算树逻辑的公式转换为与之对应的PNF公式和ENF公式的算法,并且通过实例进行分析说明。(本文来源于《陕西师范大学》期刊2016-05-01）
马占有,李永明[8]（2015）在《广义可能性决策过程的计算树逻辑模型检测》一文中研究指出模型检测作为一种形式化验证技术,已被广泛应用于各种并发系统的正确性验证。针对具有非确定性选择和广义可能性分布的并发系统,引入广义可能性决策过程作为此类系统的模型;给出描述其性质的规范语言广义可能性计算树逻辑的概念;研究此类系统的广义可能性计算树逻辑模型检测问题。结论表明,其模型检测算法的时间复杂度也为多项式时间。所获得的结果扩大了广义可能性测度在模型检测中的应用范围。(本文来源于《计算机工程与科学》期刊2015年11期）
鲍秋霜,张晋津[9]（2016）在《直觉主义计算树逻辑中的安全性和活性》一文中研究指出将Patrick Maier关于直觉主义线性时序逻辑的研究扩展到计算树逻辑中,基于完全树和非完全树构成的集合提出了一种直觉主义解释的计算树逻辑,并在此逻辑框架中研究了安全性和活性及其相关性质。比较了经典计算树逻辑与直觉主义计算树逻辑的表达能力,探究了直觉主义计算树逻辑中安全性和活性在并、交等操作下的封闭性以及与经典计算树逻辑中安全性和活性的关系,并为直觉主义计算树逻辑公式建立了分解定理。(本文来源于《计算机科学与探索》期刊2016年02期）
赵杰,李永明[10]（2016）在《广义可能性计算树逻辑的两种范式》一文中研究指出计算树逻辑(computation tree logic,CTL)的范式在模型检测方法中具有重要意义,但基于广义可能性测度的计算树逻辑的范式尚未有系统研究。为了进一步完善广义可能性计算树(generalized possibilistic computation tree logic,GPo CTL)理论,在现有的广义可能性计算树逻辑理论的基础上,参考经典计算树逻辑的范式,给出了广义可能性计算树逻辑的两种不同的范式——正态范式(positive normal form,PNF)和存在范式(existential normal form,ENF),及其对应的语构和语义解释。最后利用归纳假设法证明了任意的广义可能性计算树逻辑公式都有与之等价的PNF公式和ENF公式。(本文来源于《计算机科学与探索》期刊2016年10期）
计算树逻辑论文开题报告
（1）论文研究背景及目的
此处内容要求：
首先简单简介论文所研究问题的基本概念和背景，再而简单明了地指出论文所要研究解决的具体问题，并提出你的论文准备的观点或解决方法。
写法范例：
模型检测是一种自动验证软硬件系统行为的有效技术。为了对包含非确定性信息、不一致信息的并发系统进行形式化验证,在可能性理论、多值逻辑的基础上,研究了具有多值决策过程的广义可能性多值计算树逻辑模型检测算法,及其在检验非确定性系统中的具体应用。首先构造了多值决策过程作为系统模型,用多值计算树逻辑描述系统属性。然后给出具有多值决策过程的广义可能性多值计算树逻辑的模型检测算法,该算法将模型检测的具体问题转换为多项式时间内的模糊矩阵运算。最后就包含非确定性选择的多值系统的模型检测问题,给出一个具体的应用实例。
（2）本文研究方法
调查法：该方法是有目的、有系统的搜集有关研究对象的具体信息。
观察法：用自己的感官和辅助工具直接观察研究对象从而得到有关信息。
实验法：通过主支变革、控制研究对象来发现与确认事物间的因果关系。
文献研究法：通过调查文献来获得资料，从而全面的、正确的了解掌握研究方法。
实证研究法：依据现有的科学理论和实践的需要提出设计。
定性分析法：对研究对象进行“质”的方面的研究，这个方法需要计算的数据较少。
定量分析法：通过具体的数字，使人们对研究对象的认识进一步精确化。
跨学科研究法：运用多学科的理论、方法和成果从整体上对某一课题进行研究。
功能分析法：这是社会科学用来分析社会现象的一种方法，从某一功能出发研究多个方面的影响。
模拟法：通过创设一个与原型相似的模型来间接研究原型某种特性的一种形容方法。
计算树逻辑论文参考文献
[1].韩英杰,周清雷,朱维军.基于DNA计算的计算树逻辑模型检测方法研究进展[J].计算机科学.2019
[2].袁申,魏杰林,李永明.具有多值决策过程的广义可能性计算树逻辑模型检测[J].计算机工程与科学.2019
[3].范艳焕,李永明,潘海玉.不确定型模糊Kripke结构的计算树逻辑模型检测[J].电子学报.2018
[4].梁常建,李永明.广义可能性计算树逻辑的模型检测问题[J].电子学报.2017
[5].李丹.广义可能性计算树逻辑表达能力的研究[D].陕西师范大学.2017
[6].马占有,李永明.基于决策过程的广义可能性计算树逻辑模型检测[J].中国科学:信息科学.2016
[7].赵杰.广义可能性计算树逻辑的范式研究[D].陕西师范大学.2016
[8].马占有,李永明.广义可能性决策过程的计算树逻辑模型检测[J].计算机工程与科学.2015
[9].鲍秋霜,张晋津.直觉主义计算树逻辑中的安全性和活性[J].计算机科学与探索.2016
[10].赵杰,李永明.广义可能性计算树逻辑的两种范式[J].计算机科学与探索.2016