随机混成系统状态估计算法理论研究

In the real time embedded systems, undeterministic and random behaviours rise more and more. Recently, the formal methods scientists established different stochastic hybrid systems (SHS) modelling such complex systems for analysis and verification. The state estimation plays a core role in the study of SHS. Current estimation mainly employed the Markov process through abstracting the system states. But it is rarely hard to see the investigation of estimation to continuous states for formal methods. This may be due to the hardness of estimation to differential or even stochastic differential equations. Therefore, the project plans to (1) study the probabilistic invariant, (2) explore the filter algorithm for nonlinear SHS, and (3) investigate the method how to transform an elementary hybrid system into a polynomial hybrid system using stochastic abstracting, based on our previous work about the complete invariant generation algorithm for polynomial hybrid systems, the abstraction of elementary hybrid systems to polynomial hybrid systems, extension of Kalman filter to nonlinear systems via moments matching and the umbrella sampling technique. Our goal is to develop some high accuracy, efficient and stable state estimation method for the usage of simulation, testing and verification of SHS.

随着各种嵌入系统越来越复杂，系统的不确定性、随机性行为越来越常见。最近在形式化方法研究领域内建立了几种该类系统的随机混成系统模型，肇基随机混成系统形式化方法分析与验证研究。随机混成系统状态估计是该方向研究的一个核心内容。目前的主要方法是通过系统离散抽象，然后使用马科夫进程对离散状态进行估算。由于涉及微分方程甚至随机微分方程，适用于形式化方法中仿真、测试与验证技术的连续状态估计研究进展甚微。因此，本项目将基于我们在经典混成系统研究中提出的多项式不变式完备算法和初等混成系统多项式化抽象技术以及在非线性卡曼滤波研究中提出的高阶矩匹配方法与伞形采样技术，研究（1）随机混成系统的概率不变式，（2）非线性随机混成系统状态估计的滤波算法，（3）初等混成系统的随机方法多项式化技术。我们期望通过本项目研究找到某种可用于随机混成系统仿真、测试与验证的高效、高精度以及高稳定性的状态估计方法。

随着各种嵌入系统在智能交通、分布式机器人以及自动工厂等领域越来越复杂的应用，系统的不确定性、随机性行为越来越常见。随机混成系统是对该类系统的一个严格形式化数学模型。随机混成系统状态估计是该方向研究的一个核心内容。其中主要方法是通过系统离散抽象，然后使用马科夫进程对离散状态进行估算。由于涉及微分方程甚至随机微分方程，适用于形式化方法的仿真、测试与验证技术的连续状态估计是一件十分困难的工作。本项目基于项目组在经典混成系统研究中提出的多项式不变式完备算法和初等混成系统多项式化抽象技术以及在非线性卡曼滤波研究中提出的高阶矩匹配方法，(1)研究了随机混成系统的概率不变式方法，通过分治思路，基于无穷小生成元的Dynkin公式，结合伊藤微分引理与李导数使用鞅的方法的概率不变式的研究取得了一些进展，结合Euler–Maruyama方法、 Milstein方法以及Runge–Kutt方法研究了随机微分方程的数值逼近计算；(2)研究了非线性随机混成系统状态估计的滤波算法，结合蒙特卡洛采样法、重要性采样法、吉布斯采样法、高斯采样法、无迹采样法以及容积采样法等方法以及高斯分布特性，研究并提出了一种多重对称几何分布的无迹采样方法——几何无迹采样方法；(3)通过统线性方法研究了初等混成系统的不变式计算复杂度降低技术，提出了线性化测试布尔公式不可满足性的新判定准则，得到一个具有明确的多项式时间计算复杂度的不可满足性测试方法，提出了一个新的大规模系数线性方程组求解方法，得到一个线性方程组精确解的迭代公式，基于系统状态可达集计算内逼近方法我们提出了一种的混成安全系统设计方法可以把所有局部不安全的子系统合成一个安全混成系统。项目研究结果为安全攸关混成系统的设计与验证提供基础性理论支撑。