A pr 2 01 1 Büchi Automata can have Smaller Quotients

We study novel simulation-like preorders for quotienting n ondeterministic Büchi automata. We define fixed-word delayed simulation , a new preorder coarser than delayed simulation. We argue that fixed-w or simulation is the coarsest forward simulation-like preorder which can be us d for quotienting Büchi automata, thus improving our understanding of the li mits of quotienting. Also, we show that computing fixed-word simulation is PSPACE -complete. On the practical side, we introduce proxy simulations , which are novel polynomialtime computable preorders sound for quotienting. In partic ular, delayed proxy simulationinduce quotients that can be smaller by an arbitrarily large factor than direct backward simulation. We derive proxy simulations as the product of a theory of refinement transformers: A refinement transformer maps preorders nondecreasingly, preserving certain properties. We study und er which general conditions refinement transformers are sound for quotienting.