Detailseite
Projekt Druckansicht

Automatentheoretische Verifikationsprobleme mit Ressourcenschranken

Fachliche Zuordnung Theoretische Informatik
Förderung Förderung von 2012 bis 2015
Projektkennung Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 213443580
 
Automatentheoretische Methoden werden erfolgreich in der Verifikation im Rahmen des Model- Checking eingesetzt. Neben der Verifikation endlicher Systeme können viele Methoden auf Klassen unendlicher Systeme erweitert werden, wie z.B. Pushdownsysteme, welche zur Modellierung von Rekursion verwendet werden, und Grundtermersetzungssysteme, welche die Pushdownsysteme um eine eingeschränkte Art der Nebenläufigkeit erweitern. Im Kern handelt es sich bei Verifikationsproblemen oft um Erreichbarkeitsprobleme, also die Frage, ob man von bestimmten Systemzuständen andere Zustände über endlich viele Berechnungsschritte erreichen kann. In dem Projekt sollen Systeme betrachtet werden, die zusätzlich den Verbrauch von Ressourcen modellieren. Die Erreichbarkeitsfragen werden dann unter der Annahme einer Schranke für den Ressourcenverbrauch formuliert. Diese Schranke ist dabei nicht fest vorgegeben, sondern es wird nach der Existenz einer solchen Schranke gefragt. Ziel des Projektes ist die Entwicklung von Algorithmen für diese neue Klasse von Verifikationsproblemen auf Systemen mit Ressourcenverbrauch. Für die Beantwortung solcher algorithmisch schwierigen Fragen stellt eine kürzlich neu entwickelte Theorie der Ressourcenautomaten (in der Literatur auch als Distanz- oder Kostenautomaten bezeichnet) geeignete Werkzeuge zur Verfügung.
DFG-Verfahren Sachbeihilfen
 
 

Zusatzinformationen

Textvergrößerung und Kontrastanpassung