On the decidability of reachability in continuous time linear time-invariant systems

We consider the decidability of state-to-state reachability in linear time-invariant control systems over continuous time. We analyze this problem with respect to the allowable control sets, which are assumed to be the image under a linear map of the unit hypercube (i.e. zonotopes). This naturally models bounded (sometimes called saturated) controls. Decidability of the version of the reachability problem in which control sets are affine subspaces of Rn is a fundamental result in control theory. Our first result is decidability in two dimensions (n = 2) if matrix A satisfies some spectral conditions and conditional decidablility in general. If the transformation matrix A is diagonal with rational entries (or rational multiples of the same algebraic number) then the reachability problem is decidable. If the transformation matrix A only has real eigenvalues, the reachability problem is conditionally decidable. The time-bounded reachability problem is conditionally decidable and unconditionally decidable in two dimensions. Some of our results rely on the decidability of certain logical theories - - namely the theory of the reals with exponential (Rexp) and with bounded sine (Rexp, sin) - - which have been proven decidable conditional on Schanuel's Conjecture - - a unifying conjecture in transcendence theory. We also obtain a hardness result for a mild generalization of the problem where the target is a simple set (hypercube of dimension n - 1 or hyperplane) instead of a point. In this case, we show that the problem is at least as hard as the Continuous Positivity problem if the control set is a singleton, or the Nontangential Continuous Positivity problem if the control set is [-1, 1].