定性推理在矩形phase-portrait近似中的应用

抽象近似是验证混合系统安全性的主要方法,矩形phase-portrait近似是通过构造简单的线性混合自动机来近似原混合自动机.phase-portrait近似的关键步骤是如何划分状态空间.本文采用定性推理的方法,叙述了如何根据系统动态特征来划分状态空间及如何精化抽象模型.     

基于定性推理的矩形phase-portrait近似

矩形phase-portrait近似的关键是控制模态的有效划分.本文提出了基于定性推理的phase-portrait近似,给出了一种基于向量场、感兴趣多项式及其李导数动态特性的模态空间划分方法,并进一步给出了基于精化多项式的抽象模型精化方法.实验结果表明,基于定性推理划分的phase-portrait近似验证明显地减少了模态空间的划分数目,提高了验证的效率.     

判定非确定离散事件系统稳定性的多项式复杂度算法

本文讨论基于非确定自动机,形式语言模型的非确定离散事件系统稳定性的多项式算法.在引入拟距离的概念之后.根据拟距离形式化地定义了非确定离散事件系统稳定性.以往判定非确定离散事件系统稳定性的算法基于系统的观测器实现,该观测器在结构上具有指数复杂度,因此本文分析系统结构和观测器结构之间的关系,基于对系统状态对的讨论,提出了判定系统稳定性的有效多项式搜索算法.     

主动自动机学习中的等价查询算法优化

模型学习是一种获取黑盒软件系统行为模型的有效方法,可分为主动学习和被动学习.主动学习是基于字母表构造测试用例,通过与黑盒系统主动交互,可在多项式时间内得到目标系统的最小完备自动机,其中等价查询仍是开发和应用主动自动机学习工具的障碍之一.通过探讨反例对于学习算法的影响,定义假设的比较规则,提出测试用例构造的两个原则,同时依据原则对Wp-method等价查询算法改进,产生更优的假设,有效降低查询的数量,并基于LearnLib开源工具,分别以3类自动机为实验对象验证原则和改进算法的有效性.     

一种Active XML模式重写算法

基于树自动机理论,研究了Active xML(简记为AXML)模式重写问题,提出了一种多项式时间的AXML模式重写判定算法,并对算法进行了实现.实验结果证明了所提算法用于判定AXML模式重写的优越性.     

多项式混合曲线曲面方法构造

针对混合曲线表示及其求导和求积困难的问题,通过计算构造出一种多项式混合曲线曲面形式.当待混合曲线是多项式时,混合曲线也为多项式形式.该多项式混合公式可以推广得到任意参数连续C(n)和几何连续G(n)的混合曲线曲面.另外,在得到的混合曲线曲面族中构造出了新的更优能量光顺方程,通过设置参数可得到合适的混合曲线曲面.实验结果表明,文中提出的混合曲线曲面造型方法稳定、有效.     

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公式长度的线性表达式,验证了构造规则的正确性.在此基础上,证明了双向交换自动机与其转化的等价的非确定自动机接受的语言相同.上述工作对解决复杂并行系统建模和模型验证问题具有重要的理论意义和应用价值.     

入侵检测系统中模式匹配自动机的构造研究

本文提出了一种新的用于构造入侵检测模式匹配自动机的方法。该方法从构造判定单个模式的NFA自动机入手,通过集成单个的NFA而得到全集的NFA,并将全集NFA转换为与之等价的DFA并化简,从而可得到全集的确定型模式匹配有限自动机。由于该方法可以完全自动完成,从而可以方便地为入侵检测系统构造模式匹配自动机。     

基于规则推导的正规式相交判定算法

正规式相交判定问题在扩展标记语言(extensible markup language,XML)类型检查中起着十分重要的作用。传统方法是将其转化为自动机的相交问题,在转化过程中会产生大量计算。基于XML模式语言的特点,提出了一种基于规则推导的正规式相交判定算法。该算法直接根据输入的正规式进行推导而无需进行任何转化计算。对于一般的正规式,尽管其仍然是指数级算法,但无需进行复杂的构造自动机的计算;而对于一些特殊的正规式,特别是在XML类型检查中广泛使用的One-Unambiguous正规式,该算法的时间复杂度降为多项式级。最后证明了该算法所使用的推导规则的正确性和完备性。     

一类时间自动机的时间约束可满足性判定方法

时间自动机是一种有效描述实时系统行为的计算模型。借助时间自动机对实时系统进行分析、设计能够保证所开发的实时系统具有较高的可靠性。在此过程中对时间自动机的验证是非常关键的一步。验证的主要目的是为了保证时间自动机能够正确地描述实时系统。其中迁移的时间约束可满足性就是需要验证的性质之一。常用的方法是通过构造时间区域自动机来实现,但该方法所涉及的状态数目巨大。该文针对一类时间自动机的特点给出了基于时间关系矩阵来判定时间约束可满足性的方法,结果表明该方法能够有效地减少状态数。     

