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
9.2 Model Checking Sequential Circuits

---

Next chapter:

Further Reading:

---

Please cite the source for reprints, feel free to verify the sources cited in the article, and point out any errors or lack of clarity of expression. You can comment in the comments section below or email to GreenMeeple@yahoo.com