Bakalářské práce
Překlad MSOL formulí na konečné automaty
Autor
Jarmila Fialová
Rok
2025
Typ
Bakalářská práce
Vedoucí
RNDr. Radek Hušek, Ph.D.
Oponenti
Mgr. Michal Opler, Ph.D.
Katedra
Anotace
Použití formální logiky pro verifikaci praktických řešení je dobře prozkoumaná metoda, využívaná mnoha různými obory od hardwarové verifikace až po syntézu kontrolerů. MONA je nástroj, který dostane na vstupu popis teorie a~jehož výstup je automat, který lze použít nejenom pro verifikaci, ale i~pro nalezení řešení. Je to starý nástroj, jehož kód je težké pochopit a ještě těžší modifikovat. Tato práce analyzuje, znovuvytváří a rozšiřuje schopnosti MONY.