Název projektu
Výpočetní složitost vybraných verifikačních problémů
Kód
GA15-13784S
Předmět výzkumu
Verifikace hardwarových a softwarových systémů se stává neoddělitelnou součástí jejich vývoje. Zkoumání mezí automatizované verifikace odhalilo několik zajímavých problémů, jejichž výpočetní složitost je nejasná i přes nemalé úsilí výzkumné komunity. Takovým problémem je i ekvivalence funkčních schémat prvního řádu, který lze vyjádřit jako ekvivalenci deterministických zásobníkových automatů. Rozhodnutelnost problému je proslulý výsledek, který docílil G. Sénizergues, ale známá složitost leží někde mezi polynomiálním časem a opakovaným umocňováním. Hlavním cílem projektu je prozkoumání tohoto a příbuzných problémů podrobněji, v návaznosti na předchozí výzkum členů týmu, který vyjasnil složitost některých podpřípadů. Důležitou součástí projektu je vytvoření softwarového nástroje, který umožní experimentování s instancemi problémů, což by mělo umožnit získání většího vhledu do problémů ekvivalence.
Rok zahájení
2015
Rok ukončení
2017
Poskytovatel
Grantová agentura ČR
Kategorie
Obecná forma
Typ
Standardní projekty
Řešitel
Informační systém výzkumu, vývoje a inovací