टेम्पोरल लॉजिक

लॉजिक में, टेम्पोरल लॉजिक समय के संदर्भ में योग्य प्रस्तावों का प्रतिनिधित्व करने और उनके बारे में लॉजिक करने के लिए नियमों और प्रतीकों की कोई भी प्रणाली है (उदाहरण के लिए, मैं प्रायः भूखा हूं, मैं आखिरकार भूखा रहूंगा, या मैं भूखा रहूँगा जब तक मैं कुछ खा लूँगा )। यह कभी-कभी तनावपूर्ण लॉजिक को संदर्भित करने के लिए भी प्रयोग किया जाता है, 1950 के दशक के अंत में आर्थर प्रायर द्वारा प्रांरम्भ की गई टेम्पोरल लॉजिक की एक मॉडल लॉजिक-आधारित प्रणाली, उनका संघर्ष द्वारा महत्वपूर्ण योगदान के साथ। इसे कंप्यूटर वैज्ञानिकों, विशेष रूप से आमिर पनुएली और लॉजिकशास्त्रियों द्वारा विकसित किया गया है।

टेम्पोरल लॉजिक को औपचारिक सत्यापन में एक महत्वपूर्ण अनुप्रयोग मिला है, जहां इसका उपयोग हार्डवेयर या सॉफ्टवेयर सिस्टम की आवश्यकताओं को बताने के लिए किया जाता है। उदाहरण के लिए, कोई यह कहना चाह सकता है कि जब भी एक अनुरोध किया जाता है, संसाधन तक पहुंच आखिरकार दी जाती है, लेकिन यह दो अनुरोधकर्ताओं को एक साथ कभी नहीं दी जाती है। इस तरह के बयान को अस्थायी लॉजिक में आसानी से व्यक्त किया जा सकता है।

प्रेरणा

कथन पर विचार करें मुझे भूख लगी है। हालांकि इसका अर्थ समय में स्थिर है, कथन का सत्य मूल्य समय में भिन्न हो सकता है। कभी यह सच होता है, और कभी झूठ, लेकिन कभी भी सच और झूठ एक साथ नहीं। एक टेम्पोरल लॉजिक में, एक बयान में एक सत्य मूल्य हो सकता है जो समय के साथ बदलता रहता है - एक अस्थायी लॉजिक के विपरीत, जो केवल उन बयानों पर लागू होता है जिनके सत्य मूल्य समय में स्थिर होते हैं। समय के साथ सत्य-मूल्य का यह उपचार टेम्पोरल लॉजिक को कम्प्यूटेशनल क्रिया लॉजिक से अलग करता है।

टेम्पोरल लॉजिक में प्रायः टाइमलाइन के बारे में लॉजिक करने की क्षमता होती है। तथाकथित रैखिक-समय लॉजिक इस प्रकार के लॉजिक तक ही सीमित हैं। ब्रांचिंग-टाइम लॉजिक्स, हालांकि, कई समयसीमाओं के बारे में लॉजिक कर सकते हैं। यह उन वातावरणों के विशेष उपचार की अनुमति देता है जो अप्रत्याशित रूप से कार्य कर सकते हैं। उदाहरण को जारी रखने के लिए, ब्रांचिंग-टाइम लॉजिक में हम कह सकते हैं कि एक संभावना है कि मैं प्रायः के लिए भूखा रहूँगा, और एक संभावना है कि अंततः मुझे भूख नहीं लगेगी। यदि हम नहीं जानते कि मुझे कभी खिलाया जाएगा या नहीं, तो ये दोनों कथन सत्य हो सकते हैं।

इतिहास

हालांकि अरस्तू का लॉजिक लगभग पूरी तरह से स्पष्ट न्यायवाक्य के सिद्धांत से संबंधित है, उनके काम में ऐसे अंश हैं जिन्हें अब टेम्पोरल लॉजिक की प्रत्याशा के रूप में देखा जाता है, और प्रथम-क्रम लॉजिक का एक प्रारंभिक, आंशिक रूप से विकसित रूप हो सकता है। मोडल द्विसंयोजक लॉजिक लॉजिक। अरस्तू विशेष रूप से भविष्य की आकस्मिकताओं की समस्या से चिंतित था, जहां वह यह स्वीकार नहीं कर सकता था कि भविष्य की घटनाओं के बारे में बयानों पर द्वंद्व का सिद्धांत लागू होता है, यानी हम वर्तमान में यह तय कर सकते हैं कि भविष्य की घटनाओं के बारे में कोई बयान सही है या गलत, जैसे कि कल एक समुद्री युद्ध हो। सहस्राब्दी के लिए बहुत कम विकास हुआ, चार्ल्स सैंडर्स पियर्स ने 19 वीं शताब्दी में उल्लेख किया:

