Modal and Temporal Logic

Die Verifikation der funktionalen Korrektheit von Algorithmen und die funktionale Analyse verteilter und reaktiver Systeme erfordert nicht nur quantitative sondern vor allem logisch-symbolische Verfahren. Auch viele Steuerungsprobleme in Anwendungsfeldern wie der Robotik, intelligenten autonomen Agenten oder in Sicherheitsprotokollen lassen sich nur schwer mit herkömmlichen analytisch-numerischen Methoden behandeln. Dank der sich kontinuierlich verbessernden Leistungsfähigkeit moderner Rechner und der Erfolge im Gebiet der Computational Logic erschließen sich der formalen Logik in der Informationstechnik  immer weitere Anwendungsmöglichkeiten.

Die Vorlesung gibt einen Einblick in die Theorie und Anwendung der Modallogik als gemeinsame Grundlage der wichtigsten informatikrelevanten Logiken (Wissenslogiken, Zeitlogiken, Prozesslogik, Sicherheitslogik, usw.). Sie stellt zugehörige Semantiken und Entscheidungsverfahren vor und zeigt typische Anwendungen auf.