Project information
Překlad formulí Lineární temporální logiky na omega-automaty (LTL2AUTOMATA)

Cílem projektu je upevnit a prohloubit spolupráci mezi Fakultou informatiky Masarykovy univerzity a Ecole d'ingénieurs en informatique (EPITA) v oblasti základního výzkumu formálních metod. Spolupráce bude upevněna formou mobility mladých výzkumných pracovníků zabývajících se překladem LTL na omega-automaty. V rámci projektu spolupracující týmy identifikují žádoucí vlastnosti omega-automatů v závislosti na jejich dalším využití. Týmy dále navrhnou a následně implementují úpravy překladů nebo nové překlady formulí z LTL (či z fragmentů LTL) do různých druhů omega-automatů tak, aby výsledné automaty měly žádoucí vlastnosti. Cílem tohoto výzkumu je lepší vhled do vztahů mezi LTL, odpovídajícími automaty a jejich aplikacemi a dále zefektivnění algoritmů pracujících se specifikacemi systémů ve formě LTL formulí.