समय को सामान्यतः तर्कशास्त्रियों द्वारा 'एक्स्ट्रालॉजिकल' पदार्थ कहा जाता है। मैंने कभी इस राय को साझा नहीं किया। लेकिन मैंने सोचा है कि तर्क अभी तक विकास की स्थिति तक नहीं पहुंचा था, जिस पर इसके रूपों के लौकिक संशोधनों की प्रांरम्भ से बड़ी गड़बड़ी नहीं होगी; और मैं अभी भी उस तरह की सोच का हूं।

आश्चर्यजनक रूप से चार्ल्स सैंडर्स पियर्स के लिए, टेम्पोरल लॉजिक की पहली प्रणाली का निर्माण किया गया था, जहाँ तक हम जानते हैं, 20 वीं शताब्दी के पहले भाग में। हालांकि आर्थर प्रायर को व्यापक रूप से टेम्पोरल लॉजिक के संस्थापक के रूप में जाना जाता है, इस तरह के लॉजिक की पहली औपचारिकता 1947 में पोलिश लॉजिकशास्त्री जेरज़ी लोस द्वारा प्रदान की गई थी। अपने काम पोडस्टावी एनालिज़ी मेटोडोलॉजिक्ज़नेज कानोनोव मिल्ला (द फाउंडेशन ऑफ़ ए मेथोडोलॉजिकल एनालिसिस ऑफ़ मिल्स मेथड्स) में उन्होंने मिल के सिद्धांतों का एक औपचारिक रूप प्रस्तुत किया। जेरज़ी लॉस के दृष्टिकोण में, समय कारक पर जोर दिया गया था। इस प्रकार, अपने लक्ष्य तक पहुँचने के लिए, उसे एक लॉजिक का निर्माण करना पड़ा जो लौकिक कार्यों की औपचारिकता के लिए साधन प्रदान कर सके। लॉजिक को जेरज़ी लॉस के मुख्य उद्देश्य के प्रतिफल के रूप में देखा जा सकता है, यद्यपि यह पहला स्थितीय लॉजिक था, जिसे एक रूपरेखा के रूप में, बाद में ज्ञानशास्त्रीय लॉजिक में जेरज़ी लॉस के आविष्कारों के लिए इस्तेमाल किया गया था। लॉजिक में सिंटैक्स प्रायर के टेंस लॉजिक से बहुत अलग है, जो मोडल ऑपरेटरों का उपयोग करता है। जेरज़ी लॉस 'लॉजिक की भाषा बल्कि एक अहसास ऑपरेटर का उपयोग करती है, जो स्थिति संबंधी लॉजिक के लिए विशिष्ट है, जो विशिष्ट संदर्भ के साथ अभिव्यक्ति को बांधता है जिसमें इसका सत्य-मूल्य माना जाता है। जेरज़ी लॉस के कार्य में यह माना गया संदर्भ केवल लौकिक था, इस प्रकार अभिव्यक्ति विशिष्ट क्षणों या समय के अंतराल से बंधी हुई थी।

बाद के वर्षों में, आर्थर प्रायर द्वारा टेम्पोरल लॉजिकशास्त्र का शोध प्रांरम्भ हुआ।वह स्वतंत्र इच्छा और पूर्वनियति के दार्शनिक निहितार्थों से चिंतित थे। उनकी पत्नी के अनुसार, उन्होंने पहली बार 1953 में टेम्पोरल लॉजिक को औपचारिक बनाने पर विचार किया। उनके शोध के परिणाम पहली बार 1954 में वेलिंग्टन में सम्मेलन में प्रस्तुत किए गए।पहले प्रस्तुत की गई प्रणाली वाक्य रचना की दृष्टि से जेरज़ी लॉस लॉजिक के समान थी, हालांकि 1955 तक उन्होंने प्रायर के औपचारिक लॉजिक में परिशिष्ट 1 के अंतिम खंड में स्पष्ट रूप से जेरज़ी लॉस के कार्य का उल्लेख नहीं किया था।

