Sometimes an error in an algorithm reveals itself quickly, and sometimes it takes a very long time. The question is how to find the range in which the program can fail. A team with Polish computer scientists was awarded for solving this problem for the VASS model.
The Polish-German-British team of computer scientists received the award for the best work at the 50th edition of the International Colloquium on Automata, Languages and Programming (ICALP) 2023. The ICALP conference is divided into two paths: algorithmic and logical. This work is from the logical path. ICALP is one of the two most important logic conferences in theoretical computer science.
The paper (https://arxiv.org/abs/2305.01581) concerns error detection in algorithms. 'Our solution explains how good the algorithm for the coverability problem for the VASS model can be - both how fast it can work and how much time it needs to work properly,’ says Dr. Filip Mazowiecki from the University of Warsaw.
'If you write programs, you would like to check automatically whether any errors may occur as a result of their operation. As part of the computer science department I specialise in, formal verification, I deal with models that detect various types of errors,’ Mazowiecki says.
Firstly, the researchers wanted to show when an error can occur most quickly when running a given algorithm. And on the other hand - show how many steps you need to take to be sure that everything will go flawlessly. The idea was to find out how long the shortest and longest path to error would be.
The scientists used the Vector Addition Systems with States (VASS) model. Explaining what types of problems the algorithm deals with, Mazowiecki says: ‘Suppose we have five coordinates, each of them describing the number of people in a given room: the living room, bathroom, kitchen, hall and bedroom. In the next steps, different people enter the apartment and move around the rooms (so-called transitions) according to specific rules (this is VASS). For example, the apartment can only be entered through the hall, from the kitchen you can go to the living room, but not to the bedroom, etc. There are a number of passages between rooms. The problem of coverability is that we want to detect a transition that complies with the rules, but is an undesirable one - it is an error. Such an error may be, for example, a situation in which two (or more) people are in the bathroom at the same time (and in other rooms - it doesn't matter). The beginning of the path that the scientists studied would be the entrance of the first person into the apartment, and the end of the path - the entrance of a person to an occupied bathroom. So we check how many moves have to be made before we are sure that the fastest possible error can occur. And how far from the start an undesirable situation can be.’
She continues: ‘This is a simplified example of course, but algorithms operating according to similar rules can be useful, for example, when dividing tasks between computers or processors. It is conceivable that an error will occur if two computers simultaneously attempt to perform the same task. So it is good to be able to anticipate if such a situation may occur and when. There may be a huge number of steps before an error occurs, but it is still possible.’
In the 1970s, the complexity of the VASS algorithm was studied in terms of memory, i.e. what minimum computer memory was needed to solve the problem. The team from Poland and Germany showed how complex this algorithm was when it comes to time.
The work has five co-authors from two mathematical backgrounds - logicians and algorithmicians (they represent two paths of ICALP). Using ideas from both areas of mathematics, the researchers found a solution to the problem. 'Research on the border of areas is different - either no one understands it and it ends up in the trash, or it is appreciated for being innovative,’ says Mazowiecki.
She adds: ’I think we just did it very neatly. For people who know the subject, the problem is quite natural and not difficult to understand, and the presentation of the solution is clear and nice.’
When asked about the possible applications of this work, the scientist points out that this is a theoretical result.
'Formal verification should, by definition, answer the questions why something works and why it doesn't, where the errors are. When it comes to issues such as machine learning, sometimes you hear that these algorithms work, but no one knows why and if there are errors. And indeed, they work fast because they are inaccurate. The problem with using formal verification methods is that it slows down the computing.
'My doctoral candidate, which also dealt with formal verification, has moved to the private sector and implements solutions related to such issues,’ says Mazowiecki.
He concludes that perhaps research in this area will not be directly used to solve the humanity's problems. But not every work is meant to serve that purpose. This is more of an aesthetic issue. 'Our work can be compared to writing books. However, our work is not for the mass audience, but a completely different target group,’ he says.
The authors of the award-winning paper are: Marvin Künnemann (RPTU Kaiserslautern-Landau, Germany), Filip Mazowiecki (University of Warsaw, Poland), Lia Schütze (Max Planck Institute for Software Systems, Germany), Henry Sinclaire-Banks (University of Warwick, England) and Karol Węgrzycki from (Saarland University, Germany, previously did his PhD at the University of Warsaw).
PAP - Science in Poland, Ludwika Tomala
lt/ agt/ kap/
tr. RL
