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

مقدمه دوره Course Introduction

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

• طرح کلی تخصص Outline of Specialization

• مقدمه‌ای بر دوره دوم – مشخصات نیازمندی Introduction to Course 2 – Requirement Specification

مشخصات سطح پایین Low-Level Specifications

• پایداری Stability

• پایداری: مثال‌ها Stability: Examples

• قضیه پایداری لیاپانوف Lyapunov’s stability theorem

• قضیه پایداری لیاپانوف: مثال‌ها Lyapunov’s stability theorem: Examples

• پایداری سیستم‌های خطی Stability of linear systems

• پایداری سیستم‌های خطی: مثال Stability of linear systems: Example

• توابع لیاپانوف برای سیستم‌های خطی Lyapunov functions for linear systems

• توابع لیاپانوف برای سیستم‌های خطی: مثال Lyapunov functions for linear systems: Example

• پایداری ورودی به حالت (ISS) Input-to-state stability (ISS)

• ISS برای سیستم‌های خطی ISS for linear systems

• قضیه لیاپانوف برای ISS Lyapunov theorem for ISS

• قضیه لیاپانوف برای ISS: مثال‌ها Lyapunov theorem for ISS: Examples

• پایداری اتصالات سری Stability of series interconnections

• پایداری اتصالات فیدبک Stability of feedback interconnections

مشخصات سطح بالا: دسترسی‌پذیری، ایمنی، ویژگی‌های منظم و منظم اُمگا High-Level Specifications: Reachability, Safety, Regular and ω-Regular Properties

• محاسبه مجموعه‌های قابل دسترس از طریق زونوتوپ‌ها Computation of reachable sets via zonotopes

• محاسبه مجموعه‌های قابل دسترس برای سیستم‌های ISS Computation of reachable sets for ISS systems

• گواهی ایمنی Safety certification

• مفاهیم پایه زبان‌ها Basic concepts of languages

• عبارات منظم Regular expressions

• عبارات منظم اُمگا ω-regular expressions

• عبارات منظم اُمگا: مثال ω-regular expressions: Example

اتوماتای متناهی غیرقطعی و اتوماتای بوچی (NFA و NBA) Nondeterministic Finite and Büchi Automata (NFA and NBA)

• اتوماتای متناهی غیرقطعی (NFA) Nondeterministic finite automaton (NFA)

• زبان پذیرفته شده توسط یک NFA Accepted Language of an NFA

• حاصل‌ضرب همگام NFAها Synchronous Product of NFAs

• NFA تشخیص‌دهنده زبان‌های منظم NFA recognizing regular languages

• اتوماتای متناهی قطعی (DFA) Deterministic Finite Automaton (DFA)

• تبدیل NFA به DFA: مثال NFA to DFA: Example

• ویژگی‌های زمان خطی Linear-time properties

• اتوماتای بوچی غیرقطعی (NBA) Nondeterministic Büchi automata (NBA)

• NBA برای ویژگی‌های زمان خطی NBA for linear time properties

• از NBA به عبارات منظم اُمگا From NBA to ω-regular expressions

• از عبارات منظم اُمگا به NBA From ω-regular expressions to NBA

• از عبارات منظم اُمگا به NBA: مثال From ω-regular expressions to NBA: Example

• ویژگی‌های خطی ایمنی و هم‌ایمنی Safety and co-safety linear properties

فرمول‌های منطق زمانی خطی Linear Temporal Logic Formulae

• منطق زمانی خطی (سینتکس) Linear Temporal Logic (Syntax)

• منطق زمانی خطی (سمنتیک) Linear Temporal Logic (Semantics)

• معادل بودن فرمول‌های LTL Equivalence of LTL Formulas