Course Code: CS591
Course Name: Formal Modelling and Analysis of Cyber-Physical Systems
Prerequisites: Discrete Mathematics; Formal Languages and Automata Theory; or equivalent
Syllabus: Modelling Discrete Systems: Finite state machines, automata, discrete-time, synchronous and asynchronous models of computation, invariants, safety and liveness requirements, deductive verification with theorem provers, satisfiability modulo theories;

Temporal Logic and Model Checking: Kripke structures, branching time and linear-time temporal logics, model checking;

Dynamical and hybrid system models: Continuous-time models, linear systems, feedback-control, stability, safety and reachability, hybrid dynamical models, timed automata, linear hybrid automata;

Analysis techniques: Safety, reachability and stability verification, barrier certificates and Lyapunov functions, compositional techniques, abstraction and refinement, simulation and bisimulation;

Advanced Topics: Verification of autonomous systems and systems with machine learning components;

Case Studies: Examples of models from automotive, avionics, robotics, medical devices, etc., and their verification.
References: 1. Rajeev Alur, Principles of Cyber-Physical Systems, MIT Press, 2015.
2. Sayan Mitra, Verifying Cyber-Physical systems, MIT Press, 2021.