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.

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.

New algorithms for solving reachability problems for matrix semigroups and iterative maps can be directly incorporated into software verification tools and could have significant impact on predictability of systems for which verification tools were not previously known.

On the other hand the list of indirect and long-term beneficiaries is not limited to developers of software verification techniques and algorithms, but also include a variety of specialists in physics, chemistry, biology, environmental sciences and economics which require efficient tools for predicting the behaviour of the complex systems.
The reachability questions in matrix semigroups and iterative maps appear in
- qualitative biological models, which describe species (e.g. protein) interactions in terms of promotion or inhibition;
- population dynamics and epidemiology, which using matrix algebra and mathematical modelling for predicting and control of the population growth, infectious diseases and epidemic;
- ray tracing analysis in optics, where the tracing of a light path through the system can be performed by multiplying 2x2 matrices describing elements (lenses, mirrors, prism, etc.) of the optical system;
- quantum computations, where quantum logic gates are represented by unitary matrices and the changes of the quantum state are represented by matrix products;
they also appear in many other areas such as control theory, topology, cryptography, robotics, computer graphics, quantitative chemical analysis, etc.

Translation of results in an accessible format, collaboration and knowledge exchange are key activities that are proposed to ensure that potential beneficiaries have the opportunity to engage with project results. In addition to that standard dissemination such as publication of journal papers, presentation of conference papers and tutorials will ensure that potential beneficiaries will have access to the algorithms and new methods for solving reachability problems for matrices and iterative maps.