Beyond Linear Dynamical Systems

点击翻译按钮获取中文摘要

Dynamical systems pervade the quantitative sciences, e.g., recurrence sequences appear across computerscience, 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 mathematicaltheory. The goal of this proposal is to achieve a major advance in the algorithmic theory of fundamentaldynamical systems arising in verification and related areas. Our research program aims to expand thefrontier of what can be decided on recurrence sequences, piecewise affine maps, constraint loops, lineartime-invariant systems, and numeration systems. The decision problems that we consider (reachability,invariant synthesis, model checking, etc.) are particularly relevant to algorithmic verification, automatatheory, and program analysis. Some of these problems, such as the Skolem Problem for linear recurrencesequences, have been the subject of sustained interest in the community since the 1970s. In scope, theproposal represents an ambitious advance beyond the research program of the PI over the past 10 years. Amajor step forward involves analysing models with conditional branching, non-determinism, an externalcontroller, and polynomial recursivity. To this end, our methodology combines automata theory, modeltheory, and symbolic dynamics, on the one hand, with algebraic and Diophantine geometry, on the otherhand. If successful, this project will make significant progress on longstanding open problems and willopen new lines of research at the boundary of computer science and mathematics.