基于模糊测度的模糊分支时态逻辑模型检测

针对具有模糊性和不确定性的复杂系统的验证问题,提出一种基于模糊测度的模糊分支时态逻辑模型检测算法。首先,在模糊决策过程模型的基础上引入模糊分支时态逻辑的语法和语义。然后,给出模糊分支时态逻辑模型检测算法,该算法将模型检测问题转化为矩阵运算,具有计算方式简洁、复杂度较低的优点。最后,通过医疗专家系统的实例说明了该模型检测算法的有效性。

时态逻辑的比较与分析

对时态逻辑的两种重要形式———线性时态逻辑与分支时态逻辑进行了比较和分析，指出它们各自的特点及适用范围。

论时态逻辑的新发展

自20世纪80年代以来,在哲学、计算机科学、人工智能、语言学等诸多领域的推动下,时态逻辑取得了新的发展。主要表现为区间时态逻辑、行为时态逻辑的创立以及时态逻辑与模态逻辑的结合。对这些新的发展进行研究,既具有重大理论意义,又具有重要的实际应用价值。

基于区间的三值时态逻辑

由于许多句子的真值是相对于一定的时段或区间的,所以建立基于区间的三值时态逻辑是必要的。但是基于区间的乌卡谢维奇式三值时态逻辑系统(L3.1,L3.2)并不具有保均致性,于是又提出了一种能保广义基本均致性的语言(L’),给出了相关的语义。

基于代数-时态逻辑的象形对象研究

本文首先讨论了国内外有关面向对象方法学、代数规范、时态逻辑的研究现状 ,分析了对象形式化语义研究的不足 .其次 ,分析了几种主要的系统形式化模型和方法 .然后 ,在我们已研究的“计算机甲骨文象形码输入法”的基础上 ,从时态逻辑的角度定义了象形对象及其约束条件 ,定义了面向对象的有色 Petri网 (OOPEN) ,并应用 OOPEN描述了象形对象的层次结构 .最后 ,我们将代数规范与时态逻辑相结合 ,对象形对象的语义基础进行了一些研究 .

基于时态逻辑技术的高压输电线系统故障诊断

提出了将线性时态逻辑(LTL)技术和电网故障模拟量信息引入高压输电线系统故障诊断的新思想。建立了LTL形式化演绎的完整语法、语义解释体系。在变电站端,综合考虑系统容错需求及故障诊断的实时性要求,对故障模拟量进行了实时预处理；在调度中心,分析了故障诊断过程中保护、开关动作的时序关系,形成典型故障模式下的开关量事件序列(TDS)及其相应的模拟量状态序列(TAS),并通过LTL表示TDS和TAS中的时序约束条件。最后通过实例验证了推理的可靠性和容错性。

线性时态逻辑中的特性模式

在模型检查应用中,需要使用线性时态逻辑对软件具备的特性进行描述。虽然,不同应用背景涉及不同方面的特性描述,但是线性时态逻辑描述软件特性方式上具有共性。本文从两个方面抽取这种共性,首先,按照线性时态逻辑所描述性质划分,常见性质包括活性、安全性等;其次,按照线性时态逻辑公式的作用范围划分。通过对共同问题,找到共同的描述方法得到线性时态逻辑的特性模式。最后介绍了线性时态逻辑特性模式在SPIN中的应用。

基于时态逻辑的硬件设计形式化验证技术——模型检验

通过对时态逻辑的研究来探讨时态逻辑在硬件设计形式化验证上的应用 ,同时对布尔函数在计算机内的表示二叉判定图 (BDD)进行了进一步地分析 。

基于时态逻辑的形式化联邦校核方法

提出了一种基于时态逻辑的形式化联邦校核方法,采用时态逻辑公式描述联邦各成员的行为逻辑关系,推导出与该时态逻辑公式对应的有限自动机模型,即规范自动机。同时,建立联邦全局行为的状态转移图,即实现自动机,通过检验规范自动机所接受的语言是否包含实现自动机所接受的语言来判断联邦运行时各成员的状态变化是否满足规范要求,达到校核联邦的目的。该方法可用来校核联邦及其成员的交互设计和逻辑行为运行的正确性和逻辑性,具有理论意义和应用价值。

工作流建模中时态逻辑的研究与应用

在使用Petri网构建工作流行为结构模型的同时,使用时态逻辑描述工作流模型的需求与特性,则具有描述能力强、灵活方便的优点。在此基础上,综合考虑时态逻辑列表法和即时验证方法的特点,给出一种主要利用B櫣chi自动机进行工作流模型需求及特性验证的方法,提高了工作流模型的合理性和可靠性。最后,验证分析了电子商务的工作流实例。

时态逻辑形式化描述并发系统性质

时态逻辑是一种描述反应式(并发)系统中状态迁移序列的形式化方法,用于刻画并发系统所需验证的性质,是模型检测的基础.阐述了时态逻辑CTL 及其子逻辑CTL、LTL的语法及语义,然后分析运用时态逻辑描述并发系统性质,最后给出一个应用实例.

直觉模糊集时态逻辑算子及扩展运算性质

首先在考察Atanassov直觉模糊集的基本运算的基础上,引入两个典型的作用于直觉模糊集的时态逻辑算子“□(always)”和“◇(sometimes)”,重点研究了直觉模糊集在直觉模糊时态逻辑算子作用下的若干扩展运算及其性质。最后,将这些运算性质归结为一组定理,并给出详细的证明过程。

