Master thesis : Implementation of Automata over Linear Orderings

Abstract

The goal of this master's thesis was to implement a data structure able to represent automata over linear orderings and operations over them, in the framework of the LASH (Liège Automata-based Symbolic Handler) toolset. We first introduce the basic notions used throughout the work such as linear orderings, words, automata over finite words and infinite words. We then add the notions of left and right limit transitions in order to reach the definition of automata over linear orderings as described by Olivier Carton and Véronique Bruyère. The operations of intersection and union are presented and some potential additional operations to be implemented in the future are mentioned. We explain our solutions for the operations of intersection and union through two simplified algorithms to showcase their main principles. Two examples then demonstrate, with a representation of the stack and hash table, how those algorithms behave. The implementation of the data structure and operations was done in the C language just as the base code of LASH. To implement the intersection and union operations, some challenges had to be faced. The first one was how to handle the states that are made accessible by limit transitions while exploring the two input automata in the operations of intersection and union. We proposed a solution using a loop over a stack that keeps track of states with unexplored transitions, together with a hash table keeping track of states already added to the automaton. For each loop, the limit transitions are checked to find out if we can add them to the output automaton. We also explain how we handled left limit transitions in an efficient way using a counter to avoid pointless computations. The structures that we used to implement automata over linear orderings are presented by providing the detailed pseudo-code of the implementation of our solution. As the final step in our work, tests were made on both operations to find out their limitations. The last tests involved automata with large numbers of states and limit transitions, both left and right. The results show that the operations of intersection and union have little difference in performance for the same set of input automata. In the case of two input automata with many limit transitions, we find that the program is rapidly running out of memory as the structures necessary for keeping track of possible limit transitions increase exponentially in size. The implementation of this work has room for improvements in terms of performance. Some possible ideas for improvements are discussed as a final word.