Mobil és autonóm rendszerek futásának kiértékelése

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.