Detailseite
Projekt Druckansicht

Verifikation probabilistischer Modelle in interaktiven Theorembeweisern

Fachliche Zuordnung Theoretische Informatik
Förderung Förderung von 2013 bis 2016
Projektkennung Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 226793109
 
Erstellungsjahr 2018

Zusammenfassung der Projektergebnisse

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.

Projektbezogene Publikationen (Auswahl)

 
 

Zusatzinformationen

Textvergrößerung und Kontrastanpassung