Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Brownian Motion in Isabelle/HOL

Christian Pardillo Laursen, Simon Foster, Mark Post

TL;DR

A mechanisation of Brownian motion within Isabelle/HOL is presented and the Kolmogorov-Chentsov theorem is proved, which paves the way for modelling and verifying stochastic hybrid systems in Isabelle/HOL.

Abstract

In order to formally verify robotic controllers, we must tackle the inherent uncertainty of sensing and actuation in a physical environment. We can model uncertainty using stochastic hybrid systems, which combine discrete jumps with continuous, stochastic behaviour. The verification of these systems is intractable for state-exploration based approaches, so we instead propose a deductive verification approach. As a first step towards a deductive verification tool, we present a mechanisation of Brownian motion within Isabelle/HOL. For this, we mechanise stochastic kernels and Markov semigroups, which allow us to specify a range of processes with stationary, independent increments. Further, we prove the Kolmogorov-Chentsov theorem, which allows us to construct Hölder continuous modifications of processes that satisfy certain bounds on their expectation. This paves the way for modelling and verifying stochastic hybrid systems in Isabelle/HOL.

Brownian Motion in Isabelle/HOL

TL;DR

A mechanisation of Brownian motion within Isabelle/HOL is presented and the Kolmogorov-Chentsov theorem is proved, which paves the way for modelling and verifying stochastic hybrid systems in Isabelle/HOL.

Abstract

In order to formally verify robotic controllers, we must tackle the inherent uncertainty of sensing and actuation in a physical environment. We can model uncertainty using stochastic hybrid systems, which combine discrete jumps with continuous, stochastic behaviour. The verification of these systems is intractable for state-exploration based approaches, so we instead propose a deductive verification approach. As a first step towards a deductive verification tool, we present a mechanisation of Brownian motion within Isabelle/HOL. For this, we mechanise stochastic kernels and Markov semigroups, which allow us to specify a range of processes with stationary, independent increments. Further, we prove the Kolmogorov-Chentsov theorem, which allows us to construct Hölder continuous modifications of processes that satisfy certain bounds on their expectation. This paves the way for modelling and verifying stochastic hybrid systems in Isabelle/HOL.

Paper Structure

This paper contains 18 sections, 6 theorems, 28 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Modelling stochastic hybrid systems
  3. Mathematical background
  4. Stochastic processes
  5. Comparing processes
  6. Convergence in measure
  7. Transition kernels
  8. Kernel Product
  9. Markov semigroups
  10. Kolmogorov-Chentsov
  11. Hölder continuity
  12. Kolmogorov-Chentsov theorem
  13. Constructing Brownian motion
  14. Evaluation
  15. Question 1: How well do textbook mathematics lend themselves to mechanisation?
  16. ...and 3 more sections

Key Result

lemma \@thmcounterlemma

Let $X$ and $Y$ be stochastic processes into a metric space $(S, d)$ which are modifications of each other, and that their index takes the form $[0,T]$. Assume that $X$ and $Y$ are almost surely continuous. Then $X$ and $Y$ are indistinguishable.

Figures (1)

  • Figure 1: Thermostat hybrid automaton and simulation, adapted from Henzinger henzinger00

Theorems & Definitions (7)

  • lemma \@thmcounterlemma
  • lemma \@thmcounterlemma
  • lemma \@thmcounterlemma
  • lemma \@thmcounterlemma
  • lemma \@thmcounterlemma
  • theorem \@thmcountertheorem
  • proof