Abstract: Optimizing Buchi automata is an important step in efficient model checking for linear-time specification. In this paper we compare among three notions of simulation： direct, delay, and fair. We study simulation relations as a tool for minimizing automata.

Key words: Simulation, Automata, Minimization