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. Such systems are typically simple to describe, yet they have a rich algorithmic and mathematical theory that is replete with simply stated and compelling open problems.  

The goal of this project is to achieve a major advance in the algorithmic theory of fundamental dynamical systems arising in verification and related areas. The research programme 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 will be considered (reachability, invariant synthesis, model checking, etc.) are particularly relevant to algorithmic verification, automata theory, and program analysis.  

The project represents an ambitious advance, with a major rationale being to prosecute new approaches to central open problems on linear systems, such as the Skolem Problem. In addition, it aims to go beyond pure linear dynamics and analyse models with conditional branching, nondeterminism, an external controller, and polynomial recursivity. To this end, the methodology combines automata theory, model theory, and symbolic dynamics, on the one hand, with algebraic and Diophantine geometry, on the other.  

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.