Effective Reductions of Mealy Machines

From LRDE

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 sc MeMin 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.

Documents

Bibtex (lrde.bib)

@InProceedings{	  renkin.22.forte,
  author	= {Florian Renkin and Philipp Schlehuber-Caissier and
		  Alexandre Duret-Lutz and Adrien Pommellet},
  title		= {Effective Reductions of {M}ealy Machines},
  year		= 2022,
  booktitle	= {Proceedings of the 42nd International Conference on Formal
		  Techniques for Distributed Objects, Components, and Systems
		  (FORTE'22)},
  series	= {Lecture Notes in Computer Science},
  month		= jun,
  pages		= {114--130},
  volume	= {13273},
  publisher	= {Springer},
  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 {\sc
		  MeMin} 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 \textsc{MeMin} on a large
		  collection of test cases made of well-known instances as
		  well as new ones.},
  doi		= {10.1007/978-3-031-08679-3_8}
}