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.