Benutzer: Gast  Login
Originaltitel:
Construction and Stochastic Applications of Measure Spaces in Higher-Order Logic 
Übersetzter Titel:
Konstruktion und stochastische Anwendungen von Maßräumen in höherstufiger Logik 
Jahr:
2013 
Dokumenttyp:
Dissertation 
Institution:
Fakultät für Informatik 
Betreuer:
Nipkow, Tobias (Prof., Ph.D.) 
Gutachter:
Nipkow, Tobias (Prof., Ph.D.); Esparza Estaun, Francisco Javier (Prof. Dr. Dr. h.c.) 
Sprache:
en 
Fachgebiet:
DAT Datenverarbeitung, Informatik 
Stichworte:
Interactive Theorem Proving, Probability Theory, Markov Chains 
Übersetzte Stichworte:
Interaktives Theorembeweisen, Wahrscheinlichkeitstheorie, Markov-Ketten 
Schlagworte (SWD):
Markov-Kette; Automatisches Beweisverfahren; Isabelle Programm; HOL 
TU-Systematik:
DAT 706d; MAT 607d 
Kurzfassung:
The goal of this work is the verification of probabilistic systems in the interactive theorem prover Isabelle/HOL. This requires the formalization of probability theory. We construct probability spaces with infinitely many independent random variables and the stochastic process of a Markov chain. We use these probability spaces to verify the correctness of probabilistic model checking and to verify properties of the ZeroConf protocol and the Crowds protocol. 
Übersetzte Kurzfassung:
Ziel dieser Arbeit ist die Verifikation probabilistischer Systeme in dem interaktiven Theorembeweiser Isabelle/HOL. Dies setzt die Formalisierung von Wahrscheinlichkeitstheorie voraus. Wir konstruieren W-Räume mit unendlich vielen, unabhängigen Zufallsvariablen und den zu einer Markov-Kette gehörenden stochastischen Prozess. Wir verwenden diese W-Räume um die Korrektheit von probabilistischem Model Checking und Eigenschaften des ZeroConf-Protokolls und des Crowds-Protokoll zu verifizieren. 
Mündliche Prüfung:
19.02.2013 
Dateigröße:
864893 bytes 
Seiten:
120 
Letzte Änderung:
28.11.2013