A temporal dynamic logic for verifying hybrid system invariants

@INPROCEEDINGS{DBLP:conf/lfcs/Platzer07,
	pdf = {pub/dTL.pdf},
	slides = {pub/dTL-slides.pdf},
	study = {info/KeYmaera.html#case-studies},
	TR = {DBLP:conf/lfcs/Platzer07:TR},

  author    = {Andr{\'e} Platzer},
  title     = {A Temporal Dynamic Logic for Verifying
               Hybrid System Invariants},
  booktitle = {LFCS},
  longbooktitle = {Logical Foundations of Computer Science,
               5th International Symposium, LFCS'07, New
               York, USA, June 4-7, 2007, Proceedings},
  year      = {2007},
  pages     = {457-471},
  doi       = {10.1007/978-3-540-72734-7_32},
  editor    = {Sergei N. Art{\"e}mov and
               Anil Nerode},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {4514},
  isbn      = {978-3-540-72732-3},
  keywords  = {dynamic logic, temporal logic, sequent
               calculus, logic for hybrid systems,
               deductive verification of embedded systems},
  abstract  = {
    We combine first-order dynamic logic for reasoning
    about possible behaviour of hybrid systems with
    temporal logic for reasoning about the temporal
    behaviour during their operation. Our logic supports
    verification of hybrid programs with first-order
    definable flows and provides a uniform treatment of
    discrete and continuous evolution. For our combined
    logic, we generalise the semantics of dynamic
    modalities to refer to hybrid traces instead of final
    states. Further, we prove that this gives a
    conservative extension of dynamic logic. On this basis,
    we provide a modular verification calculus that reduces
    correctness of temporal behaviour of hybrid systems to
    non-temporal reasoning. Using this calculus, we analyse
    safety invariants in a train control system and
    symbolically synthesise parametric safety constraints.
  }
}```