PV1 ⊧ MeMinminimises Mealy machines

SAT-based minimizer for Mealy machines

Application domain/field

• Mealy machines
• Minimization

Type of tool

Minimizer for Mealy machines

Expected input

Mealy machine

Format:

KISS2 format

Expected output

result.kiss file describing the minimised 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 minimised 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.