Regisztráció és bejelentkezés

Absztrakt interpretációt használó keresési stratégiák Petri-háló alapú modellekhez

A Petri-hálók az aszinkron, elosztott, konkurens, párhuzamos és nemdeterminisztikus rendszerek elterjedt grafikus és matematikai modellező eszközei. Petri-háló alapú modellek analízisekor fontos kérdés az állapotelérhetőség, amely során azt vizsgáljuk, hogy egy adott célállapot része-e az állapottérnek. A probléma egyszerű Petri-hálók esetén eldönthető, azonban a végtelen állapottér és a Petri-hálók nagy kifejezőereje miatt a nagyon komplex, az EXPSPACE-nehéz komplexitási osztályba tartozik. A tiltó-élekkel kibővített Petri-hálók kifejezőereje azonos a Turing gépekkel, emiatt az elérhetőségi probléma ebben az esetben már nem eldönthető.

Végtelen állapotterű modellek analízisére nyújtanak megoldást a különböző, matematikai absztrakción alapuló módszerek. Ezen módszerek előnye, hogy egy véges állapottér reprezentációt építve és azt bejárva vizsgálják az elérhetőségi és/vagy invariáns tulajdonságokat. Az absztrakt interpretáció algoritmusa a véges reprezentációt konvex poliéderek segítségével állítja elő, így felülbecsülve a lehetséges elérhető állapotokat. Petri-háló alapú modellek esetén azonban az irodalomban ismert módszerek sokszor nem képesek elég precíz becslést adni. Munkám során ezen módszerek továbbfejlesztésével és kiterjesztésvel foglalkoztam.

A dolgozatban bemutatok olyan, az absztrakt interpretáció finomításán alapuló algoritmusokat, amelyek segítségével olyan rendszerek vizsgálhatóságát is lehetővé tettem, amelyre a korábbi algoritmusok nem voltak képesek. Kifejlesztettem egy új algoritmust, amely a felderített állapotteret finomítja az elérhetőségi feltétel figyelembevételével. Emellett pedig mutatok egy módszert, amely az explicit állapottér bejáró és az absztrakt interpretáción alapuló algoritmusokat együttesen alkalmazza a hatékonyság növelése érdekében. Az új algoritmusok előnyeit mintapéldákkal szemléltetem.

szerző

  • Farkas Rebeka
    mérnökinformatikus
    nappali

konzulensek

  • Dr. Vörös András
    adjunktus, Méréstechnika és Információs Rendszerek Tanszék
  • Tóth Tamás
    tudományos segédmunkatárs, Méréstechnika és Információs Rendszerek Tanszék
  • Dr. Semeráth Oszkár
    tudományos munkatárs, Méréstechnika és Információs Rendszerek Tanszék