混成系统微分不变式计算理论方法

Generating differential invariants is a key point in the design, analysis and verification of hybrid systems. Recently, we invented a complete method to generating and verifying semi-algebraic differential invariants for algebraic hybrid systems. This method and others mainly focus on the deterministic parameter-free algebraic hybrid systems. However, many practical hybrid systems contain parameters derived from the measurement error or the design of system and non-polynomial terms originated from physical motion. The parametric entanglement and the destruction of computability by non-polynomial terms are the main abstacles to generate differential invariants for general hybrid systems using curent methods. At the same time, the complexity of our complete method limits its application in practice. Therefore, based upon our complete method this project will (1) improve our complete method by investigating the propoerty of sigular points of differential invariants, (2) explore the methods to generating differential invariants for hybrid systems with parameters, and (3) attack the generation of differential invariants for elementary hybrid systems. In summary, our basic target is to develop proper methods, based on our complete method, to generating differential invariants of hybrid systems for various cases. Accordingly, the antipated results may be extensively applied to the design, analysis and verification of hybrid systems.

如何计算微分不变式是混成系统设计、分析以及验证的一个核心问题。最近我们对代数混成系统提出了一个完备方法用之生成和检验半代数微分不变式。该方法与已有的其他方法都主要针对确定性代数混成系统。但是,实际混成系统可能由于测量误差或者控制设计等因素而包含某些参数，其模型由于刻画某种物理规律而包含非多项式的子项。参数介入引起的参数纠缠和非多项式子项对模型可计算性的破坏使得一般混成系统微分不变式的研究踟蹰不前。另外，我们的方法虽是完备的，但它的复杂度制约其应用效果。因而本项目将结合完备方法，（1）通过分析不变式边界的奇点性质研究提高该方法效率的技术，（2）探索参数混成系统以及（3）初等混成系统的微分不变式生成与检验技术。本项目的基本目标是基于我们的完备方法加强对混成系统微分不变式生成技术的研究，突破当前只能计算确定性代数混成系统微分不变式的瓶颈。研究结果有望广泛应用于混成系统的分析、设计与验证。

混成系统是嵌入系统、实时系统以及物联网系统等等的一个重要数学模型。该模型对系统的连续和离散动态的描述是系统建模的一个基本方法。其中关于连续状态的建模，一般使用微分方程。但是一般微分方程很难求出解析解。这对混成系统设计、分析和验证的形成一个极大障碍。微分不变式是解决这个问题的一个有效途径。在本项目启动之前，微分不变式的研究主要针对于线性非分系统以及一些特殊多项式系统展开，而且其微分不变式形式也大多局限于多项式理想或者一些超平面的交集（超多面体）。所以本项目当时企图探索更一般的混成系统的一般微分不变式的生成算法，主要包括初等混成系统的微分不变式生成，蕴含参数的混成系统不变式生成，以及关于不变式边界性质的研究。在项目开展的这三年来，我们在该课题上取得了突破性的进展：找到一类生成初等混成系统不变式的方法称着变量变换法，完善其中的理论证明，并且研究大量实际混成系统从初等微分动力系统到多项式微分动力系统的转化案例，比如，嫦娥三号登月着落的控制模型，艾滋传染模型，两罐水箱控制模型等。在理论上，提出了一套新的系统定义域、迁移条件、重置函数的多项式化方案，提出了一套严格的抽象模拟形式化方法与算法，阐明了抽象系统与原系统的轨迹之间的投影关系。在边界性质分析与计算效率研究方面，我们研究了结合半正定规划方法比如SOS和部分求解技术来降低计算复杂度。新方法的使用使得原来一些不可求取不变式的问题得到有效解决。另外，在关于含参数的混成系统不变式研究方面，我们特别研究了参数为随机变量这个特殊情形，取得了初步的成果，提出了一个高精度的状态估计算法，该方法可比传统方法提高50%的精度。这些不变式生成方法与状态估计算法的提出，对于研究混成系统设计、分析以及验证提供了有力的理论基础支撑。