Towards a Hybrid Dynamic Logic for Hybrid Dynamic Systems

9 years 8 months ago
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.
André Platzer
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2007
Authors André Platzer
Comments (0)