计算树逻辑相关论文
计算树逻辑（Computation Tree Logic,CTL）模型检测是形式化方法研究的热点,是保证系统正确性的重要手段之一。DNA计算是以DNA分子和......
嵌入式系统的安全性不仅取决于系统硬件的稳定性,而且与系统功能实现代码有密切关系。在一些复杂的嵌入式系统中,嵌入式系统硬件上......
可编程逻辑控制器（Programmable Logic Controller，PLC）是工业自动化的一种重要的控制装置，在一些安全苛求的行业中（例如在交通、电力和......
混合系统主要研究由连续性子系统和离散性子系统相互作用而构成的一类动态系统。连续性子系统和离散性子系统二者相互作用,使系统......
如何从协议规范出发生成满足一定覆盖标准的测试序列和测试套是协议一致性测试中的一个核心问题，现有的协议一致性测试序列和测......
网络的最大特点是共享,相伴产生的安全问题也成为人们不得不面对的问题,特别是用来保证信息传输安全的网络安全协议的安全性显得尤......
为了解决复杂计算机系统的验证问题,确保系统的正确性与可靠性,人们提出了模型检测方法.该方法于1981年首次被Clark和Emerson提出,......
随着计算机软硬件体系的发展,能够确保其安全、可靠的形式化验证成为研究热点。其中,模型检测作为一种用来验证有限状态系统是否满......
混合系统是连续动态过程和离散事件动态过程并存,且相互影响、相互作用的一类动态系统。八十年代后期,随着微型计算机、大型通讯网......
摘要：安全计算机平台是轨道交通信号控制系统的核心基础安全设备,通过测试来检验安全计算机平台是否能实现设计的安全功能是至关重......
如何有效的对SoC设计进行验证已经成为缩短设计周期的关键问题.针对这个问题,本文提出一种形式化建模与验证方法,对片上系统AMBA工......
分布式信息流控制是增强系统安全的一种有效方法，但其灵活性也增加了策略管理和分析的复杂性。策略的安全性分析判定系统的所有可达......
为了增强计算树逻辑在时序上的表达能力,以广义可能性测度、决策过程和计算树逻辑为基础,研究了具有决策过程的广义可能性模糊时态......
本文研究了不确定型模糊Kripke结构的计算树逻辑的模型检测问题,并说明了该问题可以在对数多形式时间内解决.首先给出了不确定型模......
构件式系统是一种采用构件组合技术实现的结构系统，即在采用单个构件封装简单的业务功能基础上，通过集成多个构件逐步构造新的组合构......
根据初始状态、状态之间的转换关系和命题赋值函数是否为分明的，模糊Kripke结构可分为8类。提出将模糊计算树逻辑作为判断模糊Kripk......
计算树逻辑（computation tree logic，CTL）的范式在模型检测方法中具有重要意义，但基于广义可能性测度的计算树逻辑的范式尚未有系统研......
广义可能性计算树逻辑（generalized possibilistic computation tree logic，GPoCTL）在不确定性模型检测中扮演着非常重要的角色，但其表......
将Patrick Maier关于直觉主义线性时序逻辑的研究扩展到计算树逻辑中,基于完全树和非完全树构成的集合提出了一种直觉主义解释的计......
本文首先分别给出了“约束可达”,“总是可达”这两个公式在广义可能性计算树逻辑（GPo CTL）中的另外两种等价形式;其次讨论了基于广......
模型检验是系统级设计中验证可信计算系统安全性性质的有效方法。动态模型检验是模型随设计过程而变化的模型检验，动态模型检验过程......
摘要：混合系统是同时包含有相互作用的连续性子系统和离散性子系统的一类动态系统。混合自动机是目前混合系统验证研究中最常用的一......
针对LSB替换隐写的取证问题,从软件检测的角度出发,提出一种基于计算树逻辑的隐写软件检测方法。该方法采用计算树逻辑描述LSB替换......
在计算树逻辑（CTL）中引入过去时态算子，得到了表达力更强的属性规约语言CTLP，给出了CTLP的模型检测算法及其固定点刻画。该算法的复杂......
首先,给出了基于广义可能性测度的计算树逻辑的扩展GPoCTL＊、计算树逻辑的约简GPoCTL^-以及带回报的计算树逻辑GPoRCTL的语构和语义......
计算树逻辑的不动点语义在其对应的符号模型检测方法中具有重要意义。给出广义可能性计算树逻辑的不动点语义解释，并利用归纳法证明......
引入了基于Zadeh模糊逻辑的计算树逻辑的语法和语义,讨论了不同的模糊计算树逻辑公式之间的语义关系,分析了模糊计算树逻辑语义模......
可能性测度计算树逻辑模型检测验证中存在诸多问题,例如低性能效率和高时间复杂度。针对上述问题,基于传统的模型检测标记算法,为......
为了解决基于模糊逻辑的模型检测修复问题,提出了模糊计算树逻辑模型检测的模型修复算法。该算法采用原子修复操作来修复模糊Kripk......
检测部分状态空间是近年来出现的有效解决状态爆炸的模型检测技术,部分Kripke结构是描述部分状态空间的形式框架.文章主要讨论一类......
模型检查是系统验证的有效方法，在验证过程中需要对系统待检验特性用时态逻辑公式进行刻画，然后在模型检查工具中进行检验。介绍计算......
为了形式化规范、验证和分析反应式并发系统,学术界提出并发展了多种形式化规范方法。这些方法大体上可分为两类：基于动作的和基于......
随着信息技术的发展,各行各业在实际应用中都产生了大量的数据,为了能在这些海量数据中发现对其所属领域有用的信息和知识,作为知......
模型检验是一种确保设计规范正确性的形式化自动验证技术,本文提出了对UML状态机进行模型检验的方法.文中首先对UML状态机的语法和......
交互时态逻辑已被广泛应用于开放系统的规范描述，交互时态逻辑的模型检测技术是一个比较重要的验证方法。为了形式化描述和验证具有......
模糊并发博弈结构是一种可以对具有模糊不确定信息的开放系统进行建模和分析的工具,基于该模型的模糊交互时态逻辑的模型检测问题......
模型检测由图灵奖得主Clarke教授等人提出,是一种能够自动验证系统是否满足指定性质的技术,并且在系统不满足性质时提供反例,被广......
片上总线协议是片上总线技术的核心,其设计的好坏直接影响到片上系统芯片的可靠性。针对Avalon片上总线协议的自身特点和复杂性,给......
期刊
本文提出了一个基于传统BDI（Belief，Desire，Intention）结构的新型Agent模型，即：BDIM模型．通过在传统的BDI结构模型基础上追加激励算子（moti......
雷达数据处理软件是雷达目标跟踪、组网协同处理等功能的核心软件,包含多种关键算法和处理方法。这些方法的过程往往差异大,适用环......
