User: Guest  Login
Original title:
Construction and Stochastic Applications of Measure Spaces in Higher-Order Logic 
Translated title:
Konstruktion und stochastische Anwendungen von Maßräumen in höherstufiger Logik 
Year:
2013 
Document type:
Dissertation 
Institution:
Fakultät für Informatik 
Advisor:
Nipkow, Tobias (Prof., Ph.D.) 
Referee:
Nipkow, Tobias (Prof., Ph.D.); Esparza Estaun, Francisco Javier (Prof. Dr. Dr. h.c.) 
Language:
en 
Subject group:
DAT Datenverarbeitung, Informatik 
Keywords:
Interactive Theorem Proving, Probability Theory, Markov Chains 
Translated keywords:
Interaktives Theorembeweisen, Wahrscheinlichkeitstheorie, Markov-Ketten 
Controlled terms:
Markov-Kette; Automatisches Beweisverfahren; Isabelle Programm; HOL 
TUM classification:
DAT 706d; MAT 607d 
Abstract:
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. 
Translated abstract:
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. 
Oral examination:
19.02.2013 
File size:
864893 bytes 
Pages:
120 
Last change:
28.11.2013