Effective Reductions of Mealy Machines

TL;DR

This paper introduces two new techniques for reducing the size of incompletely specified Mealy machines, balancing minimization quality and computational performance, and benchmarks them against existing tools.

Contribution

It presents a novel reduction method based on simulation techniques and compares it with an existing minimization tool for Mealy machines.

Findings

The simulation-based reduction offers a good compromise between size and performance.

The proposed methods outperform existing tools on various test cases.

Benchmark results demonstrate effectiveness on both known and new instances.

Abstract

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 and solves the minimization problem, the latter is a novel approach derived from simulationbased 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.