Effective Reductions of Mealy Machines

We revisit the problem of reducing incompletely specified Mealy machines with reactive synthesis in mind. We propose two techniques: the former is inspired by the tool MEMIN [1] and solves the minimization problem, the latter is a novel approach derived from simulation-based reductions but may not guarantee a minimized machine. However, we argue that it offers a good enough compromise between the size of the resulting Mealy machine and performance. The proposed methods are benchmarked against MEMIN on a large collection of test cases made of well-known instances as well as new ones.