منطق زمانی و وجهی در محاسبات

منطق‌های زمانی و وجهی، منطق کلاسیک را با عملگرهایی برای زمان و امکان گسترش می‌دهند و زبان‌های دقیقی را برای مشخص کردن اینکه یک برنامه یا سیستم واکنشی چگونه باید در طول کل اجرای خود رفتار کند، ارائه می‌دهند.

Definition

منطق زمانی، منطق گزاره‌ای یا مرتبه اول را با عملگرهایی که توصیف می‌کنند چه زمانی ویژگی‌ها در طول یک محاسبه برقرار هستند، مانند همیشه، نهایتاً، و تا زمانی که، تقویت می‌کند؛ منطق وجهی این را با عملگرهایی برای ضرورت و امکان بر روی ساختاری از حالت‌ها و انتقال‌ها تعمیم می‌دهد.

Scope

این موضوع شامل منطق‌های زمانی خطی و شاخه‌ای مانند LTL و CTL، منطق‌های وجهی از جمله منطق دینامیک و حساب مو-وجهی (modal mu-calculus)، بیان ویژگی‌های ایمنی و زنده‌مانی، و مسائل الگوریتمی بررسی مدل (model checking) و ارضاپذیری است که این منطق‌ها را در تأیید خودکار (automated verification) محوری می‌سازد.

Core questions

• چگونه یک منطق می‌تواند بیان کند که یک اتفاق خوب نهایتاً رخ می‌دهد یا یک اتفاق بد هرگز رخ نمی‌دهد؟
• تفاوت بین استدلال در مورد یک اجرای واحد و در مورد تمام آینده‌های ممکن چیست؟
• چگونه بررسی اینکه یک سیستم یک ویژگی زمانی را برآورده می‌کند، الگوریتمی می‌شود؟
• کدام منطق‌های زمانی بین قدرت بیان و تأیید کارآمد تعادل برقرار می‌کنند؟

Key theories

منطق زمانی برای مشخصه‌سازی برنامه

پنوئلی نشان داد که منطق زمانی صحت برنامه‌های واکنشی و همزمان را با بیان ویژگی‌ها بر روی اجراهای آنها، و ارائه یک زبان یکنواخت برای الزامات ایمنی و زنده‌مانی، به تصویر می‌کشد.

بررسی مدل منطق شاخه‌ای

کلارک و امرسون منطق درخت محاسبات و الگوریتمی را برای تأیید خودکار آن در برابر یک مدل حالت محدود معرفی کردند و زمینه بررسی مدل را بنیان نهادند.

Clinical relevance

منطق‌های زمانی، زبان‌های مشخصه‌سازی بررسی‌کننده‌های مدل (model checkers) هستند که به طور معمول برای تأیید طراحی‌های سخت‌افزاری، پروتکل‌های ارتباطی، و نرم‌افزارهای همزمان استفاده می‌شوند و بن‌بست‌ها و نقض‌های ایمنی و زنده‌مانی را قبل از استقرار شناسایی می‌کنند؛ این فناوری برای بنیان‌گذاران خود جایزه تورینگ را به ارمغان آورد و در طراحی تراشه استاندارد است.

History

پنوئلی (Pnueli) منطق زمانی را برای استدلال در مورد برنامه‌ها در سال ۱۹۷۷ پیشنهاد کرد، و کلارک (Clarke) و امرسون (Emerson)، به همراه کویل (Queille) و سیفاکیس (Sifakis) به طور مستقل، بررسی مدل را در حدود سال ۱۹۸۱ توسعه دادند. این رویکرد از طریق روش‌های نمادین در اوایل دهه ۱۹۹۰ به سیستم‌های صنعتی مقیاس‌پذیر شد، و سازندگان آن جایزه تورینگ را برای این تکنیک دریافت کردند.

Key figures

• Amir Pnueli
• Edmund Clarke
• E. Allen Emerson
• Joseph Sifakis

Seminal works

• clarkeEmerson1981
• huthRyan2004

Frequently asked questions

تفاوت بین منطق زمانی خطی و شاخه‌ای چیست؟

منطق‌های زمانی خطی مانند LTL ویژگی‌های یک مسیر اجرای واحد، احتمالاً بی‌نهایت، را توصیف می‌کنند. منطق‌های زمانی شاخه‌ای مانند CTL بر روی درخت تمام آینده‌های ممکن از هر حالت کمیت‌سنجی می‌کنند و به فرد اجازه می‌دهند بگوید که در طول برخی مسیرها یا در طول تمام مسیرها یک ویژگی برقرار است. آنها قدرت‌های بیانی و الگوریتم‌های تأیید متفاوتی دارند.

بررسی مدل چگونه از این منطق‌ها استفاده می‌کند؟

یک سیستم به عنوان یک مدل حالت محدود و یک ویژگی مطلوب به عنوان یک فرمول منطق زمانی نمایش داده می‌شود. یک بررسی‌کننده مدل به طور جامع حالت‌ها را بررسی می‌کند تا مشخص کند آیا فرمول برقرار است یا خیر، و اگر ناموفق باشد یک مسیر مثال نقض تولید می‌کند، که تأیید را هم خودکار و هم تشخیصی می‌سازد.