Paper detail

Reachability Analysis of Linear System

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