Egyszerű állapottér-kiterítés (Unfolding) jellegű algoritmus megismerése és implementálása

A modern mérnöki tervezésben fontos a modellek ellenőrzése. Az ellenőrzött modelleket ezután felhasználhatjuk a megvalósítás, kódgenerálás, működő architektúrák létrehozása során.

Az elmúlt évtizedben sok próbálkozás volt, hogy a modellellenőrző algoritmusokat hatékonyabbá tegyék. Ezek közül az egyik lehetőség az "unfolding", azaz az állapottér-gráf kiterítésének alkalmazása. Ez az algoritmus alapjául szolgál a jelenleg ipari rendszerekben is széles körben alkalmazott részleges-rendezés elvű algoritmusoknak.

A hallgató feladata megismerkedi az algoritmussal, feldolgozni a szakirodalmat, és egy implementáción keresztül megvizsgálni, továbbfejleszteni azt.

A feladat során a hallgató eljuthat komolyabb algoritmusok vizsgálatáig, implementálásáig.

Lelkes és érdeklődő hallgatóknak TDK lehetőség.

Keretrendszer, melyet a Formális Módszerek MSc tárgyban is használunk:  https://www.inf.mit.bme.hu/research/tools/petridotnet