Diszkrét dinamikus rendszerek viselkedésének felderítése ellenpélda-alapú absztrakció finomítás (CEGAR) segítségével

A Petri-hálók többek között az aszinkron, elosztott, párhuzamos és nemdeterminisztikus rendszerek elterjedt grafikus és matematikai modellező eszközei. A Petri-háló modellek viselkedését az elérhető állapotok halmaza (az állapottér) adja meg, amely akár végtelen nagyságú is lehet. A Petri-hálókkal kapcsolatos vizsgálatok egyik legfontosabbika, az ún. elérhetőségi analízis is az állapottérhez kapcsolódik: 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, a komplexitására még nem tudtak felső korlátot adni, az irodalom alapján legalább az EXSPACE-nehéz komplexitási osztályba esik.

Az ellenpélda-alapú absztrakció finomítás (angolul Counter Example Guided Abstracion Refinement, röviden CEGAR) gyakran használt megközelítés végtelen állapotterű rendszerek vizsgálatára. Lényege, hogy az állapottér egy absztrakcióján vizsgáljuk az elérhetőségi kérdést, és ha kell, a konkrét állapotok bejárása során nyert információ segítségével finomítjuk az absztrakciót. A 2011. évi Petri-háló modellellenőrző versenyen több kategóriát is megnyert egy CEGAR-alapú, elérhetőséget vizsgáló algoritmus. Ez az algoritmus a Petri-hálók állapotegyenletét használja absztrakcióként, és ezt finomítja mindaddig, amíg talál egy, az elérhetőséget igazoló állapotátmeneti útvonalat, vagy bizonyítja, hogy az állapot nem elérhető.

Munkánk során ezt az algoritmust vizsgáltuk és fejlesztettük tovább. Dolgozatunkban elméleti eredményként bemutatjuk, hogy az algoritmus bizonyos esetekben nem tudja megállapítani az elérhetőséget, és megoldást javasolunk, amely felhasználásával a problémák nagyobb köre esetén jut az algoritmus eredményre. Bemutatunk olyan optimalizációkat, amelyek kiküszöbölik az eredeti algoritmus bizonyos esetekben jelentkező hiányosságait, és hatékonyan vágják a keresési teret. Ezen túlmenően kiterjesztettük az algoritmust, hogy a problémák bővebb osztályát is kezelni tudjuk:

• alkalmassá tettük az algoritmust, hogy predikátumokkal definiált elérhetőségi vagy fedési problémákat is tudjon hatékonyan vizsgálni,

• bővítettük az algoritmust, hogy a tiltó éleket tartalmazó Petri-hálók vizsgálatára is alkalmas legyen.

Ez utóbbi kiterjesztés jelentőségét az adja, hogy a tiltó élek magasabb, a Turing gépekkel azonos szintre emelik a Petri-hálók kifejező erejét. Ugyanakkor elméletileg is bizonyított tény, hogy tiltó élek használata esetén nem várható el teljesség az algoritmustól.

Dolgozatunkban bemutatjuk az eredeti algoritmus gyakorlati implementációjával szerzett tapasztalatainkat, a felfedezett hiányosságokat, és az ezek kiküszöbölésére és az algoritmus teljesítményének növelésére kidolgozott megoldásainkat. A továbbfejlesztett algoritmus hatékonyságát mérési eredményekkel is alátámasztjuk.

szerzők

• 
  Hajdu Ákos
  mérnökinformatikus
  nappali
• 
  Mártonka Zoltán
  mérnökinformatikus
  nappali

konzulensek

• 
  Dr. Vörös András
  egyetemi docens, Méréstechnika és Információs Rendszerek Tanszék
• 
  Dr. Bartha Tamás
  docens, Méréstechnika és Információs Rendszerek Tanszék

helyezés