15-424: Foundations of Cyber-Physical Systems (Fa'13)

Table of Contents
FAQ Should I take this course? What do I need to know coming into this course? What time commitment does this course need to succeed? KeYmaera Usage Further Reading Ordinary Differential Equations First-Order Logic

FAQ

Should I take this course?

You should definitely take this course if

• you ever want to program robots, or
• you ever want to develop computer control systems for cars, or
• you ever want to write programs that control aircraft or UAV, or
• you ever want to help computers control power plants or the smart grid, or
• you want to do embedded systems or cyber-physical systems, or
• you are interested in learning how computation interfaces with the real world, or
• you are simply fascinated by combining mathematics and computer science, or
• you want to see logic matter in reality

If none of those reasons apply to you, don't take this course. But, if you don't take this course, then please, pretty please, also don't ever try to write programs for any embedded or cyber-physical systems. If you, nevertheless, face the design challenges of making computers help us control those systems (and the chances of that happening are pretty big), then please go back and revisit the lecture material first.

What do I need to know coming into this course?

The formal requirements for the course are listed in the course prerequisites.

If you are afraid of programming or afraid of mathematics, then you will find this course more challenging. The course does not require particularly advanced mathematical background, but you should feel comfortable picking the required concepts up as we go. We will explain what you need to know in the course and provide pointers to further reading material. Coming into this course, you should definitely already know what a derivative is and have an intuitive understanding of differential equations. We will go over what you need to know. We will frequently need things like the following differential equation

x'=v,v'=a which can be understood as the time-derivative of x is v, and the time-derivative of v is a. In other words, this differential equation means that the derivative of the position x is the velocity v, and the derivative of the velocity v is the acceleration a.

We suggest that you look at Further Reading material for this course.

What time commitment does this course need to succeed?

The course is a 12 unit course and includes both lectures and recitations. Both the theory homework and the labs are alternating every two weeks. So there's an assignment due every week, either the theory or the lab, but never both.

How much time you need to complete this course depends on how easy the material comes to you. The course will certainly be challenging. It will not be challenging because of sheer volume of things that we demand you do. Instead, the challenges will be of a more conceptual nature. If everything comes quite natural to you, you can be done quickly. Otherwise, you may need to invest more time until you get your controllers working correctly and get them verified. We structure the labs and assignments in a way that carefully build things up layer by layer so that you will learn about cyber-physical systems in a well-structured way. You will learn about one layer of CPS challenges at a time and we will proceed to the next challenges once we have mastered the previous ones.

KeYmaera Usage

KeYmaera Documentation
Starring KeYmaera on YouTube Channel

• Tutorial: Install KeYmaera
• Tutorial: Open KeYmaera Using Java Web Start
• Tutorial: Find a Counterexample
• Tutorial: Loop Invariants with KeYmaera
• Tutorial: Simple Train Control
• Tutorial: Discover Constraints Using KeYmaera
• Tutorial: Differential Cuts, Invariants, and Weakening
• Tutorial: Abbreviate Rule
• Tutorial: Modeling Discrete Steering
• Tutorial: Differential Auxiliaries / Differential Ghosts

Further Reading

This course will make heavy use of differential equations, logic and theorem proving. While each of those topics will be discussed in this course, you are expected to be able to get up to speed quickly. Depending on your prior background and how well you remember this material from other courses, we recommend that you look at some of the following resources before the semester starts. This will make it easier for you to get going in cyber-physical systems. You may also find these resources helpful for extra reading throughout the semester.

You should feel very comfortable with the elementary background material, e.g., what a differential equation is, before the course begins. We also include advanced materials for interested students.

We will also add further reading material as the course progresses.

1. André Platzer.
   Logical Analysis of Hybrid Systems:
      Proving Theorems for Complex Dynamics.
   Springer, Heidelberg, 2010. 426 pages. ISBN 978-3-642-14508-7.
   [bib | ⧉ | doi | book | web | errata | abstract]
   
   

1. [e-book in CMU Library]

Ordinary Differential Equations

• Course notes from 21-122 Integration, Differential Equations, and Approximation
• André Platzer. Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, 2010.
  Appendix B
• Nykamp DQ. Ordinary differential equation examples. From Math Insight.
• Nykamp DQ. An introduction to ordinary differential equations. From Math Insight.
• Wolfgang Walter. Ordinary Differential Equations. Springer, 1998. ISBN 978-0387984599
• Jörn Loviscach and Miriam Swords Kalk. Differential equations in action.
• Khan Academy. First order differential equations. (very basic, image quality issues)

First-Order Logic

• Interactive Tutorial of the Sequent Calculus
• Samuel R. Buss. An Introduction to Proof Theory in Handbook of Proof Theory. Elsevier, 1998. pp 1-78.
• André Platzer. Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, 2010.
  Appendix A (advanced)
• Mordechai Ben-Ari. Mathematical Logic for Computer Science. Springer, 2012.
  Chapters 1, 2, 3.2, 7, 8.1 (focus is on tableaux calculus instead of sequent calculus).