आर्थर प्रायर ने 1955-6 में ऑक्सफोर्ड विश्वविद्यालय में इस विषय पर व्याख्यान दिया, और 1957 में एक पुस्तक, टाइम एंड मॉडेलिटी प्रकाशित की, जिसमें उन्होंने दो लौकिक संयोजकों (मोडल ऑपरेटर्स ), एफ और पी के साथ एक प्रस्तावपरक लॉजिक मोडल लॉजिक पेश किया। भविष्य में कुछ समय और अतीत में कुछ समय के अनुरूप। इस प्रारंभिक कार्य में प्रायर ने समय को रेखीय माना। हालाँकि, 1958 में, उन्हें शाऊल क्रिपके का एक पत्र मिला, जिसने बताया कि यह धारणा शायद अनुचित है। एक ऐसे विकास में जिसने कंप्यूटर विज्ञान में इसी तरह के एक को पूर्वाभास दिया, प्रायर ने इसे सलाह के तहत लिया, और ब्रांचिंग टाइम के दो सिद्धांतों को विकसित किया, जिसे उन्होंने ओखमिस्ट और पीयरसियन कहा।, 1958 और 1965 के बीच प्रायर ने चार्ल्स लियोनार्ड हैम्बलिन के साथ भी पत्राचार किया था, और इस क्षेत्र में कई शुरुआती विकासों को इस पत्राचार से खोजा जा सकता है, उदाहरण के लिए हैम्ब्लिन निहितार्थ। प्रायर ने 1967 में इस विषय पर अपना सबसे परिपक्व काम पास्ट, प्रेजेंट, एंड फ्यूचर प्रकाशित किया। दो साल बाद उनकी मृत्यु हो गई। तनावपूर्ण लॉजिक के साथ, आर्थर प्रायर ने स्थितीय लॉजिक की कुछ प्रणालियों का निर्माण किया, जो उनके मुख्य विचारों को जेर्जी लोश से विरासत में मिला। 60 और 70 के दशक में निकोलस रेसचर द्वारा स्थितीय लौकिक लॉजिक्स में काम जारी रखा गया था। कालानुक्रमिक लॉजिक पर नोट (1966), कालानुक्रमिक प्रस्तावों के लॉजिक पर (1968), स्थलीय लॉजिक (1968), और टेम्पोरल लॉजिक (1971) जैसे कार्यों में उन्होंने जेरज़ी लॉस और आर्थर प्रायर की प्रणालियों के बीच संबंधों पर शोध किया। इसके अलावा उन्होंने साबित किया कि आर्थर प्रायर के काल संचालकों को विशिष्ट स्थितीय लॉजिकशास्त्र में एक अहसास संचालक का उपयोग करके परिभाषित किया जा सकता है।निकोलस रेसचर ने अपने काम में, स्थितीय लॉजिकशास्त्र की अधिक सामान्य प्रणालियाँ भी बनाईं। हालांकि पहले वाले विशुद्ध रूप से लौकिक उपयोगों के लिए बनाए गए थे, उन्होंने लॉजिकशास्त्र के लिए टोपोलॉजिकल लॉजिक्स शब्द का प्रस्ताव दिया था, जो एक अहसास ऑपरेटर को सम्मिलित करने के लिए था, लेकिन कोई विशिष्ट लौकिक स्वयंसिद्ध नहीं था - जैसे घड़ी का स्वयंसिद्ध।

बाइनरी टेम्पोरल ऑपरेटर से और जब तक हंस काम्प द्वारा 1968 में अपनी पीएच.डी. में पेश किए गए थे। थीसिस, जिसमें एक महत्वपूर्ण परिणाम भी सम्मिलित है जो टेम्पोरल लॉजिक को पहले क्रम के लॉजिक से संबंधित करता है - एक परिणाम जिसे अब काम्प के प्रमेय के रूप में जाना जाता है। औपचारिक सत्यापन में दो प्रारंभिक दावेदार रैखिक टेम्पोरल लॉजिक थे, आमिर पनुएली द्वारा एक रैखिक-समय लॉजिक, और गणना वृक्ष लॉजिक (सीएलटी), मोर्दचाई बेन-अरी, जौहर मन्ना और अमीर पनुएली द्वारा एक शाखा-समय लॉजिक। लगभग उसी समय एडमंड एम. क्लार्क|ई द्वारा सीटीएल के लगभग समकक्ष औपचारिकता का सुझाव दिया गया था। एम. क्लार्क और ई. एलन एमर्सन|ई. ए एमर्सन। तथ्य यह है कि दूसरा लॉजिक पहले की तुलना में निर्णय समस्या कम्प्यूटेशनल जटिलता हो सकता है, सामान्य तौर पर ब्रांचिंग- और रैखिक-समय के लॉजिकों पर प्रतिबिंबित नहीं होता है, जैसा कि कभी-कभी लॉजिक दिया गया है। बदले में, इमर्सन और लेई दिखाते हैं कि किसी भी रैखिक-समय लॉजिक को शाखा-समय लॉजिक तक बढ़ाया जा सकता है जिसे उसी जटिलता से तय किया जा सकता है।

