论文标题
线性系统的可及性分析
Reachability Analysis of Linear System
论文作者
论文摘要
在本文中，我们提出了一个线性系统ξ=aξ + u的可及性的决策过程，其中矩阵A的特征值可以是任意的代数数，而输入u是三角指数式多项式的向量。如果初始组仅包含一个点，则所考虑的可及性问题将诉诸三角指数 - 指数多项式的迹象，然后通过简化验证一系列单变量多项式不等式来实现，通过taylor扩展相关的指数功能和Trigonometricric函数。如果初始集是开放的半代数，我们将提出一个基于OpenCAD的决策程序和从三角义指数多项式的签名过程中得出的真根隔离算法。实验结果表明我们方法的效率。此外，在雪泽猜想的假设下，上述程序是完整的
In this paper, we propose a decision procedure of reachability for linear system ξ' = Aξ + u, where the matrix A's eigenvalues can be arbitrary algebraic numbers and the input u is a vector of trigonometric-exponential polynomials. If the initial set contains only one point, the reachability problem under consideration is resorted to the decidability of the sign of trigonometric-exponential polynomial and then achieved by being reduced to verification of a series of univariate polynomial inequalities through Taylor expansions of the related exponential functions and trigonometric functions. If the initial set is open semi-algebraic, we will propose a decision procedure based on openCAD and an algorithm of real roots isolation derivated from the sign-deciding procedure for the trigonometric-exponential polynomials. The experimental results indicate the efficiency of our approach. Furthermore, the above procedures are complete under the assumption of Schanuel Conjecture
