Automatentheoretische Verifikationsprobleme mit Ressourcenschranken

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

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.