Towards a hybrid dynamic logic for hybrid dynamic systems

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.

@article{DBLP:journals/entcs/Platzer07,
	slides = {pub/hdL-slides.pdf},
	author = {['André 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', 'Thomas Bolander', 'Torben Braüner', 'Valeria de Paiva', 'Jørgen Villadsen']},
	series = {ENTCS},
	journal = {Electr. Notes Theor. Comput. Sci.},
	issn = {1571-0661},
	volume = {174},
	number = {6},
	month = {June},
	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.}
}