Přeskočit na hlavní obsah
Přeskočit hlavičku
Název projektu
Verifikace nekonečně stavových systémů
Kód
GA201/03/1161
Předmět výzkumu
Návrh je motivován jednou z živých oblastí současného výzkumu týkajícího se formální verifikace (a tedy i modelování a analýzy) nekonečně stavových souběžných (concurrent) systémů, kde verifikací se rozumí (zkoumání rozhodnutelnosti a složitosti)ověřován í jistých sémantických ekvivalencí těchto systémů a jejich temporálně logických vlastností. V poslední době bylo v dané oblasti dosaženo zajímavých výsledků,např.\,pro kalkuly BPA, BPP, PA, PDA a Petriho sítě, k nimž přispěly i grantové projektyGAČR reg. č. 201/93/2123, 210/97/0456 a 210/00/0400 řešené týmem, který předkládá tento návrh. Hlavním cílem navrhovaného projektu je systematicky prozkoumat zmíněné a příbuzné modely a zaměřit se na charakterizaci rozhodnutelných podtříd vzhledem kběžným sémantic kým ekvivalencím (a k adekvátním předuspořádáním), na jejich vzájemné vztahy a expresibilitu (včetně testování regularity a možností konečné charakterizace) a na rozhodnutelné modální a temporální logiky, či jejich rozumné fragmenty.
Rok zahájení
2003
Rok ukončení
2005
Poskytovatel
Grantová agentura ČR
Kategorie
Obecná forma (normální záznam)
Typ
Standardní projekty
Řešitel
Výsledky na www.rvvi.cz (RIV)
Zpět na seznam