« November 2017 »
November
MoTuWeThFrSaSu
12345
6789101112
13141516171819
20212223242526
27282930
Uni-Logo
You are here: Home Teaching Student Projects and Thesis Topics Finished [Varies] Minimization of Nested Word Automata
Document Actions

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



 

 

Personal tools