Informace o projektu
Překlad formulí Lineární temporální logiky na omega-automaty
(LTL2AUTOMATA)
- Kód projektu
- 7AMB14FR016
- Období řešení
- 1/2014 - 12/2015
- Investor / Programový rámec / typ projektu
-
Ministerstvo školství, mládeže a tělovýchovy ČR
- Aktivita MOBILITY
- Fakulta / Pracoviště MU
- Fakulta informatiky
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í.