Symbolic reachability computation of a class of second-order systems

Reachability is an important property of safety which widely analyzed in designing physical control systems. By contrast to issues related to stability and controllability of physical systems are well-studied in control theory, there are many results on reachability of those systems in computer science, but mainly for some trivial linear systems developed by formal methods and tools. In this paper, we present the first known family of second-order systems with the decidable symbolic computation problem of its reachable state space at the best of our knowledge. We extend the approach that reducing reachability computation into semi-algebraic system solving and analyzing the special type of second-order systems carefully. We also illustrate the application of our method by performing the Maple package DISCOVERER successfully.