Synthese Verteilter Systeme

Abstract

Verteilte und parallele Systeme haben einen stetig wachsenden Einfluß auf unser Leben, ob versteckt, wie in der Steuerung unseres Airbags oder ABS, oder offen, wie in Transaktionssystemen. Fehlerhafte Systeme gefährden oft Leben oder Gesundheit und können erhebliche Kosten verursachen. Für die Informatik ergibt sich daraus das zentrale Ziel, eine mathematische Fundierung für die Entwicklung solcher Systeme zu schaffen. Die vorgestellte Arbeit liefert hierzu einen zentralen Beitrag: Sie löst das Syntheseproblem für verteilte Systeme. Synthese ist das klassische Wunschziel der Informatik, eine Implementierung automatisch aus ihrer Spezifikation abzuleiten. Die Wurzeln des Syntheseproblems für verteilte Systeme reichen ein halbes Jahrhundert auf Alonzo Churchs berühmtes Lösbarkeitsproblem zurück. Die vielen seit damals entstandenen Arbeiten bieten Lösungsansätze für spezielle Systemarchitekturen, etwa Pipelines oder Ringe, und eingeschränkte Spezifikationssprachen wie zum Beispiel temporale Logiken; gleichzeitig wurde für einzelne Architekturen gezeigt, dass verteilte Synthese unentscheidbar ist. Aber die fundamentale Frage nach den tieferen Ursachen für die Unentscheidbarkeit, und eine damit mögliche Charakterisierung aller Systemarchitekturen, für die das Syntheseproblem grundsätzlich lösbar ist, blieb offen. Meine Dissertation gibt eine vollständige Charakterisierung der Systemarchitekturen, für die automatische Synthese möglich ist, das Information-Fork Kriterium, und stellt eine uniforme Entscheidungsprozedur für alle entscheidbaren Fälle vor.