Temporale Logik hat sich seit Beginn der achziger Jahre zunehmend als ein geeignetes Werkzeug zur Spezifikation und Verifikation verteilter Systeme durchgesetzt. Die Idee, ein verteiltes System durch eine logische Formel zu repräsentieren, stammte ursprünglich von Amir Pnueli und wurde dann in verschiedenen Formalismen angewandt.
Eine spezielle temporale Logik ist die Temporal Logic of Actions (kurz: TLA) von Leslie Lamport. TLA löst einige grundlegende Probleme zur Systemmodellierung besonders überzeugend: Ein System wird durch seine entscheidenden Eigenschaften modelliert; letztlich als (i.a. sehr umfangreiche) TLA-Formel. Systematisches Verfeinern ergibt dann eine Darstellung, die unmittelbar als Programm auffassbar ist. Verifikation reduziert sich somit auf logische Implikation. TLA basiert auf sog. Stottersequenzen, die es erlauben, Systemspezifikationen auf einfache Weise per Konjunktion zu komponieren, um die Spezifikation eines parallelen Gesamtsystems zu erhalten („Komposition ist Konjunktion“). Verschiedene Arten der parallelen Komposition in TLA werden untersucht. Einen systematischen Überblick hierfür bietet die Studienarbeit Parallele Komposition in TLA.
Am Lehrstuhl entstand eine neue temporale Logik, die Temporal Logic of Distributed Actions (kurz: TLDA). Mit einer speziellen Interpretation von Variablen zur Synchronisation von Aktionen wird sie über verteilten Abläufen interpretiert und basiert im Gegensatz zu TLA auf kausal geordneten Ereignissen. Dies erlaubt eine feinere Unterscheidung der Phänomene, die im zu spezifizierenden System auftreten, wie z. B. Nebenläufigkeit und Nichtdeterminismus. Die Komponierbarkeit der Spezifikationen bleibt dabei erhalten, sodass sich mit TLDA besonders gut solche Systeme modellieren lassen, die aus Komponenten aufgebaut sind und deren Aktionen synchronisierend miteinander interagieren.