Overview

This course will provide different techniques on the verification of autonomous systems against stability, regular, or omega-regular properties. Such techniques include Lyapunov theories, reachability analysis, barrier certificates, and model checking. Finally, it will introduce several techniques on designing controllers enforcing properties of interest over the original autonomous systems. This course can be taken for academic credit as part of CU Boulder’s Masters of Science in Computer Science (MS-CS) degrees offered on the Coursera platform. This fully accredited graduate degree offer targeted courses, short 8-week sessions, and pay-as-you-go tuition. Admission is based on performance in three preliminary courses, not academic history. CU degrees on Coursera are ideal for recent graduates or working professionals. Learn more: MS in Computer Science: https://coursera.org/degrees/ms-computer-science-boulder

Syllabus

Course Introduction

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.

Verification of Finite Systems

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.

Synthesis for 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.

Abstraction and Refinement

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 controllers can be modified or replaced to meet new specifications without altering the overall system behavior. The module also covers the computation of abstractions, demonstrating how we derive abstract models from complex systems to facilitate analysis and design. Additionally, we will discuss practical methods for abstracting different types of control systems, equipping us with the skills to apply theoretical concepts in real-world scenarios.