Stochastic Differential Dynamic Logic for Stochastic Hybrid Systems

Overview

Stochastic hybrid systems are systems with interacting discrete, continuous, and stochastic dynamics. There is not just one canonical way to add stochastic behavior to a system model. Stochasticity might be restricted to the discrete dynamics, as in piecewise deterministic MDPs, restricted to the continuous and switching behavior as in switching diffusion processes, or allowed in different parts as in a model called General Stochastic Hybrid Systems. Several different forms of combinations of probabilities with hybrid systems and continuous systems have been considered, both for model checking and for simulation-based validation.

We develop a very different approach. We consider logic and theorem proving for stochastic hybrid systems to transfer the success that logic has had in other domains. We develop stochastic differential dynamic logic [2], the first logic and the first compositional verification approach for stochastic hybrid systems.

The processes generating the above sample paths have been verified with stochastic differential dynamic logic [2].

Abstract

Logic is a powerful tool for analyzing and verifying systems, including programs, discrete systems, real-time systems, hybrid systems, and distributed systems. Some applications also have a stochastic behavior, however, either because of fundamental properties of nature, uncertain environments, or simplifications to overcome complexity. Discrete probabilistic systems have been studied using logic. But logic has been chronically underdeveloped in the context of stochastic hybrid systems, i.e., systems with interacting discrete, continuous, and stochastic dynamics. We aim at overcoming this deficiency and introduce a dynamic logic for stochastic hybrid systems. Our results indicate that logic is a promising tool for understanding stochastic hybrid systems and can help taming some of their complexity. We introduce a compositional model for stochastic hybrid systems. We prove adaptivity, càdlàg, and Markov time properties, and prove that the semantics of our logic is measurable. We present compositional proof rules, including rules for stochastic differential equations, and prove soundness.

Keywords: Dynamic logic, Proof calculus, Stochastic differential equations, Stochastic hybrid systems, Stochastic processes

Selected Publications

Also see publications on stochastic hybrid systems logic and the publication reading guide.

1. André Platzer.
   Dynamic logics of dynamical systems.
   arXiv:1205.4788, May 2012. Long version of LICS'12 invited tutorial.
   [bib | ⧉ | pdf | arXiv | LICS'12 | abstract]
   
   
2. André Platzer.
   Stochastic differential dynamic logic for stochastic hybrid programs.
   In Nikolaj Bjørner and Viorica Sofronie-Stokkermans, editors, International Conference on Automated Deduction, CADE-23, Wroclaw, Poland, Proceedings, volume 6803 of LNCS, pp. 446-460. Springer, 2011. © Springer
   [bib | ⧉ | pdf | doi | slides | TR | abstract]
   
   
3. André Platzer.
   Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs.
   School of Computer Science, Carnegie Mellon University, CMU-CS-11-111, 2011.
   [bib | ⧉ | pdf | CADE]
   
   

Any opinions, findings, and conclusions or recommendations expressed are those of the author(s) and do not necessarily reflect the views of any sponsoring institution.