Using mathematics to hunt for computer errors

Security gap in application discovered, update urgently recommended. Alerts like that can confront us every week. Often, a comprehensive update that addresses teething troubles is already offered when a new programme is launched. This creates manifold problems, and public entities as well as businesses are often exposed to attacks by hackers. Software is used in a growing number of sensitive areas where a computer failure might even be life threatening. It has to be noted that not all fields are affected in the same way, many computer systems run as unfailingly as the proverbial Swiss clockwork. While hardware is usually very reliable, it is the software component that may create problems.

Mathematics improve computer systems

Complex programmes actually make it very difficult to foresee every eventuality. While computer methods for testing software exist, the complexity of applications has been steadily increasing in recent years. The performance of test methods lags behind, particularly in terms of their speed – a good incentive to invest in basic research in this field. In a recently completed project funded by the Austrian Science Fund FWF, the computer scientist Krishnendu Chatterjee analysed computer systems with the help of mathematical methods with hope of providing significant improvements in this sector.

Graph theory

“This field has a long-standing tradition”, says Chatterjee. “Researchers have long been trying to find a formal basis for designing correct systems. Fundamental developments in this area go back to the 1960s, like the work by Alonzo Church, one of the founding fathers of computer sciences.” For the mathematical analysis of computer systems, scientists use what is called ‘graph theory’, which deals with objects that can be characterised as networks of interconnected points or vertices. Computer systems can be mathematically described as graphs, with a vertex representing a certain state of the system and an edge representing a transition between two states. A computer displaying this text, for instance, is in a defined state represented as a vertex. When the user clicks on a link, the system changes to another state, and this transition is shown as an edge.

Improved graph algorithms

This method is particularly suited for the verification of computer systems. Chatterjee was interested in how fast these verification algorithms work. “Computer systems are getting more complex all the time”, the computer scientist notes. “In some algorithmic problems in verification development has been stagnating since the 1990s. A new aspect of this project was to use cutting-edge approaches from graph theory to improve the algorithms. That was a completely new line of attack.” Chatterjee emphasises the significance of his cooperation with his project partner Monika Henzinger from the University of Vienna. “For me, that was an intensive learning process. It was intriguing to see how the methods of graph algorithms need to be adapted and expanded in order to arrive at better algorithms for the problems we studied.”

Limits, conditions, successes

In that respect, the project was very successful: several speed limits for certain verification algorithms were broken for the first time since the 1990s, for instance involving so-called ‘Markov decision processes’, which are models containing several options and an element of randomness. “One example for that would be the development of robots”, explains Chatterjee. “A robot interacts with an environment which includes uncertainties and it has several options, such as veering to the left or to the right. Markov decision processes provide a model for that.” For many applications it is essential to predict in such a model what events will occur with certainty. “The most efficient algorithm for addressing that problem available till now dated back to 1995 and had quadratic complexity”, notes Chatterjee. This means that the runtime of the algorithm increases quadratically with the size of the system being verified – hence, a system double in size requires fourfold runtime. “In our project we were able to overcome this limit by using graph algorithm techniques.” Chatterjee is very pleased with the success of the project. “Our two doctoral students, Sebastian Krinninger and Martin Chmelik, also did excellent work, both received prizes for their dissertations”, notes Chatterjee. Despite the topical relevance of the subject he underlines that his was a pure basic research project. “Our first project was very theoretical. Now we are trying to explore limits or conditions to see how hard it is going to be to improve our algorithms further. At the same time we want to see how these approaches can be translated into practice.”

Personal details

Krishnendu Chatterjee is a professor at the IST Austria (Institute for Science and Technology) in Klosterneuburg. His research focus is on computer-aided verification and game theory.

Publications

Krishnendu Chatterjee and Monika Henzinger: „Efficient and Dynamic Algorithms for Alternating Büchi Games and Maximal End- Component Decomposition“, in: JACM, volume 61, 15 pages 1-40, 2014.

Monika Henzinger, Sebastian Krinninger, and Danupon Nanongkai: 
„Dynamic Approximate All-Pairs Shortest Paths: Breaking the O(mn) Barrier and Derandomization“,
Conference FOCS (Foundations of Computer Science), 26 Oct 2013, pages 538-547. IEEE.

Krishnendu Chatterjee and Martin Chmelik: 
„POMDPs under probabilistic semantics“, in: Artificial Intelligence, volume: 221, pages 46-72, Feb 23, 2015. Conference version UAI (Uncertainty in Artificial Intelligence), Aug 11, 2013