Informace o projektu

Předmětem našeho výzkumu je formální verifikace systémů, které vykazují náhodné chování a zároveň musí splňovat různá časová omezení (stochastic real-time systems, SRTS). Náhodné aspekty systémů se obvykle modelují pomocí stochastických procesů. Systémy pracující v reálném čase jsou typicky modelovány pomocí časových automatů. Abychom byli schopni modelovat SRTS, musíme tyto formalismy vhodně spojit. Koncentrujeme se zejména na strukturální vlastnosti takových systémů a výpočetní složitost základních verifikačních problémů. Další obvyklou vlastností reálných systémů je nedeterminismus, tedy nejistota v chování bez jakékoliv statistické znalosti. Nedeterminismus se také objevuje v problémech, v nichž je třeba syntetizovat řídící jednotku systému. SRTS s nedeterminismem lze modelovat pomocí rozhodovacích procesů se spojitým časem, jejichž cílové podmínky lze vyjádřit pomocí časových automatů. V této oblasti se zabýváme zejména existencí řídící jednotky, která splňuje cílovou podmínku a zároveň ji lze algoritmicky konstruovat.