Logics of dynamical systems

We study the logic of dynamical systems, that is,
logics and proof principles for properties of dynamical
systems. Dynamical systems are mathematical models
describing how the state of a system evolves over time.
They are important in modeling and understanding many
applications, including embedded systems and
cyber-physical systems. In discrete dynamical systems,
the state evolves in discrete steps, one step at a
time, as described by a difference equation or discrete
state transition relation. In continuous dynamical
systems, the state evolves continuously along a
function, typically described by a differential
equation. Hybrid dynamical systems or hybrid systems
combine both discrete and continuous dynamics.

 This is a brief survey of differential dynamic logic
for specifying and verifying properties of hybrid
systems. We explain hybrid system models, differential
dynamic logic, its semantics, and its axiomatization
for proving logical formulas about hybrid systems. We
study differential invariants, i.e., induction
principles for differential equations. We briefly
survey theoretical results, including soundness and
completeness and deductive power. Differential dynamic
logic has been implemented in automatic and interactive
theorem provers and has been used successfully to
verify safety-critical applications in automotive,
aviation, railway, robotics, and analogue electrical
circuits.

@inproceedings{DBLP:conf/lics/Platzer12a,
	pdf = {pub/lds-lics.pdf},
	slides = {pub/lds-slides.pdf},
	author = {['André Platzer']},
	title = {Logics of Dynamical Systems},
	booktitle = {LICS},
	year = {2012},
	pages = {13-24},
	doi = {10.1109/LICS.2012.13},
	longbooktitle = {Proceedings of the 27th Annual ACM/IEEE
               Symposium on Logic in Computer Science, LICS
               2012, Dubrovnik, Croatia, June 25???28, 2012},
	publisher = {IEEE},
	isbn = {978-1-4673-2263-8},
	keywords = {logic of dynamical systems, dynamic logic,
               differential dynamic logic, hybrid systems,
               axiomatization, deduction},
	abstract = {
    We study the logic of dynamical systems, that is,
    logics and proof principles for properties of dynamical
    systems. Dynamical systems are mathematical models
    describing how the state of a system evolves over time.
    They are important in modeling and understanding many
    applications, including embedded systems and
    cyber-physical systems. In discrete dynamical systems,
    the state evolves in discrete steps, one step at a
    time, as described by a difference equation or discrete
    state transition relation. In continuous dynamical
    systems, the state evolves continuously along a
    function, typically described by a differential
    equation. Hybrid dynamical systems or hybrid systems
    combine both discrete and continuous dynamics.

     This is a brief survey of differential dynamic logic
    for specifying and verifying properties of hybrid
    systems. We explain hybrid system models, differential
    dynamic logic, its semantics, and its axiomatization
    for proving logical formulas about hybrid systems. We
    study differential invariants, i.e., induction
    principles for differential equations. We briefly
    survey theoretical results, including soundness and
    completeness and deductive power. Differential dynamic
    logic has been implemented in automatic and interactive
    theorem provers and has been used successfully to
    verify safety-critical applications in automotive,
    aviation, railway, robotics, and analogue electrical
    circuits.}
}