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
- Autor:
- Hölzl, Johannes
- Jahr:
- 2013
- Dokumenttyp:
- Dissertation
- Fakultät/School:
- 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.
- WWW:
- https://mediatum.ub.tum.de/?id=1116512
- Eingereicht am:
- 10.10.2012
- Mündliche Prüfung:
- 19.02.2013
- Dateigröße:
- 864893 bytes
- Seiten:
- 120
- Urn (Zitierfähige URL):
- https://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20130219-1116512-0-6
- Letzte Änderung:
- 28.11.2013
BibTeX