Beyond Linear Dynamical Systems

Dynamical systems pervade the quantitative sciences, e.g., recurrence sequences appear across computer science, combinatorics, number theory, economics, and theoretical biology, among many other areas. Characteristically such systems are simple to describe and yet have a rich algorithmic and mathematical theory. The goal of this proposal is to achieve a major advance in the algorithmic theory of fundamental dynamical systems arising in verification and related areas. Our research program aims to expand the frontier of what can be decided on recurrence sequences, piecewise affine maps, constraint loops, linear time-invariant systems, and numeration systems. The decision problems that we consider (reachability, invariant synthesis, model checking, etc.) are particularly relevant to algorithmic verification, automata theory, and program analysis. Some of these problems, such as the Skolem Problem for linear recurrence sequences, have been the subject of sustained interest in the community since the 1970s. In scope, the proposal represents an ambitious advance beyond the research program of the PI over the past 10 years. A major step forward involves analysing models with conditional branching, non-determinism, an external controller, and polynomial recursivity. To this end, our methodology combines automata theory, model theory, and symbolic dynamics, on the one hand, with algebraic and Diophantine geometry, on the other hand. If successful, this project will make significant progress on longstanding open problems and will open new lines of research at the boundary of computer science and mathematics.