Informace o projektu

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/2123 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.