Verifikation nicht-regulärer Eigenschaften

点击翻译按钮获取中文摘要

Bislang hat sich die Verifikation verteilter, reaktiver, etc. Systeme auf das Beweisen von ¿ im Sinne der formalen Sprachen ¿ regulären Eigenschaften konzentriert. Im Rahmen dieses Projektes soll der Bereich derjenigen Eigenschaften, die automatisch durch Model Checking verifiziert werden können, ausgedehnt werden. Dies beinhaltet die Definitionen entsprechender Logiken und Model Checking Algorithmen für diese, deren Optimierungen sowie ihre theoretische wie auch experimentelle Validierung im Hinblick auf ihre Benutzbarkeit.