Uni-Logo

Habilitationen

Anmerkung: Diese Liste wird derzeit überarbeitet und erhebt daher keinen Anspruch auf Vollständigkeit.

Jan-Georg Smaus
Logik und Abstraktion, Verifikation und Falsifikation
November 2008
Download: (PDF)

Die in dieser Habilitationsschrift versammelten Arbeiten beschäftigen sich mit dem Einsatz von Logik und Abstraktionstechniken zum Zwecke der Verifikation und Falsifikation von Transitionssystemen. Die Arbeiten wurden in zwei Hauptthemen untergliedert.

Im ersten Hauptthema sind die Transitionssysteme Programme, im Besonderen Logikprogramme. Verschiedene Aspekte der Korrektheit solcher Programme werden betrachtet. Ein Aspekt ist die Terminierung; die Arbeiten enthalten verschiedene Beiträge zu Beweismethoden für Terminierung. Ein anderer Aspekt ist die Typsicherheit. Die Habilitation enthält verschiedene Resultate, die die Typsysteme, für die Typsicherheit garantiert werden kann, erweitern.

Im zweiten Hauptthema sind die Transitionssysteme Realzeitsysteme und hybride Systeme. Es werden heuristische Methoden vorgestellt, um Fehlerpfade in solchen Systemen zu finden, was wichtig ist, um den Entwurfsprozess der Systeme zu unterstützen. Ein weiterer Beitrag ist eine Methode zur kompakten Repräsentation aussagenlogischer Formel als Menge von linearen pseudo-Booleschen Constraints. Dies ist unter Anderem deshalb nützlich, weil Aussagenlogik bei der Analyse von Transitionssystemen eine prominente Rolle spielt, und zwar im Gebiet des Bounded Model Checking.

Jussi Rintanen
Automated Planning: Algorithms and Complexity
Dezember 2005
Jana Koehler
IPP: A Planning System for ADL and Resource-Constrained Planning Problems
Januar 2000