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.
Automaton

Links

Last commit date

8 February 2020

Related papers

Last publication date

2002

ProVerB specific

View/edit source (Markdown)



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