Komplex események feldolgozása automataelméleti alapokon

A hagyományos kritikus rendszerekben gyakorta alkalmazott módszer a futási idejű ellenőrzés. Ennek célja olyan ellenőrző programok szintézise, melyek segítségével felderíthető egy kritikus komponens hibás, a követelményektől eltérő viselkedése a rendszer működése közben. Többek között ezt a célt szolgálja egy, a tanszéken fejlesztett keretrendszer is, amely élő modelleket használ és az azok fölött értelmezett modelltranszformációs szabályok segítségével definiálja a vizsgálandó temporális kifejezést. Modelltranszformációk helyességének ellenőrzése azonban algoritmikusan eldönthetetlen feladat általánosságban, így a definiált temporális viselkedéseket is nehéz formálisan vizsgálni.
Az irodalomban többféle megközelítés létezik a temporális viselkedések definiálására és többféle formalizmust is definiáltak automata alapokon. Ezekben közös, hogy az automaták többnyire jól vizsgálhatóak algoritmikusan, az általuk definiált és elfogadott nyelvekkel kapcsolatban lehetőség van formális analízisre és ellenőrzésre.
A hallgató feladata megvizsgálni az irodalomban ismert legfontosabb automataelméleti megközelítéseket, és ez alapján kiterjeszteni a tanszéki keretrendszert a temporális viselkedések automata elméleti reprezentációjával.