Teaching at HKUST(GZ)

ROAS 5110 Formal Verification and Control of Dynamical Systems (graduate level)

Formal methods originate from theoretical computer science and have been seamlessly integrated with dynamical systems. At its core, formal methods involve formulating specifications to form proof obligations, verifying that the systems indeed meet their specifications via algorithmic proof search, and designing systems to meet those obligations. This course bridges fundamental gaps between formal methods and control theory. It introduces fundamental theories and techniques of formal methods that apply broadly to various dynamical systems, such as robots, autonomous systems and cyber physical systems. Particularly, the following topics will be covered: symbolic system modeling, regular and omega-regular properties, linear temporal logic, model checking, system simulation and abstraction, game theoretic control synthesis and cutting-edge engineering applications.

ROAS 5600 Introduction to Discrete Event Systems (graduate level)

This course aims to provide an introduction to the fundamental knowledge of physical systems modeled with discrete state space and event driven transitions. Discrete Event Systems (DES) arise in the modeling of many engineering domains, such as automated manufacturing systems, communication networks, software systems, process control systems, and transportation systems. This course will introduce a unified modeling framework and emphasize the analysis and control of DES. Basics of automata and language theory are presented first as mathematical preliminaries. Then comes a detailed treatment of state estimation, diagnosis, security and supervisory control theory of DES based on automata model. Topics of other DES models like Petri nets, timed and hybrid automata are also covered towards the end of the course.