मूस 'स्थितीय लॉजिक

जेरज़ी लॉस लॉजिक को उनके 1947 के मास्टर की थीसिस द फ़ाउंडेशन ऑफ़ ए मेथोडोलॉजिकल एनालिसिस ऑफ़ मिल्स मेथड्स के रूप में प्रकाशित किया गया था। उनकी दार्शनिक और औपचारिक अवधारणाओं को लविव-वारसॉ स्कूल ऑफ़ लॉजिक की निरंतरता के रूप में देखा जा सकता है, क्योंकि उनके पर्यवेक्षक जेरज़ी स्लूपेकी थे, जो जन लुकासिविक्ज़ के शिष्य थे। पेपर का 1977 तक अंग्रेजी में अनुवाद नहीं किया गया था, हालांकि हेनरिक हाईज़ ने 1951 में एक संक्षिप्त, लेकिन सूचनात्मक, प्रतीकात्मक लॉजिक का जर्नल में समीक्षा प्रस्तुत की। इस समीक्षा में जेरज़ी लॉस के काम की मूल अवधारणाएँ सम्मिलित थीं और तार्किक समुदाय के बीच उनके परिणामों को लोकप्रिय बनाने के लिए पर्याप्त थीं। इस कार्य का मुख्य उद्देश्य मिल के सिद्धांतों को औपचारिक लॉजिक के ढांचे में प्रस्तुत करना था। इस लक्ष्य को प्राप्त करने के लिए लेखक ने मिल की अवधारणा की संरचना में लौकिक कार्यों के महत्व पर शोध किया। ऐसा करने के बाद, उन्होंने लॉजिक की अपनी स्वयंसिद्ध प्रणाली प्रदान की जो मिल के सिद्धांतों के साथ-साथ उनके लौकिक पहलुओं के लिए एक रूपरेखा के रूप में फिट होगी।

सिंटेक्स

पोडस्टावी एनालिज़ी मेटोडोलॉजिक्ज़नेज कानोनोव मिल्ला (द फ़ाउंडेशन ऑफ़ ए मेथोडोलॉजिकल एनालिसिस ऑफ़ मिल्स मेथड्स) में पहली बार प्रकाशित लॉजिक की भाषा में सम्मिलित हैं:

• पहले क्रम के लॉजिक ऑपरेटर्स '¬', '∧', '∨', '→', '≡', '∀' और '∃'
• प्राप्ति संचालक U
• कार्यात्मक प्रतीक δ
• प्रस्तावक चर p₁,p₂,p₃,...
• समय के क्षणों को निरूपित करने वाले चर t₁,t₂,t₃,...
• समय अंतराल को निरूपित करने वाले चर n₁,n₂,n₃,...

शर्तों का सेट (S द्वारा चिह्नित) निम्नानुसार बनाया गया है:

• समय के क्षणों या अंतराल को दर्शाने वाले चर शब्द हैं
• अगर $\tau \in S$ और $\epsilon$ एक समय अंतराल चर है, तो $\delta (\tau ,\epsilon )\in S$

सूत्रों का सेट (जिसे फॉर द्वारा दर्शाया गया है) इस प्रकार बनाया गया है:

• सभी प्रथम-क्रम लॉजिक सूत्र मान्य हैं
• अगर $\tau \in S$ और $\phi$ एक प्रस्तावक चर है, फिर $U_{\tau }(\phi )\in For$
• अगर $\phi \in For$, तब $\neg \phi \in For$
• अगर $\phi ,\psi \in For$ और $\circ \in \{\wedge ,\vee ,\rightarrow ,\equiv \}$, तब $\phi \circ \psi \in For$
• अगर $\phi \in For$ और $Q\in \{\forall ,\exists \}$ और υ तब एक प्रस्तावात्मक, क्षण या अंतराल चर है $Q_{\upsilon }\phi \in For$

