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

半线性集和无限状态系统的最小化问题

• 批准号: 2436353
• 金额: --
• 依托单位: University of Warwick
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2020
• 资助国家: 英国
• 起止时间: 2020 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2436353
• 关键词: Minimisation; questions; semi; linear; sets

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.

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