Lineáris tranzíciós rendszerek absztrakt interpretáció alapú verifikációja

A lineáris tranzíciós rendszerek (LTR), mint például a Petri-hálók, többek között az aszinkron, elosztott, konkurens, párhuzamos és nem-determinisztikus rendszerek elterjedt grafikus és matematikai modellező eszközei. A LTR modellek viselkedését az állapottér, azaz az elérhető állapotok és az állapotátmenetek halmaza adja meg.
A formális verifikáció egyik legfontosabb vizsgálata az ún. elérhetőségi analízis, amely azt vizsgálja, hogy egy adott állapot elérhető-e engedélyezett állapotátmenetek sorozatával egy adott kezdőállapotból kiindulva. Ezen eldönthetőségi probléma a matematika nehéz problémái közé esik, ezért hatékony algoritmusokra van szükség.
Az irodalomban ismert egyik hatékony algoritmus az absztrakt interpretáció, amely az állapottér egy véges, absztrakt reprezentációján végez következtetéseket.
A hallgató feladata megvizsgálni az absztrakt interpretáció algoritmusát, és amennyiben lehetséges, továbbfejleszteni azt a tanszéki fejlesztésű modellellenőrző keretrendszerben.
A hallgató feladatának a következőkre kell kiterjednie:

• Mutassa be az absztrakt interpretáció algoritmusát.
• Tervezzen meg egy absztrakt interpretációt használó verifikációs modult a tanszéki fejlesztésű modellellenőrző keretrenszerbe.
• Implementálja az algoritmust.
• Vizsgálja meg az algoritmus továbbfejlesztési lehetőségeit.