मूल स्वयंसिद्ध प्रणाली

1. $U_{t_{1}}\neg p_{1}\equiv \neg U_{t_{1}}p_{1}$
2. $U_{t_{1}}(p_{1}\rightarrow p_{2})\rightarrow (U_{t_{1}}p_{1}\rightarrow U_{t_{1}}p_{2})$
3. $U_{t_{1}}((p_{1}\rightarrow p_{2})\rightarrow ((p_{2}\rightarrow p_{3})\rightarrow (p_{1}\rightarrow p_{3})))$
4. $U_{t_{1}}(p_{1}\rightarrow (\neg p_{1}\rightarrow p_{2}))$
5. $U_{t_{1}}((\neg p_{1}\rightarrow p_{1})\rightarrow p_{1})$
6. $\forall _{t_{1}}U_{t_{1}}p_{1}\rightarrow p_{1}$
7. $\forall _{t_{1}}\forall _{n_{1}}\exists _{t_{2}}\forall _{p_{1}}(U_{\delta (t_{1},n_{1})}p_{1}\equiv U_{t_{2}}p_{1})$
8. $\forall _{t_{1}}\forall _{n_{1}}\exists _{t_{2}}\forall _{p_{1}}(U_{\delta (t_{2},n_{1})}p_{1}\equiv U_{t_{1}}p_{1})$
9. $\forall _{t_{1}}\exists _{p_{1}}\forall _{t_{2}}(U_{t_{2}}p_{1}\equiv \forall _{p_{2}}(U_{t_{1}}p_{2}\equiv U_{t_{2}}p_{2}))$

पूर्व काल का लॉजिक (टीएल)

टाइम एंड मॉडेलिटी में पेश किए गए वाक्यात्मक काल लॉजिक में चार (गैर-सत्य कार्य | सत्य-कार्यात्मक) मोडल ऑपरेटर हैं (प्रस्तावात्मक कलन में सभी सामान्य सत्य-कार्यात्मक ऑपरेटरों के अलावा | प्रथम-क्रम प्रस्तावपरक लॉजिक)।

• P: यह मामला था कि... (P अतीत के लिए खड़ा है)
• F: यह मामला होगा कि ... (F भविष्य के लिए खड़ा है)
• G: प्रायः ऐसा ही रहेगा कि...
• H: प्रायः ऐसा होता था कि...

इन्हें संयुक्त किया जा सकता है यदि हम π को एक अनंत पथ होने दें:

• $\pi \vDash FG\phi$: एक निश्चित बिंदु पर, $\phi$ पथ की सभी भावी अवस्थाओं में सत्य है
• $\pi \vDash GF\phi$:$\phi$ पथ पर अपरिमित रूप से अनेक अवस्थाओं में सत्य है

P और F से G और H को परिभाषित किया जा सकता है, और इसके विपरीत:

${\begin{aligned}F&\equiv \lnot G\lnot \\P&\equiv \lnot H\lnot \end{aligned}}$

सिंटेक्स और शब्दार्थ

टीएल के लिए एक न्यूनतम सिंटैक्स निम्नलिखित बैकस-नौर फॉर्म के साथ निर्दिष्ट किया गया है:

$\phi ,\psi ::=a\;|\;\bot \;|\;\lnot \phi \;|\;\phi \lor \psi \;|\;G\phi \;|\;H\phi$ जहाँ ए कुछ परमाणु सूत्र है। टीएल में वाक्य (गणितीय लॉजिक) की सच्चाई का मूल्यांकन करने के लिए कृपके शब्दार्थ का उपयोग किया जाता है। एक जोड़ी (T, <) एक सेट के T और एक द्विआधारी संबंध <पर T (प्राथमिकता कहा जाता है) को एक फ्रेम कहा जाता है। एक मॉडल ट्रिपल द्वारा दिया गया है (T, <, V) एक फ्रेम और एक फ़ंक्शन का V एक मूल्यांकन कहा जाता है जो प्रत्येक जोड़ी को निर्दिष्ट करता है (a, u) एक परमाणु सूत्र और एक समय मूल्य कुछ सत्य मान। धारणाϕ एक मॉडल में सच है U=(T, <, V) समय पर u संक्षिप्त है Uडबल घूमने वाला दरवाज़ा|⊨ϕ[u]। इस अंकन के साथ,

