Vorlesung Verifikation unendlicher Systeme (SS 2010)

Vorlesung im Master-Vertiefungsmodul 10-202-2110

Organisatorisches


Übersicht

Systeme mit unendlichen Zustandsräumen treten insbesondere bei der Modellisierung von Softwaresystemen auf, z. B. auf Grund von Variablen mit unendlichen Wertebereichen. Solche Systeme lassen sich abstrakt durch unendliche Transitionsysteme (Graphen) beschreiben. In der Vorlesung werden wir verschiedene Formalismen zur Beschreibung unendlicher Transitionssysteme kennenlernen (z. B. Pushdownsysteme, automatische Graphen). Wir werden sodann untersuchen, welche algorithmischen Eigenschaften solcher Systeme entscheidbar bleiben. Systemeigenschaften werden dabei in geeigneten Logiken, insbesondere temporalen Logiken (LTL, CTL), formalisiert.

Folien (Version vom 14.06.2010)


Übungsblätter


Java-Applets (von Roy Mennicke)


Software


Literatur


Impressum
Last modified: Thu Oct 2 19:10:17 CEST 2003