vix.ing · top · new · best · stats · spec

Minimization of Büchi Automata using Fair Simulation

2016/03/03 by Daniel Tischner, Tischner, Daniel
Computer Science · #Data Structures and Algorithms (cs.DS) #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic, programming, and type systems #cs.DS #cs.FL #semigroups and automata theory

paper · pdf · doi:10.48550/arxiv.1603.01107

Bachelor's thesis, 67 pages, 12 figures

arxiv created 2016/03/03 · openalex publication_date 2016/03/03 · arxiv updated 2016/03/04 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

We present an algorithm, which reduces the size of Büchi automata using fair simulation. Its time complexity is O(|Q|4 ⋅ |Δ|2), the space complexity is O(|Q| ⋅ |Δ|). Simulation is a common approach for minimizing ω-automata such as Büchi automata. Direct simulation, delayed simulation and fair simulation are different types of simulation. As we will show, minimization based on direct or delayed simulation is conceptually simple. Whereas the algorithm based on fair simulation is more complex. However, fair simulation allows a stronger minimization of the automaton. Further, we illustrate the theory behind the algorithm, cover optimizations useful in practice, give experimental results and compare our technique to other minimization strategies.

Citations

Related