Ve formální verifikaci se pomocí matematických metod dokazuje, že daný
systém splňuje požadované vlastnosti. Verifikační a analytické metody
jsou obvykle tvořeny na míru dané třídě systémů, která je
charakterizována nějakou specifickou vlastností jako například
náhodnost, závislost na reálném čase, počet stavů, apod. Reálné
systémy jsou ale obvykle komplexní a kombinují více těchto
charakteristických vlastností.

Naším cílem je studovat verifikační a analytické metody pro systémy,
které kombinují náhodnost s dalšími aspekty chování, jako je
nedeterministická volba, reálný čas, interakce, apod. Speciální
pozornost bude věnována systémům s nekonečně mnoha stavy. Studovány
budou vlastnosti formálních modelů těchto systémů, například
stochastických her s reálným časem, pravděpodobnostních zásobníkových
automatů, systémů s čítači, popisných jazyků komunikačních protokolů,
apod. Mezi cíle výzkumu patří také návrh nových formalismů vhodných
pro specifikaci vlastností takových systémů a analýza
rozhodnutelnosti a složitosti příslušných verifikačních problémů.

Publikace