A temporal dynamic logic for verifying hybrid system invariants

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.

@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é 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ëmov', '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.
  }
}