Stochastic differential dynamic logic for stochastic hybrid programs

@INPROCEEDINGS{DBLP:conf/cade/Platzer11,
	pdf = {pub/SdL.pdf},
	slides = {pub/SdL-slides.pdf},
	TR = {DBLP:conf/cade/Platzer11:TR},

  author    = {Andr{\'e} Platzer},
  title     = {Stochastic Differential Dynamic Logic for
               Stochastic Hybrid Programs},
  booktitle = {CADE},
  longbooktitle = {International Conference on Automated
               Deduction, {CADE-23}, Wroc{\l}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{\o}rner and
               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.
  }
}```