Automata, Games, and Verification (Portal)

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

Sections	Exercise
5.1. Infinite Directed Acyclic Graph (DAG)
5.2. Ranking of DAG
5.3. Complement Büchi Automaton with Odd Ranking

Chapter 6. Logics over Infinite Sequences

Sections	Exercise
6.1. Linear-Time Temporal Logic (LTL)
6.2. Expressing Program Properties using LTL
6.3. LTL and Counting Languages
6.4. Quantified Propositional Temporal Logic (QPTL)
6.5. Monadic Second-Order Logic of One Successor (S1S)
6.6. Express QPTL using S1S
6.7. S1S$_0$ and Büchi-recognizable LanguageBüchi-recognizable

Chapter 7. Alternating Büchi Automata

Sections	Exercise
7.1. Alternating Büchi Automata
7.2. From LTL to Alternating Büchi Automata	$\varphi=(\Diamond p)\ \mathcal{U}\ (\square q)$
7.3. Translating Alternating to Nondeterministic automata

Chapter 8. Linear Arithmetic

Sections	Exercise
8.1. Linear Arithmetic (Theory)
8.2 Encoding real numbers
8.3 Translation from Linear Arithmetic to Automata
8.4 Homogenous Inequality Testing is Automatic
8.5 From Linear Arithmetic to Automata

Chapter 9. LTL Model Checking

Sections	Exercise
9.1 Automata-based LTL Model Checking with Sequential Circuits
9.2 Nested depth-first search
9.3 The Emerson-Lei algorithm

Chapter 10. McNaughton’s Theorem

Sections	Exercise
10.1 The Muller Acceptance Condition
10.2 From Büchi automata to Muller automata
10.3 Closure Properties of Muller Automata under Boolean Operations

---

Next chapter:

Further Reading: