Forschungsprogramm "Quantitative Logiken und Automaten" erhält DFG-Förderung

An dem Kolleg sind zehn Professoren und Nachwuchswissenschaftler der Theoretischen
Informatik und der Künstlichen Intelligenz an der Universität Leipzig und der TU Dresden beteiligt. "Die erfolgreiche Beantragung eines Kollegs zu diesem Thema war nur möglich, weil es sowohl am Institut für Informatik der Universität Leipzig als auch an der Fakultät Informatik der TU Dresden sehr starke Theoriegruppen gibt, die sich schon seit langem mit Automaten, Logiken und deren Zusammenhang sowie ihren Anwendungen in verschiedenen Teilgebieten der Informatik auseinandersetzen, was in dieser Dichte eine in Deutschland einmalige Fokussierung darstellt", sagte Manfred Droste vom Institut für Informatik der Universität Leipzig und stellvertretender Sprecher des Kollegs. Franz Baader vom Institut für Theoretische Informatik der TU Dresden ist der Sprecher des Graduiertenkollegs.

Sowohl Automaten als auch Logiken werden in vielen Bereichen der Informatik zur Modellierung eingesetzt, wobei sich die beiden Modellierungsansätze häufig synergetisch ergänzen. In der Theoretischen Informatik wurde der Zusammenhang zwischen endlichen Automaten und Logiken seit dem Anfang der sechziger Jahre sehr intensiv untersucht. Dieser Zusammenhang ist für zahlreiche Anwendungsgebiete von großer Bedeutung. Ein Beispiel dafür ist die Verifikation von Hardware- und Software-Systemen, das heißt der automatisierte Nachweis, dass diese Systeme gewisse Anforderungen erfüllen. Hier kann das System - etwa eine Software, die Anrufer einer Service-Hotline in einer Warteschleife hält, bis ein geeigneter Mitarbeiter frei wird - durch einen endlichen Automaten modelliert und gewünschte Eigenschaften in einer geeigneten Logik ausgedrückt werden. Eine solche Anforderung könnte sein, dass jeder Anrufer einer Hotline irgendwann tatsächlich zu einem Mitarbeiter durchgeschaltet wird.

Die automatische überprüfung der Hard- und Software mit klassischen Automaten und Logiken ist bereits sehr gut erforscht. In vielen Anwendungsgebieten der Informatik müssen aber auch quantitative Phänomene repräsentiert werden. Ein Beispiel dafür wäre, dass Anrufer der Hotline durchschnittlich nicht länger als eine Minute auf ihren warten müssen. Das Ziel des Graduiertenkollegs ist daher eine gründliche und umfassende Erforschung von quantitativen Logiken und Automaten, ihres Zusammenhangs sowie ihrer Anwendung in ausgewählten Teilgebieten der Informatik.