Nondeterministic Stochastic Differential Dynamic Logic

Abstract. Complex hybrid systems can have several sources of uncertainty. Un-controllable events that change the state of the system and can be triggered un-predictably or adversarially are typically modelled as nondeterministic whereas events to which we can attribute some likelihood, either because of their funda-mental nature or because of simplifying assumptions, are typically modelled as stochastic. Although logic and theorem proving have been successfully used to reason about the possibility of events in nondeterministic hybrid systems and to reason about the probability of events in fully stochastic hybrid systems, the in-teractions between both kinds of uncertainty generate non trivial dynamics and these approaches cannot be easily merged. Herein, we introduce Nondeterminis-tic Stochastic Differential Dynamic Logic (NSdL), a logical framework over non-deterministic stochastic hybrid systems that allows for reasoning about the possi-ble probabilities of events. We introduce a model for Nondeterministic Stochastic Hybrid Systems and prove that the semantics for such models are measurable. We present compositional proof rules for a large fragment of the logic and prove their soundness. We exemplify the calculus with a version of an aircraft controller model that had previously been stripped of probabilism