Název projektu
Meze algoritmické verifikovatelnosti nekonečně stavových systémů
Kód
GA201/97/0456
Předmět výzkumu
Projekt je motivován jednou z živých oblastí současného výzkumu týkajícího se analýzy a verifikace složitých (potenciálně nekonečně stavových) konkurentních systémů. Jedná se o oblast mezi algoritmické verifikovatelnosti, kde verifikací se rozumí ověřová ní ekvivalence systémů, jejich temporálně logických vlastností apod. V poslední době bylo v dané oblasti dosaženo zajímavých výsledků, např. pro kalkuly BPA, BPP a Petriho sítě, k nimž přispěl i grant. projekt GA ČR č. 201/93/2123. Hlavním cílem navrhova ného projektu je systematicky prozkoumat zmíněné a příbuzné modely a zaměřit se na: a) charakterizaci rozhodnutelných podtříd vzhledem k běžným ekvivalencím, b) testování regularity (tj. ekvivalence s konečně stavovým systémem), c) rozhodnutelné modální a temporální logiky či rozumné fragmenty. Zároveň je plánováno studium složitosti příslušných algoritmů a pro vhodné případy jejich prototypová implementace a testování typických případů.
Rok zahájení
1997
Rok ukončení
1999
Poskytovatel
Grantová agentura ČR
Kategorie
Obecná forma
Typ
Standardní projekty
Řešitel
Informační systém výzkumu, vývoje a inovací