Die meisten heute verwendeten Verfahren zur formalen Spezifikation und Verifikation von komplexen verteilten Systemen basieren auf klassischen zweiwertigen Logiken (z.B. Aussagenlogik, Modallogik, Prädikatenlogik). Für klassische Logiken wird die zur Darstellung von dynamischem Verhalten nötige Ausdruckskraft in erster Linie durch Erweiterung der sprachlichen Ausdrucksmittel erreicht. Ein grundsätzlich anderer Ansatz besteht darin, nicht die Syntax der logischen Sprache, sondern die Reichhaltigkeit ihrer Wahrheitswerte zu erhöhen. Eine der bedeutendsten mehrwertigen Logiken, die intuitionistische Logik, wurde wegen ihrer höheren beweis- und modelltheoretischen Komplexität in diesem Zusammenhang bisher kaum beachtet.
In diesem Projekt wird eine intuitionistischen Modallogik, die sogenannte Laxe Logik für die Verzögerungsanalyse kombinatorischer Systeme eingesetzt. Dies führt auf einen neuartigen Ansatz zur Analyse datenabhängiger Verzögerungszeiten, der sich gegenüber den herkömmlichen algorithmenorientierten Verfahren in seiner semantischen Fundierung, seiner Exaktheit und seiner inhärenten Kompositionalität auszeichnet. Eine Reihe bekannter Algorithmen zur Verzögerungsanalyse sind auf diese Weise erstmalig semantisch präzise charakterisierbar. Die methodische Trennung von temporalen und funktionalen Aspekten in Laxer Logik erlaubt dabei eine nahtlose Integration von Verzögerungsanalysealgorithmen und programmiersprachlichen Typprüfungsverfahren.