An Adequate While-Language for Stochastic Hybrid Computation

TL;DR

This paper introduces a formal language for reasoning about hybrid stochastic programs combining differential and probabilistic elements, supported by operational and denotational semantics with an adequacy theorem.

Contribution

It presents a new language for hybrid stochastic computation, along with semantics and an interpreter, enabling formal reasoning about complex probabilistic systems.

Findings

Developed an operational semantics and interpreter for the language.

Established an adequacy theorem linking operational and denotational semantics.

Demonstrated applicability to systems like Brownian motion and adaptive controllers.

Abstract

We introduce a language for formally reasoning about programs that combine differential constructs with probabilistic ones. The language harbours, for example, such systems as adaptive cruise controllers, continuous-time random walks, and physical processes involving multiple collisions, like in Einstein's Brownian motion. We furnish the language with an operational semantics and use it to implement a corresponding interpreter. We also present a complementary, denotational semantics and establish an adequacy theorem between both cases.