Semantics and Axiomatization for Stochastic Differential Dynamic Logic

TL;DR

This paper develops a formal language and semantics for Stochastic Differential Dynamic Logic, improving its expressiveness and compatibility with traditional logic, and introduces a practical calculus for implementation.

Contribution

It extends previous work by defining a more expressive and compatible logic with a new semantics, and introduces a Uniform Substitution calculus for practical proof implementation.

Findings

Resolved well-definedness issues in the semantics.

Enhanced logic expressiveness with nondeterministic choice and differential terms.

First Uniform Substitution calculus for stochastic differential logic.

Abstract

Building on previous work by Andr\'e Platzer, we present a formal language for Stochastic Differential Dynamic Logic, and define its semantics, axioms and inference rules. Compared to the previous effort, our account of the Stochastic Differential Dynamic Logic follows closer to and is more compatible with the traditional account of the regular Differential Dynamic Logic. We resolve an issue with the well-definedness of the original work's semantics, while showing how to make the logic more expressive by incorporating nondeterministic choice, definite descriptions and differential terms. Definite descriptions necessitate using a three-valued truth semantics. We also give the first Uniform Substitution calculus for Stochastic Differential Dynamic Logic, making it more practical to implement in proof assistants.