| Category | Difficulty |
|---|---|
| HW | 5 |
| Labs | 6 |
| Exams | 3 |
| Project | 7 |
Have you ever wondered how people make sure airplanes never hit each other? Do you want to know the technology that goes into guaranteeing that autonomous vehicles are safe? Cyberphysical systems, which applies logic to these physical applications, is just the topic for that. This class contains lots of theory in terms of logic, but also has many fascinating applications, which makes it a good course for both the theory and less-theory inclined people.
The content taught in this class can be quite difficult, and is easier picked up if you already have a background in logic and some basic physics. However, you can still take this class with no prerequisites, you'll just have to do a little more work by yourself. Grade-wise, the class is not that hard to get a good grade, but because the content can be very difficult, you might have to work a bit harder on understanding the concepts.
Homework, or theory assignments are usually straightforward problems relating to the lecture content. It will benefit you a lot if you learn how to LaTeX your homework, especially your proofs. You will likely have to perform logic proofs, which require the busproofs package.
Labs in this class are for you to use KeYmaera X, the language implemented for CPS, to be used for writing CPS proofs. You will usually have to
- Construct a statement that satisfies the problem requirements
- Prove the statement, using the KeYmaera X system
- Submit the proof you found
Using their software to prove statements can be difficult at first, but as you learn more rules, you will become more familiar with the system. At first, it will seem like you're just clicking random buttons and things will just eventually simplify and work out, but later on, you will have to work on more difficult proofs that require you to take well-tuned steps to prove statements efficiently.
Despite the difficulty of the content in this class, the exams are surprisingly easy. They are often short, and involve straightforward short and answer and proof problems. You are also allowed a cheatsheet, where you can just copy down all the proof rules.
The only caveat maybe is that you should make sure your proofs are complete and not missing any justifications. Even then, you only lose a few points.
You should definitely make sure you pick up all the points you can on the exam.
There is a final project in this class, and a competition exhibition at the end of the semester. The final project is very open-ended, and you can pretty much do whatever you want, as long as it involves CPS. The format for most projects is something like
- Find a problem with some sort of safety involved
- Build a model for the problem using CPS constructs
- Prove the statement
- Discuss extensions to the proof
Usually stronger projects choose more interesting applications, or extend beyond the basic proofs taught in the class. For example, you can improve the KeYmaera X program, you can implement a new logic system on top of dL, you can try to apply dL to machine learning... You can look at past projects on the website to get an idea of what previous winners have done.
- Course website Past iterations of this course are also posted here
- Logical Foundations of Cyber-Physical Systems: Textbook written by Professor André Platzer himself