# Automata Theory

## Announcements

- 3/16/2015: Room for Make-up Exam. Date for results inspection of exam.
- 03/11/2015: Date for Make-up Exam
- 02/02/2015: ROOM CHANGE: exam will talk place in Room V U104 at Lehrturm!
- 27/12/2014: Written exam scheduled for 03/02/2015 10:00am Room: V U104 (was: V005 (Tuesday's class room))
- 11/04/2014: add link to MONA tool
- 10/27/2014: update of dates
- 10/16/2014: room change announcement
- 09/29/2014: first version of english homepage

## Contents

This course covers the theory of finite automata acting on infinite strings or trees. The main application of these automata is for designing decision procedures for formal logics.

Keywords: Büchi-Elgot Theorem, Presburger Arithmetic, LTL, XML, Rabin's Tree Theorem, modal µ-calculus

This course uses the textbook Automatentheorie und Logik (in German language). The lecture notes from 2010 are freely available.

Lectures will be given in English; depending on the audience we may also provide English course notes.

## Organization

**Volume:**3+2 academic hours per week, 6 ECTS**Lecture:**Prof. Dr. Martin Hofmann**Tutorials:**Gordon Cichon

## Place and Time

Session | Time | Begin | |
---|---|---|---|

Lecture | Tues, 10am-12pm | V005 (Lehrturm, Prof.-Huber-Pl. 2) | 7.10.2014 |

Lecture | Thur, 2pm-4pm | AU 117 (HGB, Geschwister-Scholl-Platz 1) | 9.10.2014 |

Tutorial | Mon, 12pm-2pm | 218 (Amalienstr. 73A) | 13.10.2014 |

Since there are 4 academic hours per week, and the course itself is only 3 hours per week, there will be **no** lecture on the following dates: week from Oct. 20th till Oct 31st. From Dec 22nd till Jan 15th.

Type/# | Date | Topic | Sections in textbook | Notes |

L1 | Oct. 7th | Revision of regular languages and finite automata | 1.1.1, 1.1.2 | |

L2 | Oct. 9th | Deterministic finite automata. Decision problems for finite automata. | 1.1.3 | |

T1 | Oct. 13th | Introduction to finite automata | Exercise sheet 1 in Uniworx | |

L3 | Oct. 14th | Weak monadic second-order logic (WMSO): syntax and semantics. | 2.1 2.2 | |

L4 | Oct. 16th | Decision procedure for WMSO, | 2.2 | |

T2 | Oct. 20th | wMSO formulae and finite automata | Exercise sheet 2 in Uniworx | |

T3 | Oct. 27th | |||

T4 | Nov. 3rd | wMSO formulae and finite automata | Exercise sheet 2 in Uniworx | |

L5 | Nov. 4th |
the tool MONA, definition of large models in WMSO Mona files: even.mona adder.mona binary.mona dist.mona |
2.3 2.4 (definition of "distnpluseins") | |

L6 | Nov. 6th | Complexity of the decision problem for WMSO. Presburger arithmetic | 2.4 2.5 | |

T5 | Nov. 10th | TBA | ||

L7 | Nov. 11th | Büchi Automata, w-regular languages | 5.1 5.2 first part | |

L8 | Nov. 13th | w-regular languages the same as Büchi recognizable, deterministic Büchi automata weaker than nondeterministic ones. | 5.2 second part | |

T6 | Nov. 17th | TBA | ||

L9 | Nov. 18th | Complementation of Büchi automata | 6 | |

L10 | Nov. 20th | Complementation of Büchi automata cont'd, other acceptance conditions | 7 | |

T7 | Nov. 24th | TBA | ||

L11 | Nov. 25th | other acceptance conditions cont'd. Determinisation of automata on infinite words. Motivation, preliminary considerations. | 7 8.1 | |

L12 | Nov. 27th | Determinisation of Buchi automata wth Safra Construction | 8.2 | |

T8 | Dec. 1st | TBA | ||

L13 | Dec. 2nd | Correctness of Safra construction, Piterman construction | 8.2 8.3 | |

L14 | Dec. 4th | Algorithms for automata on infinite words. Size-change termination | 9.1 9.3 | |

T9 | Dec. 8th | TBA | 11 | |

L13 | Dec. 9th | Automata on finite trees | 12 | |

L16 | Dec. 11th | Automata on finite trees, cont'd. | 12 | |

T10 | Dec. 15th | TBA | ||

L17 | Dec. 16th | Applications: higher-order matching, XML | 13 | |

L18 | Dec. 18th | Automata on infinite trees, parity games (definition) | 14, 15.1 | |

T11 | Jan. 12th | TBA | ||

T12 | Jan. 19th | TBA | ||

L19 | Jan. 20th | Solution of parity games, positional determinacy. | 15.1 | |

L20 | Jan. 22nd | Complementation of parity tree automata, Rabin's theorem. | 15.2 | |

T13 | Jan. 26th | TBA | ||

L21 | Jan. 27th | Synthesis of reactive systems with parity games (Pnueli's theorem), modal mu-calculus | 16.3 | |

L22 | Jan. 29th | Slack, revision. |

Legend: L means lecture, T means tutorial.

**Tutorials**

Exercises and problem solving sessions will be available on Uniworx. There will be points on successful homeworks which can be used to improve grading in the finals.

**Material**

- Lecture notes from 2010
- Homepage of MONA tool

**Exams**

### Exam

The exam will talk place on 03/02/2015 at 10:00am in Room V U104 at Lehrturm (close to Tuesday's lecture room). Inspection of exam results will be possible on 03/31/2015 between 9am and 10am in room E109.

### Make-up Exam

The make-up exam will talk place on 04/15/2015 between 4pm and 6pm in room V 005 at Lehrturm, Prof.-Huber-Platz 2.

## More Information

- There is a student discussion about this lecture in German on the following web site: die-informatiker.net.

Document Actions