Die Deutsche Forschungsgemeinschaft (DFG) bewilligt ein von der TU Dresden und der Universität Leipzig gemeinsam beantragtes Graduiertenkolleg zum Thema „Quantitative Logiken und Automaten“. Wie die DFG heute mitteilte, wird es für die Dauer von viereinhalb Jahren gefördert.

In dem Graduiertenkolleg sollen insgesamt 20 junge Doktoranden ausgebildet werden und die Möglichkeit erhalten, an dem Zusammenhang zwischen quantitativen Logiken und Automaten und deren Anwendungen in der Informatik auf höchstem fachlichen Niveau zu forschen und zu promovieren.

An dem zunächst für viereinhalb Jahre bewilligten Kolleg sind zehn Professoren und Nachwuchswissenschaftler der Theoretischen Informatik und der Künstlichen Intelligenz an der TU Dresden und der Universität Leipzig beteiligt. „Die erfolgreiche Beantragung eines Kollegs zu diesem Thema war nur möglich, weil es sowohl an der Fakultät Informatik der TU Dresden als auch an der Fakultät für Mathematik und Informatik der Universität Leipzig 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“, sagt Professor Franz Baader vom Institut für Theoretische Informatik der TU Dresden, der der Sprecher des Graduiertenkollegs ist, das im Herbst 2012 seine Arbeit aufnehmen wird.

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. Als ein Beispiel sei hier nur die Verifikation von Hardware- und Software-Systemen genannt, d.h. 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 werden und gewünschte Eigenschaften (etwa, dass jeder Anrufer irgendwann tatsächlich zu einem Mitarbeiter durchgeschaltet wird) in einer geeigneten Logik ausgedrückt werden.

Die Verifikation derartiger qualitativer Eigenschaften 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. Zum Beispiel könnte man in obigem Beispiel ausdrücken wollen, dass Anrufer im Mittel nicht länger als ein Minute warten müssen.

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.

Informationen für Journalisten:
Prof. Franz Baader
Tel.: 0351 463-39160

Kim-Astrid Magister
14 November 2011