[M.Sc. Laboratory] Reducing the Size of Büchi Automata
| Course type | Master Laboratory |
|---|---|
| Instructors | Matthias Heizmann |
| Credits | Depending on course type |
| Course Catalog | |
| Note |
For a regular language L there is a minimal deterministic finite automaton which recognizes L. Given a deterministic finite automaton A we can always compute this minimal deterministic automaton that recognizes the language of A.
For ω-regular language there is no analogous notion of a minimal Büchi automaton. However for some Büchi automata we can reduce the size of the automaton. We will develop an algorithm for this task.
| Input: Büchi Automaton A Output: Büchi Automaton A' such that L(A)=L(A') and the size of A' is not greater than the size of A. |
Result:
- We generalized the minimization algorithm for deterministic finite automata to an algorithm that reduces the size of nondetermnistic finite automata and Büchi automata.
- We took the algorithm for state space reduction of Büchi automata based on delayed simulation which was presented in the following paper. Kousha Etessami, Thomas Wilke, Rebecca A. Schuller: Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata. SIAM J. Comput. (SIAMCOMP) 34(5):1159-1175 (2005) We developed an optimized version of this algorithm where generate the progress measures of each strongly connected component of the game graph separately.
We implemented both approaches in our automata library.