B\"uchi Automata can have Smaller Quotients

TL;DR

This paper introduces new simulation preorders for quotienting nondeterministic B"uchi automata, including fixed-word delayed simulation and proxy simulations, advancing theoretical understanding and practical methods for automata minimization.

Contribution

It defines fixed-word delayed simulation as the coarsest simulation preorder suitable for quotienting B"uchi automata and introduces proxy simulations that are polynomial-time computable and can produce significantly smaller automata.

Findings

Fixed-word simulation is PSPACE-complete to compute.

Proxy simulations are polynomial-time computable and sound for quotienting.

Proxy simulations can produce arbitrarily smaller quotients than backward simulation.

Abstract

We study novel simulation-like preorders for quotienting nondeterministic B\"uchi automata. We define fixed-word delayed simulation, a new preorder coarser than delayed simulation. We argue that fixed-word simulation is the coarsest forward simulation-like preorder which can be used for quotienting B\"uchi automata, thus improving our understanding of the limits of quotienting. Also, we show that computing fixed-word simulation is PSPACE-complete. On the practical side, we introduce proxy simulations, which are novel polynomial-time computable preorders sound for quotienting. In particular, delayed proxy simulation induce 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 non-decreasingly, preserving certain properties. We study under which general conditions refinement transformers are sound for quotienting.