Brownian Motion in Isabelle/HOL
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913554102222848 |
|---|---|
| author | Laursen, Christian Pardillo Foster, Simon Post, Mark |
| author_facet | Laursen, Christian Pardillo Foster, Simon Post, Mark |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_14718 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Brownian Motion in Isabelle/HOL Laursen, Christian Pardillo Foster, Simon Post, Mark Logic in Computer Science 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. |
| title | Brownian Motion in Isabelle/HOL |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2410.14718 |