Spielebasiertes kontrollieren von Nichtdeterminismus in Systemen mit unendlichen Zustandsräumen

• Antragsteller: Dr. Patrick Totzke
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung seit 2024
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 524989976

Formale Verifikation wird benutzt um sicherzustellen, dass sich Computersysteme wie vorgesehen verhalten. Obwohl dies immer erstrebenswert ist, ist es sehr schwierig Fehlverhalten auszuschließen: eine manuelle Verifizierung ist nur in kleinen Fällen praktikabel, und vollautomatische Verfahren sind in der Regel rechenintensiv oder nachweislich unmöglich und werden deshalb nur in kritischen Anwendungen eingesetzt um Katastrophen zu vermeiden. Die Entwicklung von neuen Verifikationstechniken ist ein aktives Forschungsgebiet, das sich zusätzlich zu praktischen Anwendungen auch wesentlich mit mathematischen Grundlagen beschäftigt, um und unser Verständnis der Grenzen der Berechenbarkeit zu verbessern. Gängige Modellierungsformen erlauben nichtdeterministisches Verhalten. Dies ermöglicht, algorithmische Prozesse zu approximieren, Spezifikationen kompakt auszudrücken oder unkontrollierbare externe Einflüsse abzubilden. Analysetechniken für solche Modelle benötigen deshalb häufig kostspielige Determinisierungsschritte, die oft das Haupthindernis für effiziente Verfahren darstellt. Bei Modellen mit unendlich vielen möglichen Systemzuständen ist Nichtdeterminismus im Allgemeinen generell noch einflussreicher als für endliche Systeme, in dem es deren Ausdruckskraft strikt erweitert, aber im Gegenzug ihre Analyse komplexer macht. Historydeterminismus (HD) ist eine beschränkte Art von Nichtdeterminismus, wobei dieser schrittweise, ohne Kenntnis von zukünftigen Eingaben, auflösbar sein muss. Dieser Kompromiss ermöglicht effiziente, spielbasierte Verifikation ohne teure Determinisierung. In diesem Projekt werden wir Historydeterminismus in zwei Richtungen untersuchen. Zum einen werden wir HD-Varianten von Formalismen betrachten, die standardmäßig zur Modellierung von Parallelität, rekursiven Programmen oder Echtzeitsystemen eingesetzt werden. Unsere Hypothese ist, dass diese im Vergleich zu deterministischen Varianten ausdrucksstärker sind, also komplexere Spezifikationen ermöglichen, ohne deren Verifikation wesentlich zu erschweren. Wir werden untersuchen, inwieweit der Historydeterminismus die Ausdrucksstärke beeinflusst, ob die HD-Eigenschaft selbst algorithmisch erkannt werden kann, und wie existierende Methoden unter der Eigenschaft vereinfacht werden können. Als zweite Ausrichtung des Projektes werden wir Variationen von Historydeterminismus untersuchen, wieder mit dem Ziel die Ausdrucksstärke unserer Modelle zu maximieren und die Komplexität von Verifizierungsverfahren zu minimieren. Solche Variationen ergeben sich zum Beispiel daraus, dass man in den spielbasierten Charakterisierungen variiert, welche Art von Informationen und Ressourcen den Spielern zur Verfügung stehen, oder welche Garantien verlangt werden um zu gewinnen. Wir erwarten, dass unsere Aktivitäten neue theoretische Erkenntnisse liefern sowie praktische Auswirkungen haben, indem sie neue, effiziente Implementierungen ermöglichen.

• DFG-Verfahren: Sachbeihilfen