Algorithmic analysis of nonlinear hybrid systems

We present two methods for translating nonlinear hybrid systems into linear hybrid automata. Properties of the nonlinear systems can then be inferred from the automatic analysis of the translated linear hybrid automata. The first method, called clock translation, replaces constraints on nonlinear variables by constraints on clock variables. The second method, called linear phase-portrait approximation, conservatively overapproximates the phase portrait of a hybrid automaton using piecewise-constant polyhedral differential inclusions. Both methods are sound for safety properties. We illustrate both methods by using HYTECH, a symbolic model checker for linear hybrid automata, to automatically check properties of a nonlinear temperature controller and of a predator-prey ecology     

有理曲面的两种多项式逼近及收敛性

研究了有理曲面的hybrid多项式逼近和Hermite多项式逼近的关系.在权系数的某些假定下,得到hybrid多项式逼近和Hermite多项式逼近均收敛的充分必要条件.     

Reformulation of Global Constraints Based on Constraints Checkers

This article deals with global constraints for which the set of solutions can be recognized by an extended finite automaton whose size is bounded by a polynomial in n, where n is the number of variables of the corresponding global constraint. By reducing the automaton to a conjunction of signature and transition constraints we show how to systematically obtain an automaton reformulation. Under some restrictions on the signature and transition constraints, this reformulation maintains arc-consistency. An implementation based on some constraints as well as on the metaprogramming facilities of SICStus Prolog is available. For a restricted class of automata we provide an automaton reformulation for the relaxed case, where the violation cost is the minimum number of variables to unassign in order to get back to a solution.     

On the existence of regular approximations

We approximate context-free, or more general, languages using finite automata. The degree of approximation is measured, roughly speaking, by counting the number of incorrect answers an automaton gives on inputs of length m$m$ and observing how these values behave for large m$m$. More restrictive variants are obtained by requiring that the automaton never accepts words outside the language or that it accepts all words in the language. A further distinction is whether a given (context-free) language has a regular approximation which is optimal under the measure of approximation degree or an approximation which is arbitrarily close to optimal. We study closure and decision properties of the approximation measure.     

基于多面体包含的非线性混成系统可达性分析

针对一类非线性混成系统的可达性问题,提出了一种基于多面体包含的分析方法。首先介绍了混成系统及其可达性,讨论了如何应用多面体包含对多项式混成系统进行线性近似,并采用量词消去和非线性优化方法来构造相应的线性混成系统,然后运用验证工具SpaceEx求得原非线性混成系统的过近似可达集,并应用于验证系统的安全性。     

一种测试语言包含的算法

在积自动机基础上,利用互模拟关系引出商自动机,用以解决积自动机的状态组合爆炸问题。进而提出一个自然的测试语言包含的算法,这种算法的空间复杂度与规范自动机的状态目呈指数关系即O（2^k),其中K是规范自动机的状态数目。     

Deterministic finite automata representation for model predictive control of hybrid systems

As is well known, the computational complexity in the mixed integer programming (MIP) problem is one of the main issues in model predictive control (MPC) of hybrid systems such as mixed logical dynamical systems. Thus several efficient MIP solvers such as multi-parametric MIP solvers have been extensively developed to cope with this problem. On the other hand, as an alternative approach to this issue, this paper addresses how a deterministic finite automaton, which is a part of a hybrid system, should be expressed to efficiently solve the MIP problem to which the MPC problem is reduced. More specifically, a modeling method to represent a deterministic finite automaton in the form of a linear state equation with a smaller set of binary input variables and binary linear inequalities is proposed. After a motivating example is described, a derivation procedure of a linear state equation with linear inequalities representing a deterministic finite automaton is proposed as three steps; modeling via an implicit system, coordinate transformation to a linear state equation, and state feedback binarization. Various significant properties on the proposed modeling are also presented throughout the proofs on the derivation procedure.     

一种改进的区域自动机构造方法

用时间自动机验证一个有穷状态实时系统的正确性，可归结为判定两个时间正则语言的包含问题，亦可归结为判定两个时间正则语言的交是否为空的问题。在判定一个时间正则语言是否为空时，先要将时间自动机转化为无时间的区域自动机。Alur和Dill给出的构造区域自动机的算法，存在许多不可达或虽可达但无用的状态。通过对时钟约束进行分析，在求时钟区域和时间后继的过程中，不断地将一些不可达或无用状态筛掉，使构造出的区域自动机更为优化，改进了Alur等人给出的算法。