基于时态逻辑的软件体系结构描述语言及其可视化环境

在时态逻辑语言XYZ／E的基础上，建立了一种以可视化图形表示的软件体系结构描述语言XYZ／ADL．它可同时描述软件体系结构的静态与动态行为，能在统一的形式框架下完成不同抽象层次体系结构设计之间的逐步过渡，从而将模块化程序设计方法和基于规范的逐步求精方法有机地结合起来。

模糊交互时态逻辑及其语义结构

Alur等人建立的交互时态逻辑(ATL*)是一种重要的多Agent合作逻辑,它对计算树逻辑(CTL*)进行了合作算子拓展,然而它缺乏对不确定时态信息的刻画。通过考察模糊时态事件和模糊时态状态、描述相对时间来改进并发博弈结构,并给出模糊并发博弈结构;把模糊并发博弈结构的若干要件从相对时间域到绝对时间域进行映射,给出已映射模糊并发博弈结构;建立了模糊交互时态逻辑(FATL*),给出其语法,在已映射模糊并发博弈结构下给出其语义;阐述了FATL*的表达力比ATL*强。

基于时态逻辑的多时间序列挖掘模型

为了从多时间序列之间发现的定性的时态相关模式可而更全面的理解和把握系统的演化特性,提出了一种基于时态逻辑的多时间序列挖掘模型。它首先将多时间序列转化为多事件序列,然后将预处理后的多事件序列利用区间时态逻辑(ITL)关系子集来定义多事件序列中事件间的时态相关模式。其次进行多状态序列融合和局部时态观测序列的生成,之后采用频繁模式挖掘算法发现多时间序列的频繁时序模式。该模型有助于解决时间序列挖掘所面临的若干挑战和难题,有助于扩展现有时间序列挖掘系统的功能,从而指导时间序列等复杂类型数据的知识发现过程。实验结果表明了该模型及算法的有效性和优越性。

分拣系统运行过程的时态逻辑描述与分析

本文研究了在时态逻辑框架下自动化仓库分拣系统的工作过程。首先给出了离散事件过程的时态公式模型（ＴＦＭ），并讨论了在该模型下的性质分析问题。描述与分析了基于时态公式对被控对象、控制器和闭环期望动态行为，并对系统期望行为的可达性问题进行了形式化的证明。

面向事件图和事件时态逻辑的模型检验方法

针对目前没有适合直接对事件图模型进行性质规约的时态逻辑语言,提出一种基于事件的时态逻辑(event temporal logic,简称ETL).ETL以事件作为原子命题,根据事件图的特点增加了对事件取消操作、模型实例化、时间约束和同时事件优先级的表达能力,便于仿真领域的用户在模型检验过程中简洁地对基于事件图的模型应满足的性质进行描述.然后,在ETL公式和自动机理论的基础上,给出了面向事件图和ETL的模型检验方法来判断事件图模型是否满足ETL描述的性质规约.实例验证了ETL对事件图模型具有足够的表达能力以及该方法的有效性.

具有自反性质的线序时态逻辑研究

为了能够有效的描述现实世界中的相对静止状态,分析了在哲学逻辑理论中的线序时态逻辑定理系统中引入自反性质的可行性,在此基础上建立了具有自反性质的线序时态逻辑系统TA。叙述了TA时态系统的主要定理以及该系统具有无端稠密线序性质,并表明了该系统的紧致性、可靠性和完全性。运用状态重命名方法说明了TA系统与行为时序逻辑TLA系统之间的联系,从而将TA的定理系统运用到行为时序逻辑的研究中。

基于时态测试器的实时分支时态逻辑模型检测

基于自动机理论的模型检测技术在形式化验证领域处于核心地位,然而传统自动机在时态算子上不具备可组合性,导致各种时态逻辑的模型检测算法不能有机整合.为了实现集成限界时态算子的实时分支时态逻辑RTCTL*的高效模型检测,提出一种RTCTL*正时态测试器构造方法以及相关符号化模型检测算法,既证明了所提出的RTCTL*正时态测试器构造方法是完备的,也证明了该算法时间复杂度与被验证系统呈线性关系,与公式长度呈指数关系.基于JavaBDD软件包成功开发了该算法的模型检测工具MCTK2.0.0.完成了MCTK与著名的符号化模型检测工具nu Xmv之间的实验对比分析工作,结果表明:MCTK虽然在内存消耗上要多于nu Xmv,但是MCTK的时间复杂度双指数级小于nuXmv,使得利用MCTK验证大规模系统的实时时态性质成为可能.

行为时态逻辑TLA定理系统证明及公平性研究

行为时态逻辑TLA(temporal logic of actions)能够在一种语言中同时表达模型程序与逻辑规则,是目前模型检测技术中一个较新的研究方向。为了理解行为时态逻辑与传统时态逻辑之间的理论联系,研究了时态逻辑的语义和定理系统,并根据行为时态逻辑TLA的自身特征指出了TLA中的行为属于时态逻辑T4系统。在此基础上严格的证明了TLA的定理系统及TLA中强公平性蕴涵弱公平性的重要性质,讨论了强公平性与弱公平性等价的条件。最后以实例说明了如何确定动作的强弱公平性,进而建立系统的TLA模型。