Towards a hybrid dynamic logic for hybrid dynamic systems

@ARTICLE{DBLP:journals/entcs/Platzer07,
	slides = {pub/hdL-slides.pdf},

  author    = {Andr{\'e} Platzer},
  title     = {Towards a Hybrid Dynamic Logic for Hybrid
               Dynamic Systems},
  booktitle = {International Workshop on Hybrid Logic,
               HyLo'06, Seattle, USA, Proceedings},
  year      = {2007},
  editor    = {Patrick Blackburn and
               Thomas Bolander and
               Torben Bra\"{u}ner and
               Valeria de Paiva and
               J{\o}rgen Villadsen},
  series    = {ENTCS},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  issn      = {1571-0661},
  volume    = {174},
  number    = {6},
  month     = {Jun},
  pages     = {63-77},
  doi       = {10.1016/j.entcs.2006.11.026},
  pdf       = {https://lfcps.org/pub/hdL.pdf},
  keywords  = {hybrid logic, dynamic logic, sequent
               calculus, compositional verification,
               real-time hybrid dynamic systems},
  abstract  = {
    We introduce a hybrid variant of a dynamic logic with
    continuous state transitions along differential
    equations, and we present a sequent calculus for this
    extended hybrid dynamic logic. With the addition of
    satisfaction operators, this hybrid logic provides
    improved system introspection by referring to
    properties of states during system evolution. In
    addition to this, our calculus introduces state-based
    reasoning as a paradigm for delaying expansion of
    transitions using nominals as symbolic state labels.
    With these extensions, our hybrid dynamic logic
    advances the capabilities for compositional reasoning
    about (semialgebraic) hybrid dynamic systems. Moreover,
    the constructive reasoning support for goal-oriented
    analytic verification of hybrid dynamic systems carries
    over from the base calculus to our extended calculus.},
}```