Mathematische Logik und Anwendungen
| Projektbeschreibung | Kontakt
|
Im 20. Jahrhundert hat sich die Mathematische Logik von einer zunächst mehr grundlagentheoretisch orientierten Wissenschaft zu einer mathematischen Disziplin erweitert, deren Sichtweisen, Methoden und Ergebnisse zu einer Bereicherung traditioneller mathematischer Gebiete beitragen. Mannigfaltige Verflechtungen mit der Informatik, die in Teilen selbst aus der Mathematischen Logik hervorgegangen ist, haben zu einer wechelseitigen Förderung beider Wissenschaften geführt. Die Arbeit der Informatiker aus Freiburg und der Logiker aus Freiburg und Konstanz, die das Graduiertenkolleg tragen, war schon vor Einrichtung des Graduiertenkollegs in weiten Teilen durch diese Bezüge geprägt.
Mit dem Graduiertenkolleg wird diese "gelebte" Verflochtenheit von Logik und Mathematik/Informatik in Forschung und Lehre weiterhin intensiviert. Das Graduiertenkolleg will die vorhandene Kompetenz durch ein aufeinander abgestimmtes, attraktives Lehr- und Forschungsprogramm an Jüngere weitergeben. Weitere Details zum gesamten Graduiertenkolleg finden sich [hier].
Die Arbeitsgruppe für Rechnerarchitektur beschäftigt sich im Rahmen des Graduiertenkollegs mit (Bounded) Model Checking für Hybride Systeme: Zahlreiche eingebettete Systeme operieren mit oder bestehen selbst aus gekoppelten Netzwerken von sowohl diskreten als auch kontinuierlichen Komponenten. Das Verhalten solcher Komponenten kann ohne eine explizite Modellierung der Interaktion zwischen diskreten und kontinuierlichen Komponenten nicht verstanden werden. Werkzeuge zur Synthese und Simulation solcher Systeme existieren zwar, ihre Verifikation steht aber erst in den Anfängen.
Andererseits haben sich Model Checking und Bounded Model Checking im digitalen Hardwarebereich in den letzten Jahren etabliert. Eine erfolgreiche Übertragung dieser Ansätze auf den Bereich "Hybride
Systeme" ist Gegenstand dieses Projektes und erfordert insbesondere neue Überlegungen hinsichtlich der zu verwendenden Beweismethoden.