Minimization of Nested Word Automata
|Course type||B. Sc. Thesis, M.Sc. Praktikum, M.Sc. Teamproject
|Instructors||Matthias Heizmann, Christian Schilling
|Credits||Depending on course type
Nested Word Automata (brief)
From theoretical computer science we know that finite automata are not sufficient to recognize the language of palindromes or to describe the control flow of a program with procedure calls, like the the following recursive program.
Consider the following approach to model the control flow of this program via a finite automaton. The depicted word corresponds to a run of the automaton, however in a model of the even-odd program we want that for each return there is a corresponding call.
We can model the control flow of the even-odd program using a pushdown automaton. However, context free languages are not closed under complement and intersection. Which are desired operations e.g. in model checking.
A solution could be the use of visibly pushdown automata. The class of languages recognized by visibly pushdown automata are called visibly pushdown languages. Visibly pushdown languages are closed under intersection and complementation, e.g. the language of palindromes is a visibly pushdown language and the following visibly pushdown automaton is suitable to model the control flow of the even-odd program.
An other solution is the use of nested word automata. Nested word automata are similar to visibly pushdown automata but some complexity is shifted from the automaton to its input.
Opposed to a visibly pushdown automaton a nested word automaton does not have a stack. The input of a nested word automaton is not a word, but a nested word. A Nested word is a word with a hierarchical relation. In the even-odd example we can use this relation to express call return pair belongs together.
There are known minimization algorithms for finite automata. There are minimization algorithms for variants of visibly pushdown automata [2,3]. In this project we will examine these algorithms and develop a minimization algorithm for nested word automata.
Depending on the course type you will adapt a basic algorithm, optimize it or extend the algorithm to automata over infinite words.