К содержимому
learnspaceYOUR NEXT CHAPTER
ПРОСТРАНСТВО ОБУЧЕНИЯ
ГлавнаяКаталог курсовМоё обучениеCoursera

Знания без границ

Учитесь у лучших университетов и компаний мира.

Открыть Coursera
Интеграция
Пространство университета
Моё пространствоСтраница курса
↵
ЯЛичный кабинетСтудент
© 2026 LearnSpaceКаждый день — возможность узнать больше.Помощь
Verification and Synthesis of Autonomous Systems · LearnSpace
Назад в каталог
courseraПрограммирование

Verification and Synthesis of Autonomous Systems

Курс от University of Colorado Boulder
Средний≈ 11.3 чАнглийский
О курсеНавыкиПрограммаПреподаватели

О курсе

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

Навыки, которые вы освоите

Computational LogicVerification And ValidationTheoretical Computer ScienceAlgorithmsFunctional SpecificationSystems AnalysisSystems Design

Программа курса

4 модулей · 58 учебных материалов

01Course Introduction13 материалов

Course Overview

Course Updates and Accessibility SupportЧтениеEarn Academic Credit for your Work!ЧтениеCourse SupportЧтениеAssessment ExpectationsЧтение

Учитесь у экспертов

Majid Zamani

Associate Professor

Verification and Synthesis of Autonomous Systems
В каталоге вашей программы

Инвестируйте в себя

Новые знания — в удобное для вас время.

Начать на Coursera

Обучение откроется на Coursera
в новой вкладке

Обучение на Coursera

≈ 11.3 ч

4 модулей

Язык: Английский

Субтитры: Арабский, Французский, Итальянский, Корейский, Немецкий, Индонезийский, Испанский, Японский

Часть программы вашего университета
AI Citation and AcknowledgementЧтение
Important PrerequisitesЧтение
Notice for Degree-Seeking LearnersЧтение
Logistics: Important information about the Course Assignments and ExamЧтение
Logistics: Lecture Slides, Textbook and ReadingsЧтение

Welcome

Meet Your Instructor!Видео

Introduction to the Specilization

Outline of SpecializationВидеоAriane Flight V88Чтение

Introduction to Course

Introduction to Course 3 - Verification and Synthesis Видео
02Verification of Finite Systems17 материалов

Overview of Module 2

Overview of Module 2Чтение

Verification of Regular Safety Properties

IntroductionВидеоProduct of System and NFAВидеоExample of Product of Simple System and NFAВидеоAn ExampleВидео

Verification of Omega-Regular Properties

IntroductionВидеоProduct of System and NBAВидеоω-Regular Model CheckingВидеоω-Regular Model Checking: ExampleВидеоChecking Regular Safety vs ω-Regular PropertiesВидеоPersistence Checking via Strongly Connected ComponentВидео

LTL Model Checking

IntroductionВидеоFrom LTL to NBAВидеоNBA for LTL Formulas: ExamplesВидео

Assignment

AI Policy QuizЗаданиеAssignment 1: LTL VerificationЗаданиеAssignment 2: Persistence CheckingЗадание
03Synthesis for Finite Systems15 материалов

Overview of Module 3

Overview of Module 3Чтение

Fixed Points

OverviewВидеоFixed PointsВидеоComputation of Fixed PointsВидео

Synthesis Algorithms: Safety and Reachability

The Pre MapВидеоSynthesis for Safety SpecificationsВидеоSynthesis for Safety Specifications: ExampleВидеоSynthesis for Reachability SpecificationsВидеоSynthesis for Reachability Specifications: ExampleВидео

Synthesis Algorithms: Persistence, Recurrence, and Beyound

Synthesis for Persistence SpecificationsВидеоSynthesis for Persistence Specifications: ExampleВидеоSynthesis for Recurrence SpecificationsВидеоMore SpecificationsВидео

Assignment

Assignment 3: Computation of Maximal Fixed PointЗаданиеAssignment 4: Solving a Recurrence SynthesisЗадание
04Abstraction and Refinement13 материалов

Overview of Module 4

Overview of Module 4Чтение

Feedback Refinement Relations

MotivationВидеоDefinition of Feedback Refinement RelationsВидеоExample: Feedback Refinement RelationВидео

Controller Refinement

Theorem: Feedback Refinement Relations and Behavioral InclusionВидеоCorollary: Feedback Refinement Relations and Behavioral InclusionВидео

Computation of Abstractions

Theorem: Computation of AbstractionsВидеоExample: Computation of AbstractionsВидеоAbstractions of Sample-and-Hold Linear Control SystemВидео

Tools for the Synthesis

Instructions for Installing SCOTSЧтениеSCOTS and OmegaThreads: Tools for the Synthesis of Controllers via Finite AbstractionsВидео

Assignment

Assignment 5: Feedback Refinement RelationЗаданиеAssignment 6: Construction of an AbstractionЗадание