Advanced weakest precondition calculi for probabilistic programs

• Erweiterte wp-Kalküle für Probabilistische Programme

Kaminski, Benjamin Lucien; Katoen, Joost-Pieter (Thesis advisor); McIver, Annabelle (Thesis advisor)

Aachen (2019)
Doktorarbeit

Dissertation, RWTH Aachen University, 2019

Kurzfassung

Wir studieren die quantitative Analyse probabilistischer Programme. Dabei untersuchen wir vornehmlich zwei Aspekte: Die Analysetechniken selbst, sowie die komplexitäts- bzw. berechenbarkeitstheoretische Schwere der entsprechenden Analyseprobleme. In Bezug auf die Analysetechniken geben wir zunächst eine umfassende Einführung in den Kalkül der Schwächsten Vorerwartungen à la McIver & Morgan - ein Kalkül für die Verifikation probabilistischer Programme, der auf Dijkstras Kalkül der Schwächsten Vorbedingungen für Programme mit Nichtdeterminismus und Kozens Probabilistischer Dynamischer Aussagenlogik für probabilistische Programme aufbaut. Anschließend entwickeln wir weitergehende Kalküle für probabilistische Programme im Stile McIver & Morgans, welche dazu geeignet sind, Analysen über - erwartete Laufzeiten, - bedingte Erwartungswerte und bedingte Wahrscheinlichkeiten, und - Erwartungswerte von Zufallsvariablen mit gemischtem Vorzeichen zu fahren. Wie auch Dijkstras Kalkül sind unsere Kalküle induktiv über die Programmstruktur definiert und erlauben somit eine modulare Analyse auf Quelltextebene. Ein besonderes Augenmerk legen wir auf Regeln, welche die Analyse von Schleifen ermöglichen. Der zweite Aspekt, den wir untersuchen, ist die inhärente berechenbarkeitstheoretische Schwere der Analyse probabilistischer Programme, welche unabhängig von der verwendeten Analysetechnik selbst ist. Im Speziellen untersuchen wir dazu die Schwere der Approximation von Erwartungswerten und Kovarianzen. Wir zeigen, dass untere Schranken für Erwartungswerte nicht berechenbar, aber rekursiv aufzählbar sind, obere Schranken jedoch nicht rekursiv aufzählbar sind. Für Kovarianzen zeigen wir, dass weder obere noch untere Schranken rekursiv aufzählbar sind. Desweiteren untersuchen wir die Schwere der Entscheidbarkeit der Terminierung probabilistischer Programme. Während wir dazu zwar unterschiedliche Auffassungen eines probabilistischen Terminierungsbegriffs untersuchen, beispielsweise fast-sichere Terminierung oder Terminierung innerhalb endlicher erwarteter Zeit (auch positive fast-sichere Terminierung genannt), zeigen wir, dass die Terminierung probabilistischer Programme im Allgemeinen echt schwerer zu entscheiden ist als die Terminierung nicht-probabilistischer Programme.