Projektstart: 01.01.2006

Projektträger: Universität Augsburg

Projektverantwortung vor Ort: Prof. Dr. Bernhard Möller

Beteiligte WissenschaftlerInnen der Universität Augsburg: Roland Glück, Dr. Peter Höfner , Han-Hing Dang

Beteiligte WissenschaftlerInnen / Kooperationen: Prof. Dr. Jules Desharnais (Université Laval), Dr. Georg, Struth (University of Sheffield) und andere

Zusammenfassung

Halbringe treten in vielen Bereichen der Informatik auf. Sie charakterisieren die fundamentalen Operationen + (Auswahl) und ⋅ (sequentielle Komposition). Häufig lassen sich die Halbringelemente als Mengen von Abläufen interpretieren. Tests sind spezielle Halbringelemente, die Mengen von Abläufen der Länge 1, d.h. Mengen von Zuständen, repräsentieren. Sie spielen die Rolle von Zusicherungen in der Programmverifikation. Die Vor- und Nachbereichsoperatoren liefern Tests, die die Anfangs- und Endzustände einer Menge von Abläufen charakterisieren. Mit ihrer Hilfe lassen sich Diamant- und Box-Operatoren definieren, die die Verbindung zur modalen Logik und dem μ-Kalkül herstellen.