Verification of Probabilistic Models in Interactive Theorem Provers
Final Report Abstract
Viele Systeme in der Natur und in der Informatik sind probabilistisch. In der Informatik wird der Zufall sogar häufig dazu verwendet, Systeme robuster oder effizienter zu machen. Model Checking ist ein Methode, für Systeme mit endlichem Zustandsraum automatisch zu zu beweisen (zu „verifizieren“), dass sie den Anforderungen (der „Spezifikation“) genügen. Die zweite wichtige Verifikationstechnik in der Informatik ist die interaktive Verifikation mit einem Theorembeweiser. Ziel des Projekts war es, die mathematische Basis probabilistischer Systeme in einem Theorembeweiser zu formalisieren, um damit auch komplexe Algorithmen und Systeme verifizieren zu können, die sich nicht mehr automatisch behandeln lassen. Insbesondere kann damit die Vertrauenswürdigkeit von Model Checkern erhoht werden (durch die Verifikation der zu Grunde liegenden Algorithmen oder einzelner Läufe eines Model Checkers). Die Hauptergebnisse des Projekts sind die Formalisierungen von Teilen der Wahrscheinlichkeitstheorie und des probabilitischen Model Checkings mit Hilfe des Theorembeweisers Isabelle. Unter einer Formalisierung verstehen wir eine vom Menschen erstellte und von der Maschine (Isabelle) auf mathematische Korrektheit überprüfte Sammlung von Definitionen, Algorithmen und Beweisen. Besonderer Schwerpunkt war die Theorie der Markow-Ketten und Markow-Entscheidungsprozesse. Für den diskreten Fall konnte beide Modelle formalisiert werden. Für den kontinuierlichen Fall haben wir bisher nur Markow-Ketten formalisiert. Dabei wurden auch Fehler in der Literatur gefunden, was zeigt, dass die interaktive Verifikation die Verlässlichkeit von Informatik-Systemen erhöht. Unsere Ergebnisse sind ein wichtiger Beitrag zu dem globalen Projekt der Formalisierung der mathematischen Grundlagen der Informatik. Sie sind verfügbar im Archive of Formal Proofs [KNP], einem online Archiv von auf einander aufbauenden Formalisierungen mathematischen Theorien in Isabelle.
Publications
- A Formalized Hierarchy of Probabilistic System Types - Proof Pearl. , Dmitriy Traytel. Interactive Theorem Proving (ITP 2015)
Johannes Hölzl, Andreas Lochbihler
(See online at https://dx.doi.org/10.1007/978-3-319-22102-1_13) - A Verified Compiler for Probability Density Functions. European Symposium on Programming (ESOP 2015)
Manuel Eberl, Johannes Hölzl, Tobias Nipkow
(See online at https://dx.doi.org/10.1007/978-3-662-46669-8_4) - Markov Chains and Markov Decision Processes in Isabelle/HOL. Journal of Automated Reasoning 59(3): pp. 345–387 (2017)
Johannes Hölzl
(See online at https://doi.org/10.1007/s10817-016-9401-5) - Markov processes in Isabelle/HOL. Certified Programs and Proofs (CPP 2017)
Johannes Hölzl
(See online at https://dx.doi.org/10.1145/3018610.3018628)
