Nicht-Mehrdeutigkeit, Alternierung und Nichtstandardakzeptanz in automatenbasierter Modellprüfung probabilistischer Systeme

• Antragstellerin: Professorin Dr. Christel Baier
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2016 bis 2024
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 313089026

Das Projekt befasst sich mit der quantitativen Analyse von probabilistischen Systemen, modelliert durch Markovketten und Markoventscheidungsprozesse, gegen Linearzeiteigenschaften, dargestellt durch temporallogische Formeln. Der bekannteste Ansatz, der in mehreren Tools realisiert wurde, transformiert die Formel in einen deterministischen Rabin-Automaten und analysiert das Produkt des Systemmodells und Automaten. Die Komplexität dieses Ansatzes ist doppelt exponentiell in der Formellänge und polynomiell in der Modellgröße. Aus komplexitätstheoretischer Sicht ist dies optimal für Markoventscheidungsprozesse, nicht jedoch für Markovketten. Für diese sind effizientere Algorithmen mit einer einfach-exponentiellen Zeitschranke bekannt. Hierzu zählt ein iteratives automatenloses Verfahren sowie automatenbasierte Ansätze mit separierten (stark nicht-mehrdeutigen) und alternierenden Automaten. Implementierungen der einfach-exponentiellen Methoden sind uns nicht bekannt.In diesem Projekt werden wir Verfeinerungen und Erweiterungen dieser Algorithmen für Markovketten und deren parametrische Varianten untersuchen, und vergleichende Studien mit symbolischen und nicht-symbolischen Implementierungen durchführen. Insbesondere werden wir den Einsatz nicht-mehrdeutiger ("unambiguous") Büchi-Automaten für die Analyse von Markovketten im Detail untersuchen. Ziel des Projekts ist es u.a. einen fehlerhaften Algorithmus der Literatur zu korrigieren und die bekannten einfach-exponentiellen Verfahren in verschiedenen Richtungen zu erweitern. Die bekannten und neuen Algorithmen mit nicht-mehrdeutigen und alternierenden Automaten bzw. den iterativen automatenlosen Ansatz für probabilistische Modellprüfungszwecke werden wir in vergleichenden Studien auswerten. Während sich vorherige Arbeiten hauptsächlich auf branching-time Logiken oder lineare temporale Logik (LTL) ohne Vergangenheitsoperatoren konzentrieren, werden wir LTL mit Vergangenheitsoperatoren sowie ein Kernfragment der property specification language (PSL) untersuchen. Insbesondere werden wir neue Algorithmen für die Übersetzung von LTL-Formeln sowohl mit als auch ohne Vergangenheitsoperatoren und PSL-Formeln in nicht-mehrdeutige Automaten entwerfen.Weiterhin werden wir deterministische Automaten mit Normalformen von Muller-Akzeptanz (anstelle von Rabin-Akzeptanz) und deren Nutzen für die quantitative Analyse von Markovketten und Markoventscheidungsprozessen analysieren. Das Hauptziel zur Betrachtung von Muller-Akzeptanzbedingungen ist eine Abwägung zwischen dem Nutzen flexiblerer Akzeptanzbedingungen, die zu kleineren Automaten führen können, und des gesteigerten Berechnungsaufwands der notwendigen Graphanalyse im Produkt des Systemmodells und des Automaten.

• DFG-Verfahren: Sachbeihilfen