Feedback

Faculté des Sciences appliquées
Faculté des Sciences appliquées
MASTER THESIS
VIEW 42 | DOWNLOAD 3

Master thesis : Implementation of Automata over Linear Orderings

Download
Gualtieri, Pauline ULiège
Promotor(s) : Boigelot, Bernard ULiège
Date of defense : 4-Sep-2023/5-Sep-2023 • Permalink : http://hdl.handle.net/2268.2/18159
Details
Title : Master thesis : Implementation of Automata over Linear Orderings
Translated title : [fr] Implémentation d'Automates sur Ordres Linéaires
Author : Gualtieri, Pauline ULiège
Date of defense  : 4-Sep-2023/5-Sep-2023
Advisor(s) : Boigelot, Bernard ULiège
Committee's member(s) : Fontaine, Pascal ULiège
Rigo, Michel ULiège
Language : English
Number of pages : 58
Keywords : [en] automaton
[en] linear orderings
[en] automata over linear orderings
[en] LASH
Discipline(s) : Engineering, computing & technology > Computer science
Institution(s) : Université de Liège, Liège, Belgique
Degree: Master en sciences informatiques, à finalité spécialisée en "computer systems security"
Faculty: Master thesis of the Faculté des Sciences appliquées

Abstract

[en] 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.


File(s)

Document(s)

File
Access Implementation of Automata over Linear Orderings.pdf
Description:
Size: 640.6 kB
Format: Adobe PDF
File
Access Implementation of Automata over Linear Orderings - Abstract.pdf
Description: The abstract of the master's thesis
Size: 81.03 kB
Format: Adobe PDF

Annexe(s)

File
Access Implementation of Automata over Linear Orderings - Code.zip
Description: Zip archive including the LASH toolset with the implementation of automata over linear orderings and a readme file specifying which files are related to this work
Size: 1.32 MB
Format: Unknown

Author

  • Gualtieri, Pauline ULiège Université de Liège > Master sc. informatiques, à fin.

Promotor(s)

Committee's member(s)

  • Fontaine, Pascal ULiège Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Systèmes informatiques distribués
    ORBi View his publications on ORBi
  • Rigo, Michel ULiège Université de Liège - ULiège > Département de mathématique > Mathématiques discrètes
    ORBi View his publications on ORBi
  • Total number of views 42
  • Total number of downloads 3










All documents available on MatheO are protected by copyright and subject to the usual rules for fair use.
The University of Liège does not guarantee the scientific quality of these students' works or the accuracy of all the information they contain.