CSCA 5854: Verification and Synthesis of Autonomous Systems
Preview this courseÌýin the non-credit experience today!Ìý
Start working toward program admission and requirements right away.ÌýWork you complete in the non-credit experience will transfer to the for-credit experience when you upgrade and pay tuition. See How It Works for details.
Course Type: Elective
Specialization: Foundations of Autonomous Systems
Instructor:ÌýDr. Majid Zamani, Associate Professor
Prior knowledge needed:
This third course in the specialization focuses on modeling requirements. It is highly recommended that students take the first two courses that focus on the core structure in any autonomous system before attempting this course. We anticipate that students possess a grasp of fundamental mathematical concepts equivalent to those covered in the first year of studies for STEM majors at a US college. Additionally, a familiarity with basic differential equations and linear algebra is expected. This encompasses key principles, including:Ìý
- Sets and Functions: Proficiency in understanding the properties of sets, along with a clear comprehension of function definitions and their associated properties.
- Eigenvalues and Eigenvectors: A basic knowledge of eigenvalues and eigenvectors of matrices, coupled with an ability to perform matrix-vector multiplication.
- Systems of First Order Linear Differential Equations:ÌýÌýA basic knowledgeÌýin solving and analyzing systems of first-order linear differential equations.
Learning Outcomes
- Master the use of linear temporal logic and automata to define system requirements.
- Convert between regular expressions and non-deterministic finite automata (NFAs) for effective system requirements modeling.
- Formulate essential system properties, such as safety and reachability.
- Employ Linear Matrix Inequalities (LMIs) and Lyapunov functions to verify stability and robustness.
- Calculate reachable sets and generate safety certificates using barrier functions.
- Translate between omega-regular specifications and non-deterministic Büchi automata (NBAs).
- Develop NBAs based on linear temporal logic formulas
Course Grading Policy
| Assignment | Percentage of Grade |
|---|---|
| 6 Assignments | 60% (10% each) |
| 3 Quizzes | 20% (6.7% each) |
| Final Exam | 20% |
| Total | 100% |
Course Content
Welcome to the beginning of our exploration into formal verification and synthesis within the model-based design framework. In this introductory module, we will guide you through the key processes of specification, design, verification, and refinement of systems. We will delve into the vital role of formal methods in guaranteeing the correctness of systems. Through captivating examples, we will demonstrate the importance of formal verification, especially in safety-critical and life-critical applications. This module lays the foundation for the more advanced topics we will address throughout the course.
In this module, we focus on the verification of finite systems, particularly emphasizing regular safety properties and ω-regular properties (including those expressed as linear temporal logic formulae). We will explore a variety of verification techniques and delve into the theoretical underpinnings essential for understanding how finite systems are verified. Through detailed examples and clear, comprehensive explanations, we aim to provide a deep understanding of how these properties are verified in the context of finite systems.
In this module, we explore the synthesis of controllers for finite systems, focusing on enforcing certain linear temporal logic (LTL) formulas, including safety, reachability, persistence, and recurrence. We aim to understand how controllers can be designed to render specific LTL formulas for closed-loop systems. The module provides essential theoretical frameworks and practical algorithms necessary for synthesizing such controllers, with an emphasis on the roles of fixed-point operators and algorithms in the computation processes. Additionally, we will discuss various synthesis techniques that depend on the properties of the system and the involved LTL formulas.
In this module, we will explore the concepts of abstraction and refinement within the context of control systems. We will delve into feedback refinement relations to understand how these allow for the refinement of controllers between two related systems, particularly from finite to infinite systems. The module also covers the computation of finite abstractions, demonstrating how we derive finite abstractions of continuous-space complex control systems to facilitate their analysis and design.
Duration: 2 hours
Final Exam Format: Timed in-course exam, not proctored
This module contains materials for the final project. If you've upgraded to the for-credit version of this course, please make sure you review the additional for-credit materials in the Introductory module and anywhere else they may be found.
This is a "take home" final exam. You have 12 hours to solve them. Ìý
There is only ONE attempt (submission) allowed for the final exam.
The final is identical to our regular assignment: the problems are multiple-choice question that require you to use the concepts you have learned so far to solve problems. Ìý
We expect that the problems will cumulatively require 2 - 3 hours of work to finish and the remaining time will provide you the necessary flexibility.
Notes
- Cross-listed Courses: CoursesÌýthat are offered under two or more programs. Considered equivalent when evaluating progress toward degree requirements. You may not earn credit for more than one version of a cross-listed course.
- Page Updates: This page is periodically updated. Course information on the Coursera platform supersedes the information on this page. Click theÌýView on CourseraÌýbuttonÌýabove for the most up-to-date information.