Construction and Stochastic Applications of Measure Spaces in Higher-Order Logic

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. 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.