GreenMeeple

This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner

Chapter 1. Introduction

Sections	Exercise
1.1. Model Checking
1.2. Synthesis
1.3. The Logic-Automata Connection

Chapter 2. Büchi Automata

Sections	Exercise
2.1. Preliminaries
2.2. Automata over Infinite Words
2.3. The Büchi Acceptance Condition

Chapter 3. Büchi’s Characterization Theorem

Sections	Exercise
3.1. Kleene’s Theorem
3.2. $\omega$-regular language
3.3 Closure Properties of the Büchi-recognizable languages (Intersection and Union)
3.4 Closure Properties of the Büchi-recognizable languages (Concatenations)
3.5 Büchi’s Characterization Theorem

Chapter 4. Deterministic Büchi Automata

Sections	Exercise
4.1. Deterministic vs. Nondeterministic Büchi Automata
4.2. Complementation of deterministic Büchi Automata

Chapter 5. Complementation of Büchi automata