Reachability problems for words, matrices and maps: Algorithms and Complexity

在计算机科学中，可达性是一个基本问题，它起源于可计算性理论中第一个不可判定的决策问题——图灵机中的终止/停止问题：“给定一个任意计算机程序的描述，决定该程序是结束运行还是继续永远运行”或“给定一个程序和一个输入，决定该程序最终在输入时停止运行，还是将永远运行”。在现代世界，软件无处不在（在几乎所有的设备中，包括电话、汽车、飞机等）。可达性问题的解决方案：“确定特定代码段是否会达到不良状态，是否可以避免某些执行路径或最终会终止”是验证工具的核心组成部分，它可以保证代码的可靠性和复杂技术设备的正确功能。本项目拟开展的研究主要集中在词语、矩阵、迭代图等经典数学对象的可达性问题的研究，旨在解决数学和计算机科学中具有挑战性和根本性的长期开放性问题，这些问题也出现在物理、化学、生物、生态、自然过程的分析中。该项目的主要目标是证明，通过将计算理论、数论、代数和组合学的技术结合应用于词，有可能大大超越与矩阵半群、迭代映射和相关词问题中的可达性问题相关的已知结果。我们在这个研究项目中的主要目标是：识别具有可确定可达性问题的单词、矩阵和地图的新类，为可确定的情况设计有效的算法，并估计其计算复杂性。首先，我们提出研究涵盖原本独立但密切相关的开放问题的广义模型，并研究它们之间的约简。在此基础上，提出了以下三种解决方法：研究可达集的拓扑性质及其在可达性分析中的应用；矩阵可达性问题转化为词的组合问题和计算问题并设计了基于投影法的高维可达问题半算法，其中无限可达集可以映射成各种有限结构，并保留了部分可达性质。该项目的结果将是双重的。关于矩阵和映射的可达性问题，我们期望通过将计算复杂性理论、自动机和形式语言、代数、数论和组合语言等技术结合起来，获得与开放问题相关的新的深层次结果。在更普遍的层面上，我们期望建立新的研究方向，将数学中的挑战性问题与理论计算机科学结构、方法和结果联系起来。间接和长期受益者的名单不仅限于软件验证技术和算法的开发人员，而且还包括物理，化学，生物学，环境科学和经济学方面的各种专家，这些专家需要有效的工具来预测由矩阵和矩阵乘积表示的复杂系统的行为。

In computer science the reachability is one of the fundamental problems taking its roots from the first undecidable decision problem in the computability theory - termination/halting problem in Turing Machine: "Given a description of an arbitrary computer program, decide whether the program finishes running or continues to run forever" or "Deciding, given a program and an input, whether the program will eventually halt when run with that input, or will run forever". In the modern world software is now everywhere (in almost all devices including phones, cars, planes, etc ). The solution of the reachability problem: "Deciding whether a particular piece of code will reach a bad state, can avoid some execution path or will eventually terminate" is the core component of the verification tools that can grantee the reliability of the code and correct functionality of complex technological devices. The proposed research of this project is mostly in the study of reachability problems for classical mathematical objects such as words, matrices, iterative maps and aims to get a progress with a solution of challenging and fundamental long standing open problems in mathematics and computer science, which also appear in the analysis of natural processes in physics, chemistry, biology, ecology, economics etc.The primary goal of this project is to demonstrate that it is possible to go significantly beyond known results related to reachability problems in matrix semigroups, iterative maps and related word problems by applying a combination of techniques from computational theory, number theory, algebra and combinatorics on words. Our principal objectives within this research programme are: identifying new classes with decidable reachability problems for words, matrices and maps, designing efficient algorithms for decidable cases and estimating their computational complexity. First, we propose to study generalized model that cover originally independent, but closely related open problems and investigate the reductions between them. Then we suggest following three approaches to get a better understanding of the core problems: investigation of topological properties of the reachability sets and their application for reachability analysis; translation of matrix reachability problems into combinatorial and computational problems on words; and the design of semi-algorithms for reachability problems in higher dimensions based on projection methods, where infinite reachability set can be mapped into various finite structures which preserve some of the reachability properties. The result of the project would be twofold. In relation to reachability problems for matrices and maps, we expect that new deep results related to open problems will be obtained by applying a combination of techniques from computational complexity theory, automata and formal langauges, algebra, number theory and combinatorics on words. At a more general level we expect to establish new direction of research connecting challenging problems in mathematics with theoretical computer science structures, methods and results.The list of indirect and long-term beneficiaries is not limited to developers of software verification techniques and algorithms, but also includes a variety of specialists in physics, chemistry, biology, environmental sciences and economics which require efficient tools for predicting the behaviour of the complex systems represented by matrices and matrix products.