कथन	सच है जब बस
U⊨a[u]	V(a,u)=true
U⊨¬ϕ[u]	not U⊨ϕ[u]
U⊨(ϕ∧ψ)[u]	U⊨ϕ[u] ए nd U⊨ψ[u]
U⊨(ϕ∨ψ)[u]	U⊨ϕ[u] or U⊨ψ[u]
U⊨(ϕ→ψ)[u]	U⊨ψ[u] if U⊨ϕ[u]
U⊨Gϕ[u]	U⊨ϕ[v] for all v with u<v
U⊨Hϕ[u]	U⊨ϕ[v] for all v with v<u

फ़्रेम के वर्ग F को देखते हुए, TL का एक वाक्य ϕ है

• F के संबंध में वैध अगर प्रत्येक मॉडल U = (T, <, V) के साथ (T, <) F में और प्रत्येक u के लिए T में, U⊨ϕ [u]
• F के संबंध में संतोषजनक अगर एक मॉडल U = (T, <, V) के साथ (T, <) F में ऐसा है कि T में कुछ u के लिए, U⊨ϕ [u]
• F के संबंध में एक वाक्य ψ का परिणाम यदि प्रत्येक मॉडल के लिए U=(T,<,V) के साथ (T,<) F में और प्रत्येक u के लिए T में, यदि U⊨ψ[u], तो U⊨ϕ [u]

कई वाक्य केवल सीमित वर्ग के फ्रेम के लिए मान्य हैं। फ्रेम के वर्ग को उन लोगों तक सीमित करना आम है जिनके संबंध हैं < जो सकर्मक कमी, एंटीसिमेट्रिक संबंध , अल्हड़ रिलेशन, ट्राइकोटॉमी (गणित), अपरिवर्तनीय, कुल आदेश, घने क्रम, या इनमें से कुछ संयोजन है।

एक न्यूनतम स्वयंसिद्ध लॉजिक

बर्गेस एक ऐसे लॉजिक को रेखांकित करता है जो संबंध < पर कोई धारणा नहीं बनाता है, लेकिन निम्नलिखित स्वयंसिद्ध स्कीमा के आधार पर सार्थक कटौती की अनुमति देता है: [15]

1. A जहां A प्रथम-क्रम लॉजिक का पुनरुत्पादन टॉटोलॉजी (लॉजिक)
2. (A→B)→(GA→GB)
3. H(A→B)→(HA→HB)
4. A→GPA
5. A→HFA

कटौती के निम्नलिखित नियमों के साथ:

1. दिए गए A→B और A, घटाएँ B (एक वैध, सरल लॉजिक और निष्कर्ष के नियम के रूप)
2. एक टॉटोलॉजी A दी गई, GA का अनुमान लगाएं
3. एक टॉटोलॉजी A दिया, अनुमान हा

कोई निम्नलिखित नियम प्राप्त कर सकता है

1. बेकर का नियम: दिया गया A→B, घटाएँ TA → TB जहां T एक काल है, G, H, F, और P से बना कोई भी अनुक्रमणिका।
2. मिररिंग: एक प्रमेय दिया गया A, इसका दर्पण कथन निकालिए A^§, जो G को H से (और इसलिए F को P से) और इसके विपरीत करके प्राप्त किया जाता है।
3. द्वैत: एक प्रमेय दिया गया A, इसकी दोहरा कथन कथन A*, जो ∧ को ∨ से, G को F से, और H को P से धारणा प्राप्त की जाती है।

विधेय लॉजिक के लिए अनुवाद

बर्गेस टीएल में बयानों से एक मुक्त चर के साथ प्रथम-क्रम लॉजिक में बयानों में मेरेडिथ अनुवाद देता है x₀ (वर्तमान क्षण का प्रतिनिधित्व)। यह अनुवाद M को पुनरावर्ती रूप से निम्नानुसार परिभाषित किया गया है:

${\begin{aligned}&M(a)&&=a^{*}x_{0}\\&M(\lnot \phi )&&=\lnot M(\phi )\\&M(\phi \land \psi )&&=M(\phi )\land M(\psi )\\&M({\mathsf {G}}\phi )&&=\forall x_{1}(x_{0}<x_{1}\rightarrow M(A^{+}))\\&M({\mathsf {H}}\phi )&&=\forall x_{1}(x_{1}<x_{0}\rightarrow M(A^{+}))\end{aligned}}$

