基于线性时态逻辑的Petri网模型检测研究

线性时态逻辑Petri网结合了Petri网和时序逻辑的优点,清晰简洁的描述并发系统事件间的时序和因果关系,包括系统的活性和安全性.其中自动机的体积是模型检验的一个关键性问题,为了得到尽可能小体积的自动机,在LTL公式转换为Büchi自动机之前,对LTL公式进行预处理来减少冗余,然后通过布尔技术优化自动机.     

LTL公式到自动机的转换

在LTL公式和自动机理论的基础上,给出了一种从LTL公式到自动机的转换算法.该算法先简化LTL公式,然后再对简化的LTL公式转换,形成选择Buchi自动机.此算法与其他算法相比,具有可扩展性的优点,可以在此基础上形成属性描述语言PSL向自动机的转换.     

从基于迁移的扩展Büchi自动机到Büchi自动机

目前的模型检测方法中,有一种方法是基于自动机来实现的.具体做法是:将抽象出的系统模型用Büchi自动机来表示,将需要验证的性质用LTL(linear temporal logic)公式来表达;然后将LTL公式取反后转化为Büchi自动机,并检查这两个自动机接受语言之间的包含关系.有一类LTL公式转化为Büchi自动机的算法是:在计算过程中,首先得到一个标注在迁移上的扩展Büchi自动机(transition-based generalized Büchi automaton,简称TGBA),然后把这种扩展Büchi自动机转换成非扩展的Büchi自动机.针对这类转换算法,根据Büchi自动机接受语言的特点,重新定义了基于迁移的扩展Büchi自动机的求交运算,减少了需要复制的状态个数,使转换后的自动机具有较少的状态.测试的结果表明:对随机产生的公式,新算法相对于以往的算法有明显的优势.     

一种有效的基于LTL和Petri网的模型检测方法

模型检测的一个主要方法是构建线性与时序逻辑（LTL）公式φ的否定形式等价的Büchi自动机Aφ和系统模型M的正交积，并检测正交积的可接受语言是否为空。通过对Generalized Büchi自动机进行化简，可以减小自动机的状态空间，从而提高模型检测的效率。根据所提出的方法设计并实现的基于LTL和Petri网进行模型检测的工具包，可以有效地对基于Petri网表示的系统模型进行模型检测。     

基于EHA模型检验Statecharts

模型检验是一种重要的形式化自动验证技术。Statecharts是一种用以规约复杂反应式系统行为的可视化语言。为了验证Statecharts模型是否满足所期望的性质,该文给出了一种基于EHA模型检验Statecharts的方法,首先把Statecharts转换为EHA,通过其操作语义得到Büchi自动机,然后与LTL公式所得的Büchi自动机相乘,最后检查该乘积自动机所能接受的语言是否为空,来判断是否满足所期望的性质。     

PSL构造双向交换自动机及非确定自动机的方法

PSL(property specification language)是一种用于描述并行系统的属性规约语言,包括线性时序逻辑FL(foundation language)和分支时序逻辑OBE(optional branching extension)两部分.由于OBE就是CTL(computation tree logic),并且具有时钟声明的公式很容易改写成非时钟公式,因此重点研究了非时钟FL逻辑.为便于进行模型检验,每个FL公式必须转化成为一种可验证形式,通常是自动机(非确定自动机).构造非确定自动机的过程主要是通过中间构建交换自动机来实现.详细给出了由非时钟FL构造双向交换自动机的构造规则.构造规则的核心逻辑不仅仅局限于是在LTL(linear temporal logic)基础上的正规表达式,而且全面而充分地考虑了各种FL操作算子的可能性.并且给出了将双向交换自动机转化为非确定自动机的一种方法.最后,编写了将PSL转化为上述自动机的实现工具.FL双向交换自动机的构造规则计算复杂度仅是FL公式长度的线性表达式,验证了构造规则的正确性.在此基础上,证明了双向交换自动机与其转化的等价的非确定自动机接受的语言相同.上述工作对解决复杂并行系统建模和模型验证问题具有重要的理论意义和应用价值.     

UML模型检测方法的研究

统一建模语言（UML）是设计和分析软件系统最常用的方法，如何保证UML模型满足某些特性是一个非常重要的问题，而模型检测是一种能够有效提高系统可靠性的自动化技术。研究了使用简单进程元语言解释器（SPIN）对UML模型进行检测的方法。首先对UML模型进行形式化描述，使用层次自动机来描述状态图，然后根据层次自动机的操作语义将状态图和类图的部分信息转化为SPIN的输入语言PROMELA，使用SPIN来验证模型是否满足给定的线性时序逻辑所描述的系统约束，通过LTL公式描述顺序图的方式来验证与状态图之间的一致性问题。项目组基于此方法还开发了一套模型检测工具UMLChecker。     

一种利用非确定规划的LTL合成方法

LTL合成(Linear Temporal Logic synthesis)是程序合成(program synthesis)的一类重要子问题, 旨在自动构建一个控制器(controller), 且要求该控制器和环境(environment)的行为交互满足给定的LTL公式.一般来说, 可以将LTL合成定义为二人博弈(two-player game)问题, 博弈的双方是环境和控制器, 该问题的解称为合成策略.近年来, 有研究从理论角度讨论了LTL合成与非确定规划(non-deterministic planning)的相关性.基于此, 本文提出了一种新的利用非确定规划求解LTL合成问题的方法, 并证明了方法的正确性和完备性.具体而言, 首先获得LTL公式对应的Büchi自动机, 结合二人博弈定义, 将LTL合成问题转换为完全可观测的非确定规划模型, 然后交由高效规划器求解.通过实验结果说明, 与其他LTL合成方法相比, 本文提出的基于规划的合成方法在解质量方面具有较大的优势, 能够获得规模较小的合成策略.     

程序时序属性的自动测试

测试预言是一种用来检测被测系统的测试执行是否正确的方法。文中，作者设计并实现了一种根据程序的线性时序逻辑(LTL)的性质产生测试预言的方法。首先，作者将一线性时序逻辑公式转换为一个有限状态自动机，然后，管理源代码，以便抽取与线性时序逻辑性质有关的状态序列。最后，用谊信息来模拟状态自动机，并决定程序执行是否满足线性时序逻辑的性质。     

Streett自动机确定化工具

自动机的确定化是将非确定性自动机转换为接收相同语言的确定性自动机,是自动机理论的基本问题之一.ω自动机的确定化是诸多逻辑,如SnS, CTL*,μ演算等,判定过程的基础,同时也是解决无限博弈求解问题的关键,因此对ω自动机确定化的研究具有重要意义.主要关注一类ω自动机——Streett自动机的确定化.非确定性Streett自动机可以转换为等价的确定性Rabin或Parity自动机,在前期工作中已经分别得到了状态复杂度最优以及渐进最优算法,为了验证提出的算法的实际效果,也为了形象地展示确定化过程,开发一款支持Streett自动机确定化的工具是必要的.首先介绍4种不同的Streett确定化结构:μ-Safra tree和H-Safra tree (最优)将Streett确定化为Rabin自动机, compact Streett Safra tree和LIR-H-Safra tree (渐进最优)将Streett确定化为Parity自动机;然后,根据Streett确定化算法,基于开源工具GOAL (graphical tool for omega-automata and logics),实现...