About the event

This course studies 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 combining cyber effects with physical effects. 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 course, coordinated by Prof. André Platzer from Carnegie Mellon University, explores the theory, practice, and applications of the family of differential dynamic logics, which includes logics for hybrid systems and extensions to distributed hybrid systems and hybrid games. It explains dynamical system models, logics of dynamical systems, their semantics, and their axiomatization for proving logical formulas about dynamical systems. We study differential invariants, i.e., induction principles for differential equations. We survey theoretical results, including soundness and completeness and deductive power, and discuss algorithmic implications. Differential dynamic logics have been implemented in automatic and interactive theorem provers and have been used successfully to verify safety-critical applications in automotive, aviation, railway, and robotic domains. 

The results discussed in this course demonstrate that logic is a powerful tool, not just for studying discrete phenomena, but also continuous, distributed, and adversarial dynamics. Dynamic logics provide a strong logical foundation for dynamical systems, including cyber-physical systems. Such stable foundations for a relatively young area make it a promising direction for future research that is unique in its manifold connections to other pure and applied sciences. Given the tremendous progress that logic for classical software has made since its conception, we expect to see no less from the area of logics for dynamical systems in which programs reach out into the physical world.
 

Participants

The course is part of the MAP-i Thematic Seminar, but open to post-grad students and researchers from the MAP Universities and Research Units.
All participants are required to attend all lectures and lab sessions along the whole week. They are also supposed to previously install the course tools — KEYMAERA and MATHEMATICA — on their laptops. Instructions and the course schedule are available from the MAP-i website
 

Lecturers from CMU

André Platzer
Sarah Loos
João Martins

Venue:

Departamento de Informática
Campus de Gualtar
Universidade do Minho

Course Schedule:

available from the MAP-i website

Registration:

By email to lsb@di.uminho.pt until 14th March
Please note that attendance is free but registration is mandatory.