PV1 MeMinminimizes Mealy machines

SAT-based minimizer for Mealy machines

Application domain/field

Type of tool

Minimizer for Mealy machines

Expected input

Mealy machine

Format:

KISS2 format

Expected output

result.kiss file describing the minimized Mealy machine.

Internals

This tool focuses on minimizing incompletely specified Mealy machines (where one or mote outputs or next states might not be specified). When it minimized a Mealy machine M, it looks for a machine M' with the minimal number of states with the same input/output behavior on all input sequences for which the behavior of M is defined. M' might be defined on additional input on which M is not defined. Uses MiniSat.

Comments

Not published at CAV or TACAS but mentioned in a "Uses" clause of another tool.
Automaton

Links

Last commit date

8 May 2018

Related papers

https://doi.org/10.1109/ICCAD.2015.7372555 (ICCAD)

Last publication date

2015

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.