Minimization of B\"uchi Automata using Fair Simulation

TL;DR

This paper introduces a new algorithm for minimizing B"uchi automata using fair simulation, achieving stronger reduction than previous methods with detailed theoretical and experimental analysis.

Contribution

The paper presents a novel algorithm for B"uchi automata minimization based on fair simulation, offering improved reduction capabilities and practical optimizations.

Findings

The algorithm has a time complexity of O(|Q|^4 * |Δ|^2).

Fair simulation allows stronger minimization than direct or delayed simulation.

Experimental results demonstrate the effectiveness of the proposed method.

Abstract

We present an algorithm, which reduces the size of B\"uchi automata using fair simulation. Its time complexity is $\mathcal{O}(|Q|^4 \cdot |\Delta|^2)$, the space complexity is $\mathcal{O}(|Q| \cdot |\Delta|)$. Simulation is a common approach for minimizing $\omega$-automata such as B\"uchi 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.