जहाँ $A^{+}$ वाक्य है $A$ सभी चर सूचकांकों के साथ 1 और की वृद्धि हुई $a^{*}$ द्वारा परिभाषित एक स्थान का विधेय है $x\mapsto V(a,x)$.

टेम्पोरल ऑपरेटर्स

टेम्पोरल लॉजिक में दो प्रकार के ऑपरेटर होते हैं: तार्किक ऑपरेटर और मोडल ऑपरेटर। लॉजिकल ऑपरेटर सामान्य सत्य-कार्यात्मक ऑपरेटर होते हैं ($\neg ,\lor ,\land ,\rightarrow$). लीनियर टेम्पोरल लॉजिक और कम्प्यूटेशन ट्री लॉजिक में उपयोग किए जाने वाले मोडल ऑपरेटर्स को निम्नानुसार परिभाषित किया गया है।

शाब्दिक	प्रतीकात्मक	परिभाषा	व्याख्या	आरेख
बाइनरी ऑपरेटर्स
φ U ψ	$\phi ~{\mathcal {U}}~\psi$	$(B\,{\mathcal {U}}\,C)(\phi )=\ (\exists i:C(\phi _{i})\land (\forall j<i:B(\phi _{j})))$	तब तक (Untill): ψ वर्तमान या भविष्य की स्थिति पर कायम रहता है, और φ को उस स्थिति तक बने रहना होता है। उस स्थिति में φ को और अधिक धारण करने की आवश्यकता नहीं है।	<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>
φ R ψ	$\phi ~{\mathcal {R}}~\psi$	$(B\,{\mathcal {R}}\,C)(\phi )=\ (\forall i:C(\phi _{i})\lor (\exists j<i:B(\phi _{j})))$	R elease: φ ψ जारी करता है यदि ψ सत्य है और इसमें पहली स्थिति सम्मिलित है जिसमें φ सत्य है (या हमेशा के लिए यदि ऐसी स्थिति सम्मिलित नहीं है)।	<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>
यूनरी ऑपरेटर्स
N φ	$\bigcirc \phi$	${\mathcal {N}}B(\phi _{i})=B(\phi _{i+1})$	N ext: φ को अगले राज्य में रखना है। ( एक्स समानार्थक रूप से प्रयोग किया जाता है।)	<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 φ	$\Diamond \phi$	${\mathcal {F}}B(\phi )=(true\,{\mathcal {U}}\,B)(\phi )$	Future : φ को अंततः पकड़ना होगा (कहीं बाद के रास्ते पर)।	<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 φ	$\Box \phi$	${\mathcal {G}}B(\phi )=\neg {\mathcal {F}}\neg B(\phi )$	Globally: φ को बाद के पूरे रास्ते पर पकड़ बनानी है।	<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 φ	$\forall \phi$	$({\mathcal {A}}B)(\psi )=\ (\forall \phi :\phi _{0}=\psi \to B(\phi ))$	All: φ को वर्तमान स्थिति से प्रांरम्भ होने वाले सभी पथों पर पकड़ बनाना है।
E φ	$\exists \phi$	$({\mathcal {E}}B)(\psi )=\ (\exists \phi :\phi _{0}=\psi \land B(\phi ))$	Exists: वर्तमान स्थिति से प्रारम्भ होने वाला कम से कम एक पथ सम्मिलित है जहां φ धारण करता है।

वैकल्पिक प्रतीक:

• ऑपरेटर R को कभी-कभी V द्वारा निरूपित किया जाता है
• ऑपरेटर W तक कमजोर ऑपरेटर है: $f\mathbf {W} g$ के बराबर है $f\mathbf {U} g\lor \mathbf {G} f$

यूनरी ऑपरेटर जब भी अच्छी तरह से बने सूत्र होते हैं B(φ) सुगठित है। जब भी बाइनरी ऑपरेटर अच्छी तरह से गठित सूत्र होते हैं B(φ) और C(φ) सुगठित हैं।

कुछ लॉजिक्स में, कुछ ऑपरेटरों को व्यक्त नहीं किया जा सकता है। उदाहरण के लिए, एन ऑपरेटर को क्रियाओं के अस्थायी लॉजिक में व्यक्त नहीं किया जा सकता है।

टेम्पोरल लॉजिक्स

