Minimisation questions on semi-linear sets and infinite-state systems

半线性集是整数的最终周期集到高维的推广。它们出现在各种理论计算机科学主题中；例如，Frobenius硬币问题可以被解释为寻找不包含在给定（一维）受限形式半线性集合中的最大整数的问题。在形式验证中，半线性集合族是一系列验证算法的理论基础，它与Presburger算法中可定义的集合族，即带加法和有序整数的一阶理论相吻合。软件系统中的周期性行为，特别是那些具有并发性的行为，通常可以通过该逻辑捕获，然后自动决策过程（例如在可满足模理论解算器中实现的那些过程）为验证这些系统铺平了道路。由于潜在决策问题的计算复杂度很高，这种方法依赖于输入的小表示。根据确切的设置，半线性集可以使用它的生成器（显式地），通过Presburger算法中的公式，甚至作为计算机程序的正式模型产生的自动机或语法来表示。然而，简洁的表示可能会进一步增加复杂性，这意味着需要寻求折衷。然而，对于任何给定的表示形式，这就提出了最小化表示大小的问题。该项目着眼于在几个关键表示中半线性集的最小化和描述问题的经济性，其目标是找到(1)新的特征，(2)有效的最小化过程，以及(3)下界参数。表示大小的下界特别有趣：对于涉及不确定性选择的建模形式（例如自动机，以及更广泛的非确定性无限状态系统），获得表示大小的严格下界是一个众所周知的挑战。在目前的背景下，我们期望利用与逻辑和几何的联系，以及在理解普雷斯伯格算术方面的新发展，而不是在最小化和描述经济的背景下探索。我们将考虑几个复杂性度量，例如生成器表示中的比特数和集合数，自动机（如计数器自动机，寄存器机等）的状态数。我们还将能够利用无限状态系统验证理论的最新进展，例如向量加法系统可达性问题的非初等下界。

Semi-linear sets are a generalisation of ultimately periodic sets of integers to higher dimensions. They appear in a variety of Theoretical Computer Science topics; for instance, the Frobenius coin problem can be interpreted as the problem of finding the largest integer not contained in a given (1-dimensional) semi-linear set of a restricted form. In formal verification, the family of semi-linear sets forms a theoretical basis for a range of verification algorithms, by the virtue of coinciding with the family of sets definable in Presburger arithmetic, the first-order theory of the integers with addition and order. Periodic behaviour in software systems, especially those featuring concurrency, can often be captured by this logic, and then automated decision procedures (such as those implemented in satisfiability modulo theory solvers) pave the way for verification of these systems.Because of the high computational complexity of the underlying decision problems, this approach relies on small representations of inputs. Depending on the exact setup, the semi-linear set may be represented using its generators (explicitly), by a formula in Presburger arithmetic, or even as an automaton or grammar arising as a formal model of a computer program. Succinct representations may, however, bring the complexity further up, which means that a tradeoff needs to be sought. However, for any given representation formalism, this raises the question of minimising representation size.This project looks at minimisation and economy of description questions for semi-linear sets in several key representations, with the goals of finding (1) new characterizations, (2) efficient minimisation procedures, and (3) lower bound arguments. Lower bounds on representation size are of particular interest: for modeling formalisms that involve nondeterministic choice (such as automata, and non-deterministic infinite-state systems more widely) obtaining tight lower bounds on the representation size is a well-known challenge. In the present context, we expect to take advantage of the link to logic and geometry and of the new developments in the understanding of Presburger arithmetic, not explored previously in the context of minimisation and economy of description. We will consider several complexity measures, such as the number of bits and the number of sets in generator representation, the number of states of automata (such as counter automata, register machines, etc.). We will also be able to capitalise on recent advances in the theory of verification of infinite-state systems, such as the nonelementary lower bound for the reachability problem in vector addition systems.