Reduktionsmethoden zur Verifikation omega-regulärer und temporallogischer Eigenschaften für kommunizierende probabilistische Prozesse
Final Report Abstract
Probabilismus ist ein zentrales Konzept im Kontext der Modellierung und Analyse verteilter Systeme. Beispielsweise wird Randomisierung in zahlreichen Koordinationsalgorithmen für verteilte Systeme sowie Kommunikations- und kryptographischen Protokollen eingesetzt. Die Zielsetzung des Projekts war eine detaillierte Untersuchung von Reduktionsmethoden für probabilistische verteilte Systeme, welche die Systemanalyse unter quantitativen Aspekten unterstützen. Das Projekt befasste sich sowohl mit den theoretischen Grundlagen der Partial Order Reduction und hierzu komplementären Abstraktionstechniken als auch deren praktische Umsetzung durch die Entwicklung und Implementierung eines entsprechenden Werkzeugs. Als operationelles Systemmodell wurden diskrete Markov Entscheidungsprozesse, sowie Varianten hiervon mit Kostenfunktionen oder Fairnessannahmen, verwendet. Zur Formalisierung der Eigenschaften haben wir deterministische ω-Automaten und Formeln der temporalen Logiken LTL (linear temporal logic) und PCTL/PCTL*(probabilistic computation tree logic) betrachtet. Wie im nichtprobabilistischen Fall beruht die Partial Order Reduction auf der Kommutativität unabhängiger Aktionen, jedoch stellt sich hier die zusätzliche Schwierigkeit, dass α; (β1 + β2) nicht denselben Effekt wie (β1+β2); α hat, sofern α eine probabilistische Aktion und β1, β2 beliebige Aktionen sind. (Dabei stehen ; und + für sequentielle Komposition bzw. nichtdeterministische Auswahl.) Dieses für den probabilistischen Fall spezifische Phänomen machte stärkere Bedingungen als im nichtprobabilistischen Fall erforderlich. In experimentellen Studien war die Reduktionsgüte dennoch vergleichbar mit dem nichtprobabilistischen Fall. Das Projekt befasste sich auch mit Methoden, die die für die quantitative Analyse zu lösenden linearen Programme vereinfachen und mit Algorithmen, die gestartet mit einer LTL Formel einen möglichst kompakten deterministischen Automaten zu konstruieren versuchen. Unsere Untersuchungen zu probabilistischen Automaten zur Darstellung ω-regulärer Eigenschaften erwiesen sich zwar auf Grund von Unentscheidbarkeitsergebnissen als Irrweg bezogen auf deren Einsatz im Kontext von probabilistischem Model Checking. Dennoch stellte sich das Konzept von probabilistischen Büchi Automaten als sehr interessant heraus, da sie sich durch eine Reihe bemerkenswerter Eigenschaften auszeichnen und eine konzeptionelle Nähe zu probabilistischen Modellen für verteilte Systeme aufweisen, in denen die einzelnen Komponenten nur partielle Information über die globalen Zustände haben.
