سیستم‌های واکنشی reactive)‎)، سیستم‌هایی هستند که رفتار آن‌ها به گونه‌ای پیوسته و تنگاتنگ در ارتباط با محیط (environment) تعریف می‌شود. اینگونه سیستم‌ها معمولاً در کاربردهای حساس ‎ (critical applications) به کار می‌آیند. نمونه‌هایی از این کاربردها عبارتند از: سیستم‌های عامل ‎ (operating systems)، شبکه‌های کامپیوتری سریع ‎ (high-speed computer networks)، سیستم‌های همراه بی سیم ‎ (wireless mobile systems)، سیستم‌های سایبری-فیزیکی (cyber-physical systems)، اینترنت اشیاء (Internet of things)، هوانوردی (avionics) ‎، کنترل فرایندهای صنعتی (industrial process control) ‎، نیروگاه‌های اتمی (nuclear plants) و غیره. از خواص مهم این سیستم‌ها، همروندی (concurrency)، جنبه‌های بی‌درنگ (real-time)، و کارایی (performance)، اتکاپذیری (dependability) و امنیت (security) بالا‎ است. سه خاصیت اخیر معمولاً مستلزم درستی رفتار اینگونه سیستم‌ها در شرایط مختلف است. از سویی دیگر، تعیین چنین درستی رفتاری به دلیل جنبه‌های همروندی و بی‌درنگی معمولاً بسیار پیچیده است. این درس درباره مفاهیم و روش‌های رسمی (formal methods)ای است که برای توصیف مشخصات (specification) ‎و اعتبارسنجی (validation) سیستم‌های واکنشی به کار می‌آیند.

1. درستی‌یابی سیستم (۱ جلسه)
   • وارسی الگو، مشخصات وارسی الگو، نقاط قوت و ضعف.
2. مدل‌های همروندی (۳ جلسه)
   • سیستم‌های گذار، مدل‌های متنی مبتنی بر متغیرهای مشترک، مسائل معنایی، روابط هم‌ارزی بین دستورات، مدل‌های متنی مبتنی بر ارسال پیام، مدل ‎CSP‎، مدل ‎CCS‎، شبکه‌های پتری، هم‌ارزی رفتاری، توازی همگام، ‎NanoPromela‎، توازی همگام، مساله انفجار فضای حالت، تبعات ملزومات عدالت، عدالت ضعیف، عدالت قوی، دستورات هماهنگ‌سازی، دستورات ارتباطی، جنبه‌های معنایی عدالت، عدالت در شبکه‌های پتری، عدالت در سیستم‌های گذار.
3. خواص زمان خطی (۴ جلسه)
   • بن بست، رفتار زمان خطی، خواص و تغییر ناپذیرهای ایمنی، خواص زندگی، انصاف.
4. خواص منظم (۴ جلسه)
   • خودکارها در روی کلمات متناهی، وارسی الگوی خواص ایمنی منظم، خودکارها در روی کلمات نامتناهی، وارسی الگوی خواص ‎ω‎ منظم.
5. منطق زمانی خطی (۶ جلسه)
   • نحو و معنا، هم‌ارزی فورمول‌های ‎LTL‎، وارسی الگوی مبتنی بر خودکارهای ‎LTL.
6. منطق درخت محاسباتی (۶ جلسه)
   • نحو و معنا، قابلیت توصیف ‎CTL‎ نسبت به ‎LTL‎، وارسی الگوی ‎CTL‎، انصاف در ‎CTL‎، وارسی الگوی نمادین ‎CTL‎، ‎CTL*‎.
7. هم‌ارزی و تجرید (۳ جلسه)
   • شبیه‌سازی دوسویه، شبیه‌سازی دوسویه و هم‌ارزی ‎CTL*‎، الگوریتم‌های پیمانه سازی شبیه‌سازی دو سویه، روابط شبیه‌سازی، شبیه‌سازی دوسویه و هم ارزی CTL* ‎∀
8. کاهش ترتیب جزئی (۱ جلسه)
   • استقلال اعمال، رهیافت مجموعه‌ی زمان خطی ‎Ample‎، رهیافت مجموعه‌ی زمان شاخه‌ای ‎Ample‎.
9. خودکارهای زمانی (۱ جلسه)
   • معنا، منطق درخت محاسباتی زمانی، وارسی الگوی ‎TCTL‎.
10. سیستم‌های احتمالی (۱ جلسه)
    • زنجیره‌های مارکوف، منطق درخت محاسباتی احتمالی، خواص زمان خطی، ‎PCTL*‎ و شبیه‌سازی دوسویه احتمالی، زنجیره‌های مارکوف و هزینه‌ها، فرایند‌های تصمیم‌گیری مارکوف.

• آزمون: آزمون‌های میان‌نیمسال و پایان‌نیمسال (۶۵ درصد نمره)
• ارائه: گردآوری یک یا دو مقاله تحقیقی و ارائه شفاهی آنها (۳۵ درصد نمره)