Verifikation von gewichteten Zeitautomaten

• Antragstellerin: Dr. Karin Quaas
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2010 bis 2018
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 181095210

Gewichtete Zeitautomaten erweitern klassische endliche Automaten um eine endliche Menge reellwertiger Uhrenvariablen, sowie um eine Gewichtsfunktion, die sowohl den Transitionen als auch den Zuständen eines Automaten ein Gewicht zuweist. Das Gewicht einer Transition gibt an, wieviel das Ausführen dieser Transition kostet. Das Gewicht, das einem Zustand zugewiesen ist, bestimmt hingegen die Kosten, die pro Zeiteinheit während des Verweilens in diesem Zustand entstehen. Gewichtete Zeitautomaten eignen sich besonders als abstraktes Modell für Echtzeitsysteme mit kontinuierlichem Ressourcenverbrauch. Seit ihrer Einführung im Jahre 2003 haben sie daher auch ein großes Interesse in der Forschung auf dem Gebiet der Echtzeitsysteme hervorgerufen. Allerdings sind viele Entscheidungsprobleme für gewichtete Zeitautomaten unentscheidbar oder haben hohe computationale Komplexitäten. So ist zum Beispiel das Model Checking Problem für eine gewichtete Version von MTL zwar entscheidbar, jedoch nur mit nicht primitiv-rekursiver Komplexität, und auch nur dann wenn der Zeitautomat höchstens eine Uhrenvariable verwendet und die Gewichtsraten der Zustände entweder null oder eins sind. Für alle anderen Varianten des Modells ist das Problem unentscheidbar. Deswegen wollen wir in diesem Projekt Zeitautomaten mit diskreten Transitionsgewichten in den ganzen Zahlen betrachten, d.h., wir erlauben keine kontinuierlichen Gewichte, die durch die Gewichtsraten an den Zuständen entstehen. Dies ist zwar eine erhebliche Einschränkung des ursprünglichen Modells; jedoch ist dieses Modell trotzdem stark genug um interessante Eigenschaften auszudrücken. Dies kann man auch an der äußerst lebhaften Forschung auf dem Gebiet der verwandten Einzählersysteme sehen. Wir möchten weiterhin Kombinationen aus Zeitautomaten und Einzählersystemen untersuchen, mit denen man Beschränkungen über die Werte der Gewichtsvariablen ausdrücken kann. Für diese Modelle wollen wir das Model Checking Problem und andere Verifikationsprobleme, wie z.B. das Sprachinklusionsproblem, untersuchen. Als Spezifikationssprachen wollen wir wohlbekannte Erweiterungen von LTL, wie z.B. MTL, Freeze LTL, oder TPTL, betrachten. Die meisten dieser Logiken haben unentscheidbare Probleme. Deswegen wollen wir uns auf Fragmente konzentrieren, die sowohl ausdrucksstark sind, als auch handhabbare Entscheidungsprobleme besitzen. Wir hoffen dabei, von kürzlich erbrachten Resultaten zu Fragmenten von, z.B., MTL, sowohl im Gebiet der Echtzeitsysteme, als auch im Gebiet der Einzählersysteme, profitieren zu können. Mit dem Projekt hoffen wir weiterhin, die gegenseitige Befruchtung dieser beiden Gebiete der Theoretischen Informatik voranzubringen.

• DFG-Verfahren: Sachbeihilfen