B\"uchi Automata can have Smaller Quotients
Lorenzo Clemente

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
Topicssemigroups and automata theory · Formal Methods in Verification · Ferroelectric and Negative Capacitance Devices
