Kritikus valós idejű rendszerek fejlesztésében kulcsfontosságú kihívás a szoftverrendszerek helyes működésének verifikációja. Az automatizált modellellenőrzésben a rendszernek egy formális (matematikai) leírásán kerülnek ellenőrzésre a kívánt biztonsági követelmények, egy automatizált eszköz által. Ezen automatizált eszközök különböző matematikai bizonyító és gráf algoritmusokat használnak működés közben. A modellellenőrzés problémája már közepes méretű rendszereken végezve is algoritmikusan nehéz feladat, ugyanis a bejárandó állapotok száma gyakran a modell méretében exponenciálisan nő. Ezen kívül az időzítések megszámlálhatatlanul végtelen állapotteret okoznak. Annak érdekében, hogy ezen rendszerek is vizsgálhatók legyenek, hatékony algoritmusokra van szükségünk. Az önálló munka során a hallgató beletanul az egyetemen fejlesztett Theta nyílt forráskódú modellellenőrző keretrendszerbe (https://github.com/ftsrg/theta) és azt új algoritmusokkal egészíti ki.