Informace o projektu
Verifikace nekonečně stavových systémů

Informace

Projekt nespadá pod Pedagogickou fakultu, ale pod Fakultu informatiky. Oficiální stránka projektu je na webu muni.cz.
Logo poskytovatele
Kód projektu
GA201/03/1161
Období řešení
1/2003 - 12/2005
Investor / Programový rámec / typ projektu
Grantová agentura ČR
Fakulta / Pracoviště MU
Fakulta informatiky
Klíčová slova
concurrency theory, infinite-state systems, equivalence checking, decidability, complexity
Spolupracující organizace
Vysoká škola báňská - Technická univerzita v Ostravě

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é projekty GAČ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 k běžným sémantický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.
Dále chceme zkoumat vhodné modely pro oblast (i nemonotonních)souběžných systémů s omezeními (concurrent constraint systems), které by
umožnily asynchronní i synchronní komunikaci v tomto paradigmatu a studovat výše uvedené problémy i pro tyto systémy.

Publikace

Počet publikací: 43


Předchozí 1 2 3 4 5 Další

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.