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.
|