24.05.2026 –, Sprachschule 1: Argentinien Sprache: Deutsch
Im Gebiet der Softwarespezifikation und -verifikation sind Temporallogiken ein nützliches Mittel, um das Verhalten von Algorithmen zu beschreiben und ihre Eigenschaften zu formalisieren. So kann zum Beispiel die Korrektheit von nebenläufigen Programmen bewiesen werden, oder man kann Fehler in real existierender Software durch Finden von Gegenbeispielen aufzeigen.
Nach einer Diskussion wie man Softwareverhalten beschreiben kann, schauen wir uns die LTL (Lineare Temporallogik) an, wie deren Formeln aufgebaut sind und was sie bedeuten.
Danach betrachten wir die Variante TLA (Temporallogik der Aktionen) sowie dessen Softwareimplementierung TLA+; damit können wir Softwaresysteme beschreiben und computergestützt überprüfen.
Voraussetzungen: grundliegende Programmierkenntnisse (insbesondere boolesche Ausdrücke), keine Angst vor mathematischen Formeln. Ansonsten wird alles erklärt, ihr müsst nur zuhören und aufpassen.
