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
10.4 Semi-Deterministic Büchi Automata
10.5 From semi-deterministic Büchi to deterministic Muller

Chapter 11. Infinite Games

Sections	Exercise
11.1 Infinite Games (Basic Definitions)
11.2 Reachability Games
11.3 Büchi Games
11.4 Parity Games
11.5 Muller Games
11.6 A Remark on Undetermined Games

Chapter 12. Rabin’s Theorem

Sections	Exercise
12.1 Tree Automata and Acceptance Game
12.2 Emptiness Game
12.3 Complementation of Parity Tree Automata

Chapter 13. Application: CTL Model Checking

---

Next chapter:

Further Reading: