آموزش تأیید و سنتز سیستم‌های خودمختار - آخرین آپدیت

معرفی دوره Course Introduction

• آشنایی با مدرس! Meet Your Instructor!

• سرفصل‌های تخصص Outline of Specialization

• معرفی دوره ۳: تأیید و سنتز Introduction to Course 3 - Verification and Synthesis

تأیید سیستم‌های متناهی Verification of Finite Systems

• مقدمه Introduction

• حاصل‌ضرب سیستم و NFA Product of System and NFA

• مثالی از حاصل‌ضرب سیستم ساده و NFA Example of Product of Simple System and NFA

• یک مثال کاربردی An Example

• مقدمه Introduction

• حاصل‌ضرب سیستم و NBA Product of System and NBA

• مدل‌بررسی امگا-منظم ω-Regular Model Checking

• مدل‌بررسی امگا-منظم: مثال ω-Regular Model Checking: Example

• بررسی ایمنی منظم در مقابل ویژگی‌های امگا-منظم Checking Regular Safety vs ω-Regular Properties

• بررسی پایداری از طریق مؤلفه‌های قویاً متصل Persistence Checking via Strongly Connected Component

• مقدمه Introduction

• از LTL به NBA From LTL to NBA

• NBA برای فرمول‌های LTL: مثال‌ها NBA for LTL Formulas: Examples

سنتز برای سیستم‌های متناهی Synthesis for Finite Systems

• مرور کلی Overview

• نقاط ثابت Fixed Points

• محاسبه نقاط ثابت Computation of Fixed Points

• نگاشت Pre-Map The Pre Map

• سنتز برای مشخصات ایمنی Synthesis for Safety Specifications

• سنتز برای مشخصات ایمنی: مثال Synthesis for Safety Specifications: Example

• سنتز برای مشخصات دسترسی Synthesis for Reachability Specifications

• سنتز برای مشخصات دسترسی: مثال Synthesis for Reachability Specifications: Example

• سنتز برای مشخصات پایداری Synthesis for Persistence Specifications

• سنتز برای مشخصات پایداری: مثال Synthesis for Persistence Specifications: Example

• سنتز برای مشخصات تکرار Synthesis for Recurrence Specifications

• سایر مشخصات More Specifications

انتزاع و پالایش Abstraction and Refinement

• انگیزه و ضرورت Motivation

• تعریف روابط پالایش بازخورد Definition of Feedback Refinement Relations

• مثال: رابطه پالایش بازخورد Example: Feedback Refinement Relation

• قضیه: روابط پالایش بازخورد و شمول رفتاری Theorem: Feedback Refinement Relations and Behavioral Inclusion

• نتیجه: روابط پالایش بازخورد و شمول رفتاری Corollary: Feedback Refinement Relations and Behavioral Inclusion

• قضیه: محاسبه انتزاعات Theorem: Computation of Abstractions

• مثال: محاسبه انتزاعات Example: Computation of Abstractions

• انتزاعات سیستم کنترل خطی نمونه‌بردار و نگهدار Abstractions of Sample-and-Hold Linear Control System

• ابزارهای SCOTS و OmegaThreads: ابزارهایی برای سنتز کنترل‌کننده‌ها از طریق انتزاعات متناهی SCOTS and OmegaThreads: Tools for the Synthesis of Controllers via Finite Abstractions