Beyond Linear Dynamical Systems

动力学系统渗透在定量科学中，例如，递归序列出现在计算机科学、组合学、数论、经济学和理论生物学等许多领域。这种系统的特点是描述简单，但有丰富的算法和数学理论。该提案的目标是实现验证和相关领域中产生的fundamentaldynamic系统的算法理论的重大进展。我们的研究计划旨在扩大thefrontier什么可以决定递归序列，分段仿射映射，约束环，线性时不变系统，和计数系统。我们考虑的决策问题（可达性，不变综合，模型检查等）与算法验证、自动机理论和程序分析特别相关。其中一些问题，如线性递归序列的Skolem问题，自20世纪70年代以来一直受到社会的持续关注。在范围上，该提案代表了PI在过去10年研究计划之外的雄心勃勃的进步。一个主要的进步涉及分析模型的条件分支，非确定性，外部控制器和多项式递归。为此，我们的方法相结合的自动机理论，modeltheory和符号动力学，一方面，代数和丢番图几何，另一方面。如果成功，这个项目将在长期存在的开放问题上取得重大进展，并将在计算机科学和数学的边界上开辟新的研究领域。

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.