Reachability Analysis of Linear System

TL;DR

This paper introduces a decision procedure for reachability analysis in linear systems with algebraic eigenvalues and trigonometric-exponential inputs, utilizing algebraic and semi-algebraic methods, and assuming Schanuel's Conjecture for completeness.

Contribution

It presents a novel decision procedure for reachability in linear systems with complex inputs, combining polynomial inequalities and semi-algebraic set analysis, under a conjecture-based completeness assumption.

Findings

The approach is efficient based on experimental results.

Decidability is achieved for systems with single-point initial sets.

Procedures are complete assuming Schanuel's Conjecture.

Abstract

In this paper, we propose a decision procedure of reachability for linear system {\xi}' = A{\xi} + 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