منطق زمانی

در منطق، منطق زمانی هر سیستمی از قواعد و نمادها برای بازنمایی و استدلال دربارهٔ گزاره‌هایی است که از نظر زمانی واجد شرایط هستند (مثلاً «من همیشه گرسنه هستم»، «در نهایت گرسنه خواهم بود» یا «گرسنه خواهم بود». تا زمانی که چیزی بخورم"). گاهی اوقات برای اشاره به منطق زمان، یک سیستم منطق زمانی مبتنی بر منطق مدال که توسط آرتور پریور در اواخر دهه ۱۹۵۰ معرفی شد، با پژوهش‌های مهم هانس کمپ نیز استفاده می‌شود. این منطق بیشتر توسط دانشمندان رایانه، به ویژه امیر پنولی، و منطق دانان توسعه یافته‌است.

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

انگیزه

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

منطق زمانی همیشه این توانایی را دارد که دربارهٔ یک جدول زمانی استدلال کند. به اصطلاح خطی «منطق‌های زمانی» به این نوع استدلال محدود می‌شود. با این حال، منطق‌های انشعاب می‌تواند در مورد چندین جدول زمانی استدلال کند. این امر محیطی را پیش‌فرض می‌گیرد که ممکن است غیرقابل پیش‌بینی عمل کند. برای ادامه مثال، در یک منطق منشعب ممکن است بگوییم که «این امکان وجود دارد که برای همیشه گرسنه بمانم» و «این احتمال وجود دارد که در نهایت دیگر گرسنه نباشم». اگر ندانیم که آیا من هرگز سیر خواهم شد یا نه، این گفته‌ها می‌توانند هر دو درست باشند.

تاریخ

اگرچه منطق ارسطو تقریباً به‌طور کامل به نظریه قیاس مقوله‌ای مربوط می‌شود، در آثار او عباراتی وجود دارد که اکنون به عنوان پیش‌بینی منطق زمانی تلقی می‌شوند و ممکن است دلالت بر شکل اولیه و تا حدی توسعه‌یافته‌ای از منطق باینری موقتی مرتبه اول داشته باشند. . ارسطو به ویژه به مسئله احتمالات آینده توجه داشت، جایی که او نمی‌توانست بپذیرد که اصل دو ظرفیتی در مورد گزاره‌های مربوط به رویدادهای آینده اعمال می‌شود، یعنی در حال حاضر می‌توانیم دربارهٔ درست یا نادرست بودن گزاره‌ای در مورد رویداد آینده تصمیم بگیریم، مانند «در آنجا فردا یک نبرد دریایی خواهد بود."

چارلز سندرز پیرس در قرن نوزدهم خاطرنشان کرد: برای هزاران سال توسعه کمی وجود داشت: الگو:گفتاورد تزیینی به‌طور شگفت‌انگیزی برای پیرس، اولین سیستم منطق زمانی، تا آنجا که می‌دانیم، در نیمه اول قرن بیستم ساخته شد. اگرچه آرتور پریور به‌طور گسترده‌ای به عنوان بنیانگذار منطق زمانی شناخته می‌شود، اولین رسمی سازی چنین منطقی در سال ۱۹۴۷ توسط منطق دان لهستانی، جرزی لوش ارائه شد. او در کار خود Podstawy Analizy Metodologicznej Kanonów Milla (مبانی تحلیل روش شناختی روش‌های میل) رسمی سازی قوانین میل را ارائه کرد. در رویکرد Łoś تأکید بر عامل زمان قرار گرفت؛ بنابراین، برای رسیدن به هدف خود، باید منطقی را ایجاد می‌کرد که می‌توانست ابزاری برای رسمی کردن کارکردهای زمانی فراهم کند. منطق را می‌توان محصول فرعی هدف اصلی لوش دانست، اگرچه این اولین منطق موضعی بود که بعداً به عنوان چارچوبی برای اختراعات لو در منطق معرفتی استفاده شد. خود منطق دارای نحو بسیار متفاوتی با منطق زمان قبلی است که از عملگرهای مدال استفاده می‌کند. زبان منطق Łoś بیشتر از یک عملگر تحقق خاص برای منطق موقعیتی استفاده می‌کند که عبارت را با زمینه خاصی که در آن ارزش حقیقت در نظر گرفته می‌شود پیوند می‌دهد. در کار لو، این زمینه در نظر گرفته شده فقط زمانی بود، بنابراین عبارات با لحظات یا فواصل زمانی خاصی پیوند خوردند.

در سال‌های بعد، تحقیق دربارهٔ منطق زمانی توسط آرتور پریور آغاز شد. او به مفاهیم فلسفی اراده آزاد و جبر توجه داشت. به گفته همسرش، او برای اولین بار در سال ۱۹۵۳ به رسمیت بخشیدن به منطق زمانی فکر کرد. نتایج تحقیقات او برای اولین بار در کنفرانس ولینگتون در سال 1954 شد. سیستمی که پیش از این ارائه شد، از نظر نحوی مشابه منطق Łoś بود، اگرچه تا سال ۱۹۵۵ او به صراحت به کار Łoś در آخرین بخش از ضمیمه ۱ در منطق رسمی قبلی اشاره کرد.

پیش از این در سال‌های ۱۹۵۵–۱۹۵۶ در دانشگاه آکسفورد دربارهٔ این موضوع سخنرانی کرد و در سال ۱۹۵۷ کتابی به نام «زمان و روش» منتشر کرد که در آن یک منطق مدال گزاره‌ای را با دو رابط زمانی (عملگرهای مدال)، F و P که مربوط به «گاهی در آینده» و «گاهی در گذشته». در این کار اولیه، پریور زمان را خطی می‌دانست. با این حال، در سال ۱۹۵۸، او نامه ای از سائول کریپکه دریافت کرد، که به این موضوع اشاره کرد که این فرض ممکن است بیجا باشد. پریور در تحولی که مشابه آن را در علوم کامپیوتر پیش‌بینی می‌کرد، این موضوع را تحت نظر گرفت و دو نظریه دربارهٔ زمان انشعاب ایجاد کرد که آنها را «اکهامیست» و «پیرسین» نامید.الگو:نیازمند شفاف‌سازی بین سالهای ۱۹۵۸ و ۱۹۶۵ قبل از آن نیز با چارلز لئونارد هامبلین مکاتبه داشت و تعدادی از تحولات اولیه در این زمینه را می‌توان در این مکاتبات ردیابی کرد، به عنوان مثال مفاهیم هامبلین. پرور بالغ‌ترین اثر خود را در مورد این موضوع، کتاب گذشته، حال و آینده در سال ۱۹۶۷ منتشر کرد. او دو سال بعد درگذشت.

همراه با منطق زمان، پریور چند سیستم منطق موقعیتی را ساخت که ایده‌های اصلی خود را از Łoś به ارث برده‌اند. کار در منطق‌های زمانی موقعیتی توسط نیکلاس رسچر در دهه ۶۰ و ۷۰ ادامه یافت. در آثاری مانند یادداشت بر منطق زمانی (۱۹۶۶)، در مورد منطق قضایای زمانی (۱۹۶۸) ، منطق توپولوژیکی (۱۹۶۸)، منطق زمانی (۱۹۷۱) او در مورد ارتباط بین سیستم‌های Łoś و Prior تحقیق کرد. علاوه بر این او ثابت کرد که عملگرهای زمان قبلی را می‌توان با استفاده از عملگر تحقق در منطق‌های موقعیتی خاص تعریف کرد. رسچر در کار خود همچنین سیستم‌های کلی تری از منطق‌های موقعیتی ایجاد کرد. اگرچه اولین‌ها برای استفاده‌های صرفاً زمانی ساخته شدند، او اصطلاحی از منطق‌های توپولوژیکی را پیشنهاد کرد که شامل یک عملگر تحقق می‌شد، اما بدیهیات زمانی خاصی نداشت - مانند اصل ساعت.

عملگرهای زمانی دودویی Since و Until توسط هانس کمپ در دکترای سال ۱۹۶۸ معرفی شدند. پایان‌نامه، که همچنین حاوی یک نتیجه مهم است که منطق زمانی را به منطق مرتبه اول مرتبط می‌کند - نتیجه ای که اکنون به عنوان قضیه کمپ شناخته می‌شود.

دو رقیب اولیه در راستی‌آزمایی‌های رسمی، منطق زمانی خطی، منطق زمانی خطی توسط امیر پنولی، و منطق درخت محاسباتی، منطق زمانی منشعب شده توسط مردخای بن‌آری، زوهر ماننا و امیر پنولی بودند. یک فرمالیسم تقریباً معادل CTL در همان زمان توسط EM Clarke و EA Emerson پیشنهاد شد. این واقعیت که منطق دوم را می‌توان کارآمدتر از منطق اول تصمیم گرفت، به‌طور کلی بر منطق‌های انشعاب و خطی منعکس نمی‌شود، همان‌طور که گاهی اوقات استدلال شده‌است. در عوض، امرسون و لی نشان می‌دهند که هر منطق خطی را می‌توان به منطق انشعابی که می‌توان با همان پیچیدگی تصمیم‌گیری کرد، گسترش داد.

منطق موضعی Łoś

منطق Łoś با عنوان پایان‌نامه کارشناسی ارشد او در سال ۱۹۴۷ به زبان لهستانی منتشر شد. مفاهیم فلسفی و رسمی او را می‌توان ادامهٔ مکتب منطق لوو-ورشو دانست، زیرا سرپرست او یرژی اسلوپسکی، شاگرد یان لوکاسیویچ بود. این مقاله تا سال ۱۹۷۷ به انگلیسی ترجمه نشد، اگرچه هنریک هیژ در سال ۱۹۵۱ یک بررسی مختصر اما آموزنده در مجله منطق نمادین ارائه کرد. بررسی او حاوی مفاهیم اصلی کارش بود و برای محبوب کردن نتایج لوش در میان جامعه منطقی کافی بود. هدف اصلی این کار ارائه قوانین میل در چارچوب منطق صوری بود. برای دستیابی به این هدف، نویسنده در مورد اهمیت توابع زمانی در ساختار مفهوم میل تحقیق کرد. با توجه به اینکه او سیستم منطقی بدیهی خود را ارائه کرد که به عنوان چارچوبی برای قوانین میل همراه با جنبه‌های زمانی آنها مناسب است.

نحو

زبان منطق که اولین بار در Podstawy Analizy Metodologicznej Kanonów Milla (مبانی تجزیه و تحلیل روش شناختی روش‌های میل) منتشر شد عبارت بود از:

• عملگرهای منطقی مرتبه اول '¬'، '∧'، '∨'، '→'، '≡'، '∀' و '∃'
• اپراتور تحقق U
• نماد عملکردی δ
• متغیرهای گزاره ای p ₁, p ₂, p ₃ ,. . .
• متغیرهایی که لحظه‌های زمانی t ₁ ,t ₂ ,t ₃, را نشان می‌دهند. . .
• متغیرهایی که بازه‌های زمانی n ₁, n ₂, n ₃, را نشان می‌دهند. . .

مجموعه ای از اصطلاحات (که با S مشخص می‌شود) به صورت زیر ساخته می‌شود:

• متغیرهایی که لحظه‌ها یا بازه‌های زمانی را نشان می‌دهند اصطلاح هستند
• اگر $\tau \in S$ و $ϵ$ یک متغیر بازه زمانی است، پس $\delta (\tau ,ϵ)\in S$

مجموعه ای از فرمول‌ها (که با For مشخص می‌شوند) به صورت زیر ساخته می‌شوند:

• تمام فرمول‌های منطقی مرتبه اول معتبر هستند
• اگر $\tau \in S$ و $\varphi$ پس یک متغیر گزاره ای است $U_{\tau }(\varphi )\in For$
• اگر $\varphi \in For$ ، سپس $\mathrm{\neg }\varphi \in For$
• اگر $\varphi ,\psi \in For$ و $\circ \in \{\wedge ,\vee ,\to ,\equiv \}$ ، سپس $\varphi \circ \psi \in For$
• اگر $\varphi \in For$ و $Q\in \{\mathrm{\forall },\mathrm{\exists }\}$ و υ یک متغیر گزاره ای، لحظه ای یا بازه ای است، پس $Q_{\upsilon }\varphi \in For$

سیستم اصلی آکسیوماتیک

1. $U_{t_1}\mathrm{\neg }{p}_1\equiv \mathrm{\neg }{U}_{t_1}{p}_1$
2. $U_{t_1}(p_1\to p_2)\to (U_{t_1}{p}_1\to U_{t_1}{p}_2)$
3. $U_{t_1}((p_1\to p_2)\to ((p_2\to p_3)\to (p_1\to p_3)))$
4. $U_{t_1}(p_1\to (\mathrm{\neg }{p}_1\to p_2))$
5. $U_{t_1}((\mathrm{\neg }{p}_1\to p_1)\to p_1)$
6. ${\mathrm{\forall }}_{t_1}{U}_{t_1}{p}_1\to p_1$
7. ${\mathrm{\forall }}_{t_1}{\mathrm{\forall }}_{n_1}{\mathrm{\exists }}_{t_2}{\mathrm{\forall }}_{p_1}(U_{\delta (t_1,n_1)}{p}_1\equiv U_{t_2}{p}_1)$
8. ${\mathrm{\forall }}_{t_1}{\mathrm{\forall }}_{n_1}{\mathrm{\exists }}_{t_2}{\mathrm{\forall }}_{p_1}(U_{\delta (t_2,n_1)}{p}_1\equiv U_{t_1}{p}_1)$
9. ${\mathrm{\forall }}_{t_1}{\mathrm{\exists }}_{p_1}{\mathrm{\forall }}_{t_2}(U_{t_2}{p}_1\equiv {\mathrm{\forall }}_{p_2}(U_{t_1}{p}_2\equiv U_{t_2}{p}_2))$

منطق زمان قبلی (TL)

منطق زمان جمله ای معرفی شده در Time and Modality دارای چهار عملگر مودال (غیر حقیقت-عملکردی) است (علاوه بر همه عملگرهای صدق تابعی معمول در منطق گزاره ای مرتبه اول.

• پ: «اینطور بود. . " (P مخفف "گذشته" است)
• ف: «اینطور خواهد بود. . " (F مخفف "آینده" است)
• G: "همیشه همینطور خواهد بود. . "
• ح: «همیشه همین‌طور بود. . "

اگر اجازه دهیم π یک مسیر نامتناهی باشد، اینها را می‌توان ترکیب کرد:

• $\pi \models FG\varphi$ : «در یک نقطه خاص، $\varphi$ در تمام حالات آینده مسیر صادق است»
• $\pi \models GF\varphi$ : «$\varphi$ در بی‌نهایت بسیاری از حالات در مسیر درست است»

از P و F می‌توان G و H را تعریف کرد و بالعکس:

$\begin{array}{cc}F& \equiv \mathrm{\neg }G\mathrm{\neg }\\ P& \equiv \mathrm{\neg }H\mathrm{\neg }\end{array}$

نحو و معناشناسی

حداقل نحو برای TL با دستور BNF زیر مشخص شده‌است:

$\varphi ,\psi ::=a|\mathrm{\perp }|\mathrm{\neg }\varphi |\varphi \vee \psi |G\varphi |H\varphi$

که در آن a یک فرمول اتمی است.

از مدل‌های کریپکی برای ارزیابی صدق جملات در TL استفاده می‌شود. یک جفت (الگو:متغیر, <) از یک مجموعه الگو:متغیر و یک رابطه دودویی < روی الگو:متغیر (به نام "تقدم") یک قاب نامیده می‌شود. یک مدل با سه‌گانه (الگو:متغیر, <, الگو:متغیر) یک قاب و تابع الگو:متغیر به نام ارزش گذاری داده می‌شود که به هر جفت (الگو:متغیر, الگو:متغیر) از یک فرمول اتمی و مقدار زمانی مقداری حقیقت را اختصاص می‌دهد. مفهوم " الگو:متغیر در یک مدل الگو:متغیر =(الگو:متغیر, <, الگو:متغیر) در زمان الگو:متغیر " به اختصار الگو:متغیر ⊨ الگو:متغیر [[[:الگو:متغیر]]] است. با این نماد،

بیانیه	… درست زمانی است که
الگو:متغیر ⊨ الگو:متغیر [[[:الگو:متغیر]]]	الگو:متغیر (الگو:متغیر, الگو:متغیر)=درست است
الگو:متغیر ⊨¬ الگو:متغیر [[[:الگو:متغیر]]]	نه الگو:متغیر ⊨ الگو:متغیر [[[:الگو:متغیر]]]
الگو:متغیر ⊨(الگو:متغیر ∧ الگو:متغیر)[[[:الگو:متغیر]]]	الگو:متغیر ⊨ الگو:متغیر [[[:الگو:متغیر]]] و الگو:متغیر ⊨ الگو:متغیر [[[:الگو:متغیر]]]
الگو:متغیر ⊨(الگو:متغیر ∨ الگو:متغیر)[[[:الگو:متغیر]]]	الگو:متغیر ⊨ الگو:متغیر [[[:الگو:متغیر]]] یا الگو:متغیر ⊨ الگو:متغیر [[[:الگو:متغیر]]]
الگو:متغیر ⊨(الگو:متغیر → الگو:متغیر)[[[:الگو:متغیر]]]	الگو:متغیر ⊨ الگو:متغیر [[[:الگو:متغیر]]] اگر الگو:متغیر ⊨ الگو:متغیر [[[:الگو:متغیر]]]
الگو:متغیر ⊨G الگو:متغیر [[[:الگو:متغیر]]]	الگو:متغیر ⊨ الگو:متغیر [[[:الگو:متغیر]]] برای همه الگو:متغیر با الگو:متغیر < الگو:متغیر
الگو:متغیر ⊨H الگو:متغیر [[[:الگو:متغیر]]]	الگو:متغیر ⊨ الگو:متغیر [[[:الگو:متغیر]]] برای همه الگو:متغیر با الگو:متغیر < الگو:متغیر

با توجه به کلاس الگو:متغیر از فریم‌ها، یک جمله الگو:متغیر از TL است

• با توجه به الگو:متغیر معتبر است اگر برای هر مدل الگو:متغیر =(الگو:متغیر ,<, الگو:متغیر) با (الگو:متغیر ,<) در الگو:متغیر و برای هر الگو:متغیر در الگو:متغیر, الگو:متغیر ⊨ الگو:متغیر [[[:الگو:متغیر]]]
• اگر یک مدل الگو:متغیر =(الگو:متغیر ,<, الگو:متغیر) با (الگو:متغیر ,<) در الگو:متغیر وجود داشته باشد به گونه ای که برای برخی از الگو:متغیر در الگو:متغیر, الگو:متغیر ⊨ الگو:متغیر [[[:الگو:متغیر]]] با توجه به الگو:متغیر قابل رضایت است.
• نتیجه یک جمله الگو:متغیر با توجه به الگو:متغیر اگر برای هر مدل الگو:متغیر =(الگو:متغیر ,<, الگو:متغیر) با (الگو:متغیر ,<) در الگو:متغیر و برای هر الگو:متغیر در الگو:متغیر, اگر الگو:متغیر ⊨ الگو:متغیر [[[:الگو:متغیر]]]، آنگاه الگو:متغیر ⊨ الگو:متغیر [[[:الگو:متغیر]]]

بسیاری از جملات فقط برای دسته محدودی از فریم‌ها معتبر هستند. معمول است که کلاس فریم‌ها را به آنهایی که رابطه ای < متعدی، ضد متقارن، انعکاسی، تریکوتومی، غیر انعکاسی، کل، متراکم یا ترکیبی از اینها دارند محدود کنیم.

یک منطق بدیهی حداقلی

برگس منطقی را ترسیم می‌کند که هیچ فرضی در رابطه < ایجاد نمی‌کند، اما بر اساس طرح بدیهی زیر امکان استنتاج‌های معنی دار را می‌دهد:

1. الگو:متغیر where الگو:متغیر is a tautology of first-order logic
2. G(الگو:متغیر→الگو:متغیر)→(Gالگو:متغیر→Gالگو:متغیر)
3. H(الگو:متغیر→الگو:متغیر)→(Hالگو:متغیر→Hالگو:متغیر)
4. الگو:متغیر→GPالگو:متغیر
5. الگو:متغیر→HFالگو:متغیر

با قوانین کسر زیر:

1. با توجه به الگو:متغیر → الگو:متغیر و الگو:متغیر، الگو:متغیر را استنباط کنید (modus ponens)
2. با توجه به توتولوژی الگو:متغیر, G الگو:متغیر را استنباط کنید
3. با توجه به توتولوژی الگو:متغیر, H الگو:متغیر را استنباط کنید

می‌توان قوانین زیر را استخراج کرد:

1. قانون بکر: با توجه به الگو:متغیر → الگو:متغیر, T الگو:متغیر → T الگو:متغیر را استنباط کنید که در آن T یک زمان است، هر دنباله ای که از G, H، F و P ساخته شده باشد.
2. آینه سازی: با در نظر گرفتن یک قضیه الگو:متغیر، گزاره آینه ای آن الگو:متغیر ^§ را استنباط کنید، که با جایگزینی G با H (و بنابراین F با P) و بالعکس به دست می‌آید.
3. دوگانگی: با در نظر گرفتن یک قضیه الگو:متغیر، عبارت دوگانه الگو:متغیر * را استنباط کنید که از مبادله ∧ با ∨، G با F و H با P به دست می‌آید.

ترجمه به منطق محمول

برگس ترجمه مردیتی را از گزاره‌های TL به گزاره‌هایی در منطق مرتبه اول با یک متغیر آزاد الگو:متغیر ₀ (نماینده لحظه حال) ارائه می‌کند. این ترجمه الگو:متغیر به صورت بازگشتی به صورت زیر تعریف می‌شود:

$\begin{array}{cccc}& M(a)& & =a^{*}{x}_0\\ & M(\mathrm{\neg }\varphi )& & =\mathrm{\neg }M(\varphi )\\ & M(\varphi \wedge \psi )& & =M(\varphi )\wedge M(\psi )\\ & M(𝖦\varphi )& & =\mathrm{\forall }{x}_1(x_0<x_1\to M(A^{+}))\\ & M(𝖧\varphi )& & =\mathrm{\forall }{x}_1(x_1<x_0\to M(A^{+}))\end{array}$

جایی که $A^{+}$ جمله است $A$ با تمام شاخص‌های متغیر با ۱ و افزایش یافته‌است $a^{*}$ یک محمول یک مکان است که توسط $x\mapsto V(a,x)$ .

عملگرهای زمانی

منطق زمانی دو نوع عملگر دارد: عملگرهای منطقی و عملگرهای مدال. عملگرهای منطقی عملگرهای معمولی با تابع حقیقت هستند ($\mathrm{\neg },\vee ,\wedge ,\to$). عملگرهای مدال مورد استفاده در منطق زمانی خطی و منطق درخت محاسباتی به صورت زیر تعریف می‌شوند.

متنی	نمادین	تعریف	توضیح	نمودار
عملگرهای باینری
الگو:Mvar U الگو:Mvar	$\varphi 𝒰\psi$	$(B𝒰C)(\varphi )=(\mathrm{\exists }i:C({\varphi }_i)\wedge (\mathrm{\forall }j<i:B({\varphi }_j)))$	U ntil: الگو:Mvar در موقعیت فعلی یا آینده باقی می‌ماند و الگو:Mvar باید تا آن موقعیت باقی بماند. در آن موقعیت الگو:Mvar لازم نیست بیشتر نگه دارد.	<timeline> ImageSize = width:240 height:94 PlotArea = left:30 bottom:30 top:0 right:20 DateFormat = x.y Period = from:0 till:6 TimeAxis = orientation:horizontal AlignBars = justify ScaleMajor = gridcolor:black increment:1 start:0 ScaleMinor = gridcolor:black increment:1 start:0 PlotData= bar:p color:red width:10 align:left fontsize:S from:1 till:3 bar:q color:red width:10 align:left fontsize:S from:3 till:5 bar:pUq color:red width:10 align:left fontsize:S from:1 till:5 </timeline>
الگو:Mvar R الگو:Mvar	$\varphi ℛ\psi$	$(BℛC)(\varphi )=(\mathrm{\forall }i:C({\varphi }_i)\vee (\mathrm{\exists }j<i:B({\varphi }_j)))$	رها شدن R: الگو:Mvar آزاد می‌کند اگر الگو:Mvar درست باشد تا زمانی که اولین الگو:Mvar که الگو:Mvar درست است (یا برای همیشه اگر چنین موقعیتی وجود نداشته باشد) را شامل می‌شود.	<timeline> ImageSize = width:240 height:100 PlotArea = left:30 bottom:30 top:0 right:20 DateFormat = x.y Period = from:0 till:8 TimeAxis = orientation:horizontal AlignBars = justify ScaleMajor = gridcolor:black increment:1 start:0 ScaleMinor = gridcolor:black increment:1 start:0 PlotData= bar:p color:red width:10 align:left fontsize:S from:2 till:4 from:6 till:8 bar:q color:red width:10 align:left fontsize:S from:1 till:3 from:5 till:6 from:7 till:8 bar:pRq color:red width:10 align:left fontsize:S from:1 till:3 from:7 till:8 </timeline>
عملگرهای Unary
N الگو:Mvar	$◯\varphi$	$𝒩B({\varphi }_i)=B({\varphi }_{i+1})$	N ext: الگو:Mvar باید در حالت بعدی باقی بماند. (X به صورت مترادف استفاده می‌شود)	<timeline> ImageSize = width:240 height:60 PlotArea = left:30 bottom:30 top:0 right:20 DateFormat = x.y Period = from:0 till:6 TimeAxis = orientation:horizontal AlignBars = justify ScaleMajor = gridcolor:black increment:1 start:0 ScaleMinor = gridcolor:black increment:1 start:0 PlotData= bar:p color:red width:10 align:left fontsize:S from:2 till:3 from:5 till:6 bar:Np color:red width:10 align:left fontsize:S from:1 till:2 from:4 till:5 </timeline>
F الگو:Mvar	$◊\varphi$	$ℱB(\varphi )=(true𝒰B)(\varphi )$	F uture: الگو:Mvar در نهایت باید نگه داشته شود (جایی در مسیر بعدی).	<timeline> ImageSize = width:240 height:60 PlotArea = left:30 bottom:30 top:0 right:20 DateFormat = x.y Period = from:0 till:6 TimeAxis = orientation:horizontal AlignBars = justify ScaleMajor = gridcolor:black increment:1 start:0 ScaleMinor = gridcolor:black increment:1 start:0 PlotData= bar:p color:red width:10 align:left fontsize:S from:2 till:3 from:4 till:5 bar:Fp color:red width:10 align:left fontsize:S from:0 till:5 </timeline>
G الگو:Mvar	$◻\varphi$	$𝒢B(\varphi )=\mathrm{\neg }ℱ\mathrm{\neg }B(\varphi )$	G lobally: الگو:Mvar باید در کل مسیر بعدی باقی بماند.	<timeline> ImageSize = width:240 height:60 PlotArea = left:30 bottom:30 top:0 right:20 DateFormat = x.y Period = from:0 till:6 TimeAxis = orientation:horizontal AlignBars = justify ScaleMajor = gridcolor:black increment:1 start:0 ScaleMinor = gridcolor:black increment:1 start:0 PlotData= bar:p color:red width:10 align:left fontsize:S from:1 till:3 from:4 till:6 bar:Gp color:red width:10 align:left fontsize:S from:4 till:6 </timeline>
A الگو:Mvar	$\mathrm{\forall }\varphi$	$(𝒜B)(\psi )=(\mathrm{\forall }\varphi :{\varphi }_0=\psi \to B(\varphi ))$	A ll: الگو:Mvar باید در تمام مسیرهایی که از حالت فعلی شروع می‌شوند، حفظ شود.
E الگو:Mvar	$\mathrm{\exists }\varphi$	$(ℰB)(\psi )=(\mathrm{\exists }\varphi :{\varphi }_0=\psi \wedge B(\varphi ))$	E xists: حداقل یک مسیر وجود دارد که از حالت فعلی شروع می‌شود، جایی که الگو:Mvar برقرار است.

نمادهای جایگزین:

• عملگر R گاهی با V نشان داده می‌شود
• عملگر W ضعیف است تا زمانی که عملگر: $f𝐖g$ برابر است با $f𝐔g\vee 𝐆f$

هر زمان که الگو:ریاضی به خوبی شکل گرفته باشد، عملگرهای Unary فرمول‌های خوبی هستند. عملگرهای دودویی هر زمان که الگو:ریاضی و الگو:ریاضی به خوبی شکل گرفته باشند، فرمول‌های خوبی هستند.

در برخی از منطق‌ها، برخی از عملگرها قابل بیان نیستند. به عنوان مثال، عملگر N را نمی‌توان در منطق زمانی اعمال بیان کرد.

منطق‌های زمانی

منطق‌های زمانی عبارتند از:

• برخی از سیستم‌های منطق موضعی
• منطق زمانی فاصله (ITL)
• منطق زمانی خطی (LTL)
• منطق درخت محاسباتی (CTL)
• منطق زمانی سیگنال (STL)
• منطق زمانی مهر زمانی (TTL)
• زبان مشخصات ویژگی (PSL)
• CTL* که LTL و CTL را تعمیم می‌دهد
• منطق هنسی-میلنر (HML)
• مدال μ-حساب که به عنوان یک زیر مجموعه HML و CTL* را شامل می‌شود
• منطق زمانی متریک (MTL)
• منطق زمانی فاصله متریک (MITL)
• منطق زمانی گزاره ای زمان‌بندی شده (TPTL)
• منطق زمانی خطی کوتاه (TLTL)
• منطق بیش از حد زمانی (HyperLTL)

تغییراتی که ارتباط نزدیکی با منطق زمانی یا زمانی یا زمانی دارد، منطق‌های مودال مبتنی بر «توپولوژی»، «مکان» یا «موقعیت مکانی» هستند.

جستارهای وابسته

• فرمالیسم HPO
• ساختار کریپکی
• تئوری خودکار
• دستور زبان چامسکی
• سیستم انتقال دولت
• محاسبه مدت زمان (DC)
• منطق ترکیبی
• منطق زمانی در تأیید حالت محدود
• منطق زمانی اعمال (TLA)
• انتشارات مهم در تأیید رسمی (از جمله استفاده از منطق زمانی در تأیید رسمی)
• زبان هماهنگی Reo
• منطق مدال
• مواد تحقیق: آرشیو انجمن ماکس پلانک

منابع

• مردخای بن آری، زوهر ماننا، امیر پنولی: منطق زمانی شاخه‌بندی زمان. POPL 1981: 164-176
• Amir Pnueli: The Temporal Logic of Programs FOCS 1977: 46-57
• Venema, Yde, 2001, "Temporal Logic" در Goble, Lou, ed. , The Blackwell Guide to Philosophical Logic. بلک ول.
• EA Emerson و C. Lei, " روش‌های بررسی مدل: منطق زمان انشعاب ضربه می‌زند "، در Science of Computer Programming 8, pp. 275-306، ۱۹۸۷.
• EA Emerson, " منطق زمانی و مدال "، کتابچه راهنمای علوم کامپیوتر نظری، فصل ۱۶، انتشارات MIT، ۱۹۹۰
• مقدمه ای عملی بر PSL، سیندی آیزنر، دانا فیسمن
• 978-3-540-69849-4 پیش چاپ. دیدگاه تاریخی در مورد اینکه چگونه ایده‌های به ظاهر متفاوت در علوم کامپیوتر و مهندسی گرد هم آمده‌اند. (اشاره به چرچ در عنوان این مقاله اشاره ای به یک مقاله کمتر شناخته شده در سال ۱۹۵۷ است که در آن چرچ راهی برای انجام تأیید سخت‌افزاری پیشنهاد کرده‌است)

پیوند به بیرون

• دایرةالمعارف فلسفه استنفورد: " منطق زمانی " - نوشته آنتونی گالتون.
• منطق زمانی نوشته Yde Venema، شرح رسمی نحو و معناشناسی، سوالات بدیهی سازی. همچنین عملگرهای زمانی دوتایی کامپ (از تا کنون)
• یادداشت‌هایی درباره بازی‌ها در منطق زمانی توسط ایان هادکینسون، از جمله توصیف رسمی از منطق زمانی مرتبه اول
• CADP - چک کننده‌های مدل عمومی را برای منطق‌های زمانی مختلف ارائه می‌دهد
• PAT یک مدل جستجوگر رایگان، جستجوگر LTL، شبیه‌ساز و بررسی کننده اصلاحات برای CSP و برنامه‌های افزودنی آن (با متغیر مشترک، آرایه‌ها، طیف وسیعی از عدالت) است.