PV1 ⊧ Reduceminimizes Büchi automata

Büchi automata minimization tool

Application domain/field

• Büchi automata
• Nondeterministic finite automata
• Automata minimization

Type of tool

Automata translator?

Expected input

Büchi automaton (BA) or nondeterministic finite automaton (NFA)

Format:

../Formats/ba format

Expected output

Minimized automaton?

Internals

Reduce can be invoked with one of the following options:

• -light to use the Light-k method
• -nojump to use the Heavy-k method
• -pebble uses a 2-pebble simulation (tends to be slow in practice)
• -sat might create an automaton with fewer states, possibly with more transitions

By default Reduce will reduce Büchi automata. You can switch to NFA semantics by using the option -finite.