टेम्पोरल लॉजिक्स में सम्मिलित हैं:

• स्थितीय लॉजिक की कुछ प्रणालियाँ
• लीनियर टेम्पोरल लॉजिक (एलटीएल अंतराल टेम्पोरल लॉजिक बिना ब्रांचिंग टाइमलाइन के
• कम्प्यूटेशन ट्री लॉजिक (सीटीएल) टेम्पोरल लॉजिक ब्रांचिंग टाइमलाइन के साथ
• अंतराल अस्थायी लॉजिक (आईटीएल)
• कार्यों का अस्थायी लॉजिक (टीएलए)
• सिग्नल टेम्पोरल लॉजिक (एसटीएल)* टाइमस्टैम्प अस्थायी लॉजिक (टीटीएल)
• संपत्ति विशिष्टता भाषा (पीएसएल)
• सीटीएल*, जो एलटीएल और सीटीएल का सामान्यीकरण करता है
• हेनेसी-मिलनर लॉजिक (एचएमएल)
• मोडल μ-कैलकुलस, जिसमें एक सबसेट एचएमएल और सीटीएल के रूप में सम्मिलित है*
• मीट्रिक टेम्पोरल लॉजिक (एमटीएल)
• मीट्रिक अंतराल टेम्पोरल लॉजिक (एमआईटीएल)
• समयबद्ध प्रस्तावपरक टेम्पोरल लॉजिक (टीपीटीएल)
• ट्रंकेटेड लीनियर टेम्पोरल लॉजिक (टीएलटीएल)
• हाइपर टेम्पोरल लॉजिक (हाइपरएलटीएल)

लौकिक या कालानुक्रमिक या काल लॉजिक से निकटता से संबंधित भिन्नता, टोपोलॉजी, स्थान या स्थानिक स्थिति पर आधारित मोडल लॉजिक्स हैं।

यह भी देखें

• एचपीओ औपचारिकता
• कृपके संरचना
• ऑटोमेटा सिद्धांत
• चॉम्स्की व्याकरण
• राज्य संक्रमण प्रणाली
• अवधि कलन (डीसी)
• हाइब्रिड लॉजिक
• परिमित-राज्य सत्यापन में अस्थायी लॉजिक
• Reo समन्वय भाषा
• मोडल लॉजिक
• अनुसंधान सामग्री: मैक्स प्लैंक सोसायटी आर्काइव

संदर्भ

• Mordechai Ben-Ari, Zohar Manna, Amir Pnueli: The Temporal Logic of Branching Time. POPL 1981: 164–176
• Amir Pnueli: The Temporal Logic of Programs FOCS 1977: 46–57
• Venema, Yde, 2001, "Temporal Logic," in Goble, Lou, ed., The Blackwell Guide to Philosophical Logic. Blackwell.
• E. A. Emerson and Chin-Laung Lei, "Modalities for model checking: branching time logic strikes back", in Science of Computer Programming 8, pp. 275–306, 1987.
• E. A. Emerson, "Temporal and modal logic", Handbook of Theoretical Computer Science, Chapter 16, the MIT Press, 1990
• A Practical Introduction to PSL, Cindy Eisner, Dana Fisman
• Vardi, Moshe Y. (2008). "From Church and Prior to PSL". In Orna Grumberg; Helmut Veith (eds.). 25 years of model checking: history, achievements, perspectives. Springer. ISBN 978-3-540-69849-4. preprint. Historical perspective on how seemingly disparate ideas came together in computer science and engineering. (The mention of Church in the title of this paper is a reference to a little-known 1957 paper, in which Church proposed a way to perform hardware verification.)

अग्रिम पठन

• Peter Øhrstrøm; Per F. V. Hasle (1995). Temporal logic: from ancient ideas to artificial intelligence. Springer. ISBN 978-0-7923-3586-3.

बाहरी संबंध

• Stanford Encyclopedia of Philosophy: "Temporal Logic"—by Anthony Galton.
• Temporal Logic by Yde Venema, formal description of syntax and semantics, questions of axiomatization. Treating also Kamp's dyadic temporal operators (since, until)
• Notes on games in temporal logic by Ian Hodkinson, including a formal description of first-order temporal logic
• CADP – provides generic model checkers for various temporal logic
• PAT is a powerful free model checker, LTL checker, simulator and refinement checker for CSP and its extensions (with shared variable, arrays, wide range of fairness).