Bachelor theses
Translation of MSOL formulas to finite automatons
Author
Jarmila Fialová
Year
2025
Type
Bachelor thesis
Supervisor
RNDr. Radek Hušek, Ph.D.
Reviewers
Mgr. Michal Opler, Ph.D.
Department
Summary
Using formal logic to verify practical solutions is a well-known method used by a wide variety of fields, ranging from hardware verification to controller synthesis. MONA is a tool that takes in a theory and outputs an automaton that can be used not only to verify, but also find solutions. It is an old tool, whose code is hard to comprehend and harder to modify. This thesis analyzes, recreates and expands MONA's capabilities.