منطق موقت خطی

منطق زمانی خطی (Linear temporal logic) در منطق، منطق زمانی خطی یا منطق زمانی خطی (در انگلیسی linear temporal logic or linear-time temporal logic(یک منطق زمانی موجهاتی است با توجیهاتی به زمان.

در منطق زمانی خطی یک مسئله می‌تواند بررسی فرموله کردن آینده یک مسیر می‌باشد مثلاً این که یک شرط در نهایت درست خواهد شد یا …

منطق زمانی خطی خود یک قسمتی از منطق پیچیده‌تر CTL* می‌باشد که اجازه شاخه شاخه شدن حالات زمان و سنجه‌ها را می‌دهد. همچنین منطق زمانی خطی را منطق زمانی گزاره ای (به انگلیسی propositional temporal logic , PTL) نیز می‌نامند.

منطق زمانی یک فرمالیسم مناسب برای مشخص کردن و تصدیق خاصیت‌های یک سیستم واکنشی است.

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

یک مدل منطق زمانی خطی یک دنباله نامتناهی از حالاتی است که هر نقطه در هر لحظه از زمان دارای پیآمد (successor) خاصی است.

شروع و انگیزه

منطق زمانی خطی ابتدا برای صحت یابی رسمی برنامه‌های کامپیوتری در سال ۱۹۷۷ توسط امیرپنئولی در مقاله ای به نام "منطق زمانی برنامه‌ها (به انگلیسی: The Temporal Logic Of Programs) پیشنهاد شد. او در خلاصه این مقاله می‌نویسد:

یک روش جامع و یکپارچه برای تصدیق (verification) پیشنهاد شده که برای برنامه‌های موازی و پی درپی قابل پیاده‌سازی است. روش اصلی اثبات پیشنهادی، استدلال زمانی است با این پیش فرض که اتفاقات دارای وابستگی زمانی می‌باشند.

دو سیستم رسمی (formal systems) برای برآورده کردن اصول مورد نیاز استدلال زمانی معرفی شده‌است.

یکی از فرم‌ها، فرمالیسم روش اثبات متناوب (method of intermittent assertions) است و دیگری انطباق با سیستم محکم (adaptation of the tense logic system K_b) که کاملاً برای استدلال در مورد رویدادهای همزمان مناسب است.

نحو

منطق زمانی زمانی یک دسته متناهی از متغیرهای گزاره (propositional variables)، عملگرهای منطقی ¬ و ∨، و در کنار ارتباط دهندگان معمول، فرمول‌های زمانی می‌توانند با عملگرهای زمانی تولید شوند.

عملگرهای زمانی آینده
[]p	از حالا به بعد p
<>p	بالاخره p
p تا q	q یه مقدار زمان به طول خواهد انجامید، و p حداقل تا ابتدای q خواهد بود
p منتظر q	یا p همیشه خواهد بود، یا p تا q
()p	p دفعه بعد اتفاق می‌افتد
Past Temporal Operators
[-]p	تا حالا p
<->p	یک باریp
p از وقتی q	q زمانی در گذشته منتظر مانده، و p حداقل تا ابتدای q خواهد بود
pبلافاصله q	یا p از وقتیq, یا [-]p
(-)p	p در زمان قبلی اتفاق افتاده (و زمان فعلی ۰ نیست)
(~)p	p در زمان قبلی اتفاق افتاده یا زمان فعلی ۰ است (زمانی قبل از این وجود نداشته‌است)

معنا

یک فرمول منطق زمانی خطی می‌تواند با استفاده از یک رشته از حقیقت سنج‌هایی که زیر مجوعه از متغیرهای گزاره هستنند اثبات شوند.

یک فرمول منطق زمانی p تصدیق پذیر است اگر که یک دنباله از حالات S باشد به صورتی S,0 |= p. این زمانی درست خواهد بود که نفی آن غیرقابل تصدیق باشد. یک فرمول منطق گزاره ای زمانی یک فرمول زمانی هست اگر همه اتم‌های آن متغیرهای گزاره ای باشند. (یک فرمول زمانی گزاره ای در نتیجه شامل مقدار سنج‌ها و مسندهای مرکب نخواهد بود)

اگر w = a₀,a₁,a₂,... را یک ω-کلمه در نظر بگیریم. w(i) = a_i. wⁱ =... , a_i,a_i+1

به صورت رسمی، رابطه تصدیق پذیری |= بین یک کلمه و یک فرمول منطق زمانی زمانی به صورت زیر تعریف می‌شود:

w |= p اگر p ∈ w(0)

w |= ¬ψ اگر w |= ψ

w |= φ ∨ ψ اگر w |= φ یا w |= ψ

w |= X ψ اگر w¹ |= ψ (در زمان گام بعدی ψ باید صحیح باشد)

w |= φ U ψ اگر وجود داشته باشد i ≥ ۰ به صورتی که wⁱ |= ψ، برای همه 0<i>k و φ |= w^k (φ باید صحیح بماند تا زمانی که ψ صحیح بشود)