稠密时间区间时序逻辑的可满足性判定

定义了稠密时间区间时序逻辑(DTITL),它是区间时序逻辑的一种实时扩充．通过定义DTITL无穷状态空间上的具有有限个数等价类的等价关系,把DTITL的连续状态模型离散化为一阶区间时序逻辑模型．定义了一套规则来构造DTITL公式对应的有界整数域上一阶区间时序逻辑子集SFO的公式,从而把DTITL的可满足性判定问题等价地转化成了SFO的判定问题．利用多个命题变量等价表示有界整数,把SFO的可满足性判定问题等价转换为可判定的命题区间时序逻辑的判定问题．解决了DTITL的可满足性判定问题．     

基于时间区间时序逻辑的实时系统统一模型检测

在同一个逻辑框架内无法自动验证实时区间模型的实时区间性质. 为此, 该文使用一个离散时间区间时序逻辑公式建立实时系统模型, 使用另一个离散时间区间时序逻辑公式描述实时系统需要满足的性质, 在此基础上, 离散时间区间时序逻辑统一模型检测问题即可归约为目前已解决的离散时间区间时序逻辑可满足性判定问题. 该文证明了新方法的有效性以及正确性, 为区间实时逻辑这一类的模型检测问题提供了方法.     

多速率混合系统的模型检查

研究了初始化的多速率混合系统的模型检查问题,即检验初始化的多速率自动机是否满足某个混合区间时序逻辑公式描述的性质．首先定义了一套转换规则把混合区间时序逻辑公式转化为区间时序逻辑公式．接着定义了初始化的多速率自动机状态空间上的等价关系及其对应的域自动机,并且通过构造域自动机对应的标注有限状态自动机,把初始化的多速率混合系统的模型检查问题等价地转换成了可解的区间时序逻辑的模型检查问题．利用区间时序逻辑的模型检查算法加上上述的转换规则,就可以解决初始化的多速率混合系统的模型检查问题．     

使用扩展区间时序逻辑为并发工作流建模

针对集中式体系结构并发工作流的两种运行方式(活动并发执行和活动以任意顺序执行),对区间时序逻辑进行扩展,提出两个新操作符“交错”和“限制性交错”．根据工作流状态的偏序关系以及逻辑公式连接前后其模型的长度关系,证明用新操作符连接的区间时序逻辑公式适于表示并发工作流．结合一个并发工作流实例,说明如何用扩展区间时序逻辑表示活动及由活动组建的并发工作流,从而得到并发工作流的区间时序逻辑模型．利用并发工作流的区间时序逻辑模型验证并发工作流的活性和安全性,可大大提高并发工作流设计的可靠性．     

基于OBDD的εL^（￢）本体判定算法

有序二叉决策图(OBDD)是一种新型的数据结构,在较大状态空间规模的模型检测和验证等领域中,已经得到了成功应用,并且在逻辑公式的可满足性判定方面也具有巨大的应用潜力.通过采用OBDD实现了描述逻辑εL(一)判定算法.以基于OBDD的SHIQ判定算法为基础,针对描述逻辑εL(一)进行了优化,应用标准化规则取代了FLAT规则,重构了知识库模型,进而将该模型转化为满足3CNF(每个从句含有3个变元的合取形式)约束的布尔函数并利用OBDD进行可满足性判定,并以实例对算法过程进行了演示.     

区间时序逻辑的模型检查

为了检验标注有限状态自动机描述的系统是否满足某个区间时序逻辑公式刻画的性质,定义了一套转换规则．利用这些规则,可以构造一个chop-自动机,该自动机接受的语言恰是所有满足这个区间时序逻辑公式的模型的集合．同时,定义了一套转换规则把一个chop-自动机转换为一个标注有限状态自动机,使得它们接受相同的原子命题序列集．这样,区间时序逻辑的模型检查问题就等价地转换成了很容易解决的两个标注有限状态自动机的语言包含问题．     

Verilog程序的命题投影时序逻辑符号模型检测

为了保证以Verilog硬件描述语言设计的片上系统的正确性,提出了Verilog程序的符号模型检测方法．依据形式化操作语义将Verilog程序建模为有限状态机,将设计规范用命题投影时序逻辑公式描述,并采用命题投影时序逻辑符号模型检测工具对程序进行验证,从而证明片上系统满足设计规范．以Verilog程序描述的四位同步二进制计数系统的验证实例表明,Verilog程序的命题投影时序逻辑符号模型检测方法是可行的．     

支持Stutter-不变性的命题区间时序逻辑

