PV2 ⊧ MONAtranslates WS1S and WS2S into minimum DFAs and GTAs

Tool that translates formulas to finite-state automata

Application domain/field

Finite-state automata

Type of tool

Translator

Expected input

WS1S (weak monadic Second-order theory of 1 successor) or WS2S formula

Format:

MONA has its own syntax. The tool expects a .mona file.

Internals

MONA translates WS1S and WS2S formulas into minimum DFAs (Deterministic Finite Automata) and GTAs (Guided Tree Automata), respectively.