Tanszéki konzulens: 

Micskei Zoltán tanszékvezető helyettes, docens Szoba: IB419 Tel.: +36 1 463-3594 Email: micskeiz (*) mit * bme * hu

Az olyan elosztott rendszerek ellenőrzése, amik viselkedése az aktuális környezettől függ mindig (pl. mobil rendszerek, robotok és autonóm rendszerek), rendkívül nehéz az ilyen rendszerekben meglévő dinamizmus és nemdeterminizmus miatt. Egy-egy kezdeti állapothoz megjósolni a pontos elvárt állapotot (pl. a robot pontosan milyen irányban kezdi el felderíteni a környezetét) nem mindig lehetséges. Ellenben állandóan teljesítendő köveletelményeket könnyebb megfogalmazni (pl. a robot ne ütközzön falnak), és ezek segítségével is ki lehet értékelni a rendszerünk viselkedését. A feladat ilyenkor az, hogy a konkrét futtatások során rögzítjük folyamatosan mind a rendszerünk, mind a környezet állapotát egy úgynevezett futási trace-be, és ezen vizsgáljuk a követelményeinket. Autonóm rendszerek esetén az a kihívás, hogy a rendszer akcióihoz folyamatosan illeszteni kell környezeti állapotot, és ezt is figyelembe kell venni az eredményben. A feladat olyan leírások (pl. különböző kifejezőerejű automaták) és algoritmusok megismerése majd implementálása, amik ezt az ellenőrzést hatékonyan megoldják.