Brownian Motion in Isabelle/HOL

TL;DR

This paper presents a formal mechanisation of Brownian motion in Isabelle/HOL, enabling the specification and verification of stochastic hybrid systems with uncertainty in robotic controllers.

Contribution

It introduces a mechanisation of stochastic kernels and Markov semigroups in Isabelle/HOL, and proves the Kolmogorov-Chentsov theorem for stochastic process modifications.

Findings

Mechanisation of Brownian motion in Isabelle/HOL

Formal proof of the Kolmogorov-Chentsov theorem

Foundation for verifying stochastic hybrid systems

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\"older 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.