Název projektu
Nekonečně stavové souběžné systémy - modely a verifikace
Kód
GA201/00/0400
Předmět výzkumu
Projekt je motivován jednou z živých oblastí současného výzkumu týkajícího se modelování, analýzy a verifikace složitých (potenciálně nekonečně stavových) souběžných (concurrent) systémů. Jejich verifikací se rozumí (zkoumání možností algoritmického) ověřování jistých ekvivalencí těchto 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 BBA, BPP, PA a Petriho sítě, k nimž přispěly grant. projekty GAČR č. 201/93/212 a č. 210/97/0456 ř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 k běžným ekvivalencím a jejich vzájemné vztahy, testování regularity (tj. ekvivalence s konečně stavovým systémem) a možností konečné charakterizace (i vzhledem k adekvátním předuspořádáním), a na rozhodnutelné modální a temporální logiky, či rozumné fragmenty.
Rok zahájení
2000
Rok ukončení
2002
Poskytovatel
Grantová agentura ČR
Kategorie
Obecná forma
Typ
Standardní projekty
Řešitel
Informační systém výzkumu, vývoje a inovací