We present an algorithm for the minimization of Buechi automata based on the notion of fair simulation introduced in [6], Unlike direct simulation, fair simulation allows flexibility in the satisfaction of the acceptance conditions, and hence leads to larger relations. However, it is not always possible to remove edges to simulated states or merge simulation-equivalent states without altering the language of the automaton. Solutions proposed in the past consisted in checking sufficient conditions [11, Theorem 3], or resorting to more restrictive notions like delayed simulation. By contrast, our algorithm exploits the full power of fair simulation by efficiently checking the correctness of changes to the automaton (both merging of states and removal of edges).
展开▼
