Automata on Infinite Structures

In this course unit, we deal with a fraction of automata theory that is applied when it comes to representing behaviours of reactive systems (OS, communications protocols, control systems, etc.). The common abstraction of the indefinite running time of such systems is the assumption that they run forever, leading to automata models operating on infinite sequences or trees. We will explore different equivalent models of automata on infinite words, namely Büchi, Muller, and Rabin Automata. We will learn how to manipulate them algorithmically, and explore their relation to logic, in particular to the monadic second-order logic of one successor. Finally, we will look at what changes, when these automata are applied to infinite trees rather than infinite words.
 

Learning Outcomes: 

After the completion of this course unit, the student will:

  • know how to manipulate automata algorithmically
  • be able to relate set operations to operations on the automaton level
  • understand the limited expressiveness of finite-state automata
  • see the link between logic and automata
  • know how to exploit automata and logic to express properties of systems
     
Type: 
Course
Semester: 
S2017
ECTS: 
5
Tracks: 
Lecturer: 
Site: 
F
Code: 
43024
Language: 
english
Period: 
weekly
Schedule: 
Wednesday: 9:15 - 12:00
Location: 
UniFR, PER21
Room: 
F207
Evaluation type: 
oral exam
Comment: 

First Lecture
The first lecture will take place on Wednesday, 22.02.2017 at 09:15 in UniFR, PER21, room F207.

ILIAS
The course page in ILIAS can be found at https://ilias.unibe.ch/goto_ilias3_unibe_crs_1006984.html.