You are here: Home Finished [Varies] Minimization … Minimization of Nested Word …

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
Course Catalog

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.

even-odd.png

 

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.

Approach1-FiniteAutomata.png

 

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.

 Approach2-PushdownAutomata.png

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.

Approach3-VisibleyPushdownAutomata.png

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.

Approach4-NestedWordAutomata.png

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.

NestedWord.png

Minimization

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.

Literature

[1] Rajeev Alur's nested word automata website

[2] Congruences for visibly pushdown languages; Alur, Kumar, Madhusudan, and Viswanathan; ICALP 2005.

[3] Patrick Chervet, Igor Walukiewicz: Minimizing Variants of Visibly Pushdown Automata. MFCS 2007:135-146