Building on previous work by Andre 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 works 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.
تحميل البحث