FIT student Barbora Šmahlíková wins another prestigious award

Barbora Šmahlíková is collecting one award after another for her bachelor thesis in the field of stream automation. After the Government Prize for a Gifted Student, the Vienna Center for Logic and Algorithms awarded her the prestigious international prize "The Outstanding Undergraduate Thesis Award" for the world's best undergraduate thesis in the field of formal methods.

What does Barbora do?

Unless you are an IT expert, you probably don't know what stream automation is. It is a mathematical model behind, among other things, the techniques that ensure that critical programs (e.g., control systems in aircraft, automobiles, satellites, etc.) are free from errors that could cause a catastrophic accident.

Very simply, a programmer can check that a program is error-free by taking two dictionaries. One dictionary will contain words that describe all possible behaviours of the program (in this case, the word will contain letters representing different events in the program, such as function calling, sending a signal to eject the pilot, operations with variables, etc.) and the other dictionary will contain words that describe all correct behaviours of the program. The task is to check whether all the words from the first dictionary are included in the second dictionary. For one simple word, it's straightforward. In our case, however, both dictionaries contain an infinite number of words of infinite length, which complicates the situation considerably. Stream automation just allows the description of such infinite dictionaries of infinite words. Verifying the correctness of the system then corresponds to verifying the set inclusion between these dictionaries.

Fig. 1 An example of the complement of the Büchi automaton using the algorithm of Section V. Havleny, O. Lengál and B. Šmahlíková "Sky Is Not the Limit: Tighter Rank Bounds for Elevator Automata in Büchi Automata Complementation"; TACAS 2022. Red states (and the states that would follow from them) will not be generated due to the optimizations in place.

What is the contribution of Barbora's work?

One of Barbora's contributions is the optimization of what is termed the rank-based complementation algorithm. This basic algorithm is theoretically optimal: in the worst case, its output will be an automaton with O((0,76n)^n) states (where n is the number of states of the input automaton). Which is also the lower limit (i.e. there are input automations for which a smaller complement cannot exist). In practice, however, this drastic complexity can often be avoided. The expression (0.76n)^n corresponds, in simplified terms, to the number of possible surjections on the n-element set (it is an approximation of the so-called Stirling number of the second kind used in combinatorics), which is the structure used in the algorithm. 

Based on the structural properties of the input automaton (namely, on the basis of its decomposition into strongly connected components and their analysis, i.e., finding out whether they are deterministic or inherently weak components), the optimization, which Barbora participated in the development of, can reduce the size of the domain of surjection values and thus combinatorially reduce the size of the generated automaton.

Scientific work since the beginning of her studies

Barbora started her research in the 2nd year of her Bachelor's degree in the Project Practice course with Vojtěch Havlena and Ondřej Lengál from the VeriFIT group. In September, she will be entering the second year of her master's studies. During these three years, she has contributed significantly to four papers presented at international conferences, three of which are considered to be at the cutting edge of the field.

The significance of the award is reflected in the fact that the Vienna Center for Logic and Algorithms (VCLA) is one of the most prestigious organizations in the world dealing with logic and formal methods. This is the seventh year that the award has been given for the best bachelor's and master's thesis in the field of formal methods.