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
- Author:
- Hölzl, Johannes
- Year:
- 2013
- Document type:
- Dissertation
- Faculty/School:
- 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.
- WWW:
- https://mediatum.ub.tum.de/?id=1116512
- Date of submission:
- 10.10.2012
- Oral examination:
- 19.02.2013
- File size:
- 864893 bytes
- Pages:
- 120
- Urn (citeable URL):
- https://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20130219-1116512-0-6
- Last change:
- 28.11.2013
BibTeX