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

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.

Další info