为了将命题区间时序逻辑(PITL)应用于组合验证,并降低组合产生的状态爆炸风险,提出了支持Stutter-不变性的命题区间时序逻辑PITLst.PITLst继承了PITL的结构相关性,可表达所有PITL能够表达的Stutter-不变性质,支持模块抽象约简系统规模,降低了状态爆炸风险.自动加油站模型的组合验证实例表明,PITLst可有效应用于组合验证技术.     

半定性约束满足问题求解

从地理信息系统、环境智能等领域的实际需求出发,提出了半定性约束满足问题(SQCSP),并得到了初步结果。证明了区间代数及扩展模型的SQCSP可由QCSP判定。给出了RCC5的多项式时间SQCSP判定算法。RCC8的SQCSP是NP完全问题,给出了带限制条件SQCSP的多项式时间判定算法。证明了上述判定算法的正确性,并给出了实例构造算法。最后,利用SQCSP算法实现了带变量布尔运算的QCSP求解。     

基于 OBDD 的描述逻辑 ALC判定算法

针对描述逻辑 ALC的经典判定算法在处理大规模问题上的不足,而 OBDD 对于处理大规模问题有高效性,给出了一种基于 OBDD 的 ALC判定算法并证明正确性.该算法根据 ALC 的概念的形式,计算所有子概念和每个子概念的否定形式的集合,然后根据该集合里的每个概念的形式构造出其相应的布尔函数,将布尔函数转化为 OBDD 的表示形式来进行概念的可满足性判定.     

Propositional projection temporal logic based distributed model checking method

To alleviate the state-explosion problem of model checking, a novel distributed model checking method based on the propositional projection temporal logic (PPTL). First, the property to be verified in the PPTL formula is transformed into an automaton with the technique of Labeled Normal Form Graph, which in turn is partitioned into multiple subautomata according to the strongly connected components. Then, each subautomaton and the system model in the Hierarchical Syntax Chart are delivered to the members of the verification server cluster, and model checking of the system is implemented in parallel with the on-the-fly technique on multiple computers. Experimental results indicate that, compared with the standalone model checking approach, the proposed method can not only significantly reduce the time consumption but also verify more complex systems.     

用于描述和验证数字电路的一阶间隔时态逻辑

提出一种新的时态逻辑——一阶间隔时态逻辑（ＦＯＩＴＬ）,它是扩充了间隔时间算子的一阶时态逻辑。它能精确地描述数字电路的时间特性,支持连续和离散的时间结构并能对时间信息进行推理。本文给出了ＦＯＩＴＬ的基本框架,并对其进行了验证。     

基于 KQML的多智能体系统建模与验证

为了保证 MAS相关属性的可满足性、有效性以及验证的高效性,提出了一种基于 KQML 通信语言的MAS建模以及能够实现自动验证相关规范的方法.设计并实现了 KQML 语言转化为完整描述状态转换关系的一组状态迁移七元组的算法,以及从七元组到多智能体模型检测工具 MCMAS输入语言ISPL的转化算法,从而实现多智能体系统的自动形式化建模,并用 MCMAS对多智能体系统规范的正确性进行验证.实验结果表明,所提出的算法不仅能够验证多智能体系统的时态规范,还能验证其特有的认知规范.     

Polynomial algorithm of limited propositional deduction

For the problem of propositional satisfiability a polynomial algorithm of limited propositional deduction is proposed which can be viewed as a sort of boolean constraint propagation mechanism. It can be embodied in a backtracking search program for propositional satisfiability problems to make search efficient. The efficiency is gained in two ways: One is to use the algorithm to derive literals so as to overcome the ambiguities in search. The other is to exploit the consequence sets of unbound atoms generated during limited deduction as a heuristic measure for possible choices. The experiments have shown remarkable improvement in reducing search space. Project supported by the “863” High-Tech Program of China.     

进位保留加法器的命题投影时序逻辑组合验证

为保证硬件设计的正确性,提出了对硬件设计组合验证的新方法．该方法在命题投影时序逻辑的统一框架下,实现对硬件系统行为的建模,对所期望性质的形式化描述,并利用命题投影时序逻辑合理且完备的公理系统对系统性质进行验证,从而证明硬件系统满足期望的性质,保证设计的正确性．进位保留加法器的验证实例说明了该方法的可行性．     

界标知识及其应用研究进展

国内外相关研究表明界标知识的三种应用角度为：设计问题分解方法、设计启发函数和设计约束传播机制.利用界标知识设计的可纳启发函数与最优松弛估计的相对误差能降低到2.5％;利用界标知识设计的经典规划启发函数对搜索算法的引导能力优于之前的启发函数;利用界标知识设计的时态规划启发函数能使规划系统得到更高质量的规划解;将界标知识转化为命题逻辑子句能在大规模困难问题上提高可满足性判定算法的求解效率.因此,界标知识在时态规划启发函数设计和基于动作序列空间的规划方法上的应用值得深入研究.