Stochastic differential dynamic logic for stochastic hybrid programs

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, cadlag, 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.

@inproceedings{DBLP:conf/cade/Platzer11,
	pdf = {pub/SdL.pdf},
	slides = {pub/SdL-slides.pdf},
	TR = {DBLP:conf/cade/Platzer11:TR},
	author = {['André Platzer']},
	title = {Stochastic Differential Dynamic Logic for
               Stochastic Hybrid Programs},
	booktitle = {CADE},
	longbooktitle = {International Conference on Automated
               Deduction, CADE-23, Wrocław, Poland,
               Proceedings},
	year = {2011},
	pages = {446-460},
	doi = {10.1007/978-3-642-22438-6_34},
	keywords = {dynamic logic, proof calculus,
               stochastic differential equations,
               stochastic hybrid systems,
               stochastic processes},
	editor = {['Nikolaj Bjørner', 'Viorica Sofronie-Stokkermans']},
	publisher = {Springer},
	series = {LNCS},
	volume = {6803},
	isbn = {},
	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, cadlag, 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.
  }
}