रैखिक लौकिक तर्क

तर्क में, रैखिक अस्थायी तर्क या रैखिक-समय अस्थायी तर्क (लीनियर-टाइम टेम्पोरल लॉजिक) [1] [2] (एलटीएल) समय के संदर्भ में तौर-तरीकों के साथ एक सामान्य लौकिक तर्क है। एलटीएल (LTL) में, पथों के भविष्य के बारे में सूत्रों को एनकोड कर सकते हैं, उदाहरण के लिए, एक शर्त अंततः सत्य होगी, एक शर्त तब तक सत्य होगी जब तक कि कोई अन्य तथ्य सत्य न हो जाए, आदि। यह अधिक जटिल सीटीएल* का एक टुकड़ा है, जो अतिरिक्त रूप से शाखाओं में बंटने की अनुमति देता है समय और परिमाणक। एलटीएल को कभी-कभी प्रोपोज़िशनल टेम्पोरल लॉजिक कहा जाता है, संक्षिप्त रूप में पीटीएल। [3] अभिव्यंजक शक्ति के संदर्भ में, लीनियर टेम्पोरल लॉजिक (एलटीएल) प्रथम-क्रम तर्क का एक टुकड़ा है। [4] [5]

एलटीएल को पहली बार 1977 में आमिर पनुएली द्वारा कंप्यूटर प्रोग्राम के औपचारिक सत्यापन के लिए प्रस्तावित किया गया था। [6]

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

अभिव्यंजक शक्ति (कंप्यूटर विज्ञान) के संदर्भ में, रैखिक टेम्पोरल लॉजिक (एलटीएल) प्रथम-क्रम तर्क का टुकड़ा है। एलटीएल को पहली बार 1977 में आमिर पनुएली द्वारा कंप्यूटर प्रोग्राम के औपचारिक सत्यापन के लिए प्रस्तावित किया गया था।

सिंटेक्स

एलटीएल प्रस्तावात्मक चर एपी, तार्किक संयोजी ¬ और ∨, और टेम्पोरल लॉजिक मोडल ऑपरेटरों 'X' (कुछ साहित्य 'O' या 'N' का उपयोग करता है) और 'यू' के एक सीमित सेट से बनाया गया है। औपचारिक रूप से, एपी पर एलटीएल सूत्रों का सेट निम्नानुसार परिभाषित किया गया है:

• यदि p ∈ AP तो p एक एलटीएल सूत्र है;
• यदि ψ और φ एलटीएल सूत्र हैं तो ¬ψ, φ ∨ ψ, 'X' ψ, और φ 'U' ψ एलटीएल सूत्र हैं।

X को ne x t के रूप में पढ़ा जाता है और U को तब तक पढ़ा जाता है।

इन मौलिक ऑपरेटरों के अलावा, एलटीएल सूत्रों को संक्षिप्त रूप से लिखने के लिए मौलिक ऑपरेटरों के संदर्भ में परिभाषित अतिरिक्त तार्किक और अस्थायी ऑपरेटर हैं। अतिरिक्त तार्किक संकारक ∧, →, ↔, सत्य और असत्य हैं।

निम्नलिखित अतिरिक्त टेम्पोरल ऑपरेटर हैं।

• G हमेशा के लिए (विश्व स्तर पर)
• F अंत में
• रिलीज के लिए R
• जब तक कमजोर के लिए W
• शक्तिशाली रिलीज के लिए M

शब्दार्थ

एपी में चर के सत्य मूल्यांकन के अनंत अनुक्रम द्वारा एक एलटीएल फॉर्मूला संतोषजनक हो सकता है। इन अनुक्रमों को क्रिप्के संरचना के पथ पर एक शब्द के रूप में देखा जा सकता है (वर्णमाला 2^AP पर एक ω-शब्द )। मान लीजिए w = a ₀ ,a ₁ ,a ₂ ,... ऐसा ω-शब्द है। मान लीजिए w ( i ) = a _i । चलो w ⁱ = a _i , a _{i +1} ,..., जो w का एक प्रत्यय है. औपचारिक रूप से, एक शब्द और एलटीएल सूत्र के बीच संतुष्टि संबंध ⊨ को निम्नानुसार परिभाषित किया गया है:

• w ⊨ p अगर p ∈ w(0)
• w ⊨ ¬ψ अगर डब्ल्यू ⊭ ψ
• ⊨ में φ ∨ ψ अगर w ⊨ φ या w ⊨ ψ
• w ⊨ 'X' ψ अगर w¹ ⊨ ψ (अगली बार चरण में ψ सच होना चाहिए)
• व ⊨ φ U ψ अगर वहाँ मौजूद है i ≥ 0 ऐसा है कि w ⁱ⊨ ψ और सभी के लिए 0 ≤ k < i, w^{k ⊨ φ (φ तक सत्य रहना चाहिए ψ सच हो जाता है)}

हम कहते हैं कि एक ω-शब्द w एक एलटीएल सूत्र को संतुष्ट करता है ψ जब डब्ल्यू ⊨ ψ.

ω-भाषा एल (ψ) द्वारा परिभाषित ψ है {डब्ल्यू | डब्ल्यू ⊨ ψ}, जो संतुष्ट करने वाले ω-शब्दों का समुच्चय है ψ.

एक सूत्र ψ संतोषजनक है अगर वहाँ एक ω-शब्द w मौजूद है जैसे कि w ⊨ ψ. एक सूत्र ψ मान्य है यदि प्रत्येक ω-शब्द w के लिए वर्णमाला 2^AP, हमारे पास w ⊨ है ψ.

अतिरिक्त तार्किक ऑपरेटरों को निम्नानुसार परिभाषित किया गया है:

• φ ∧ ψ ≡ ¬(¬φ ∨ ¬ψ)
• φ → ψ ≡ ¬φ ∨ ψ
• φ ↔ ψ ≡ (φ → ψ) ∧ ( ψ → φ)
• ट्रू ≡ p ∨ ¬p, जहां p ∈ AP
• फॉल्स ≡ ¬ट्रू

अतिरिक्त टेम्पोरल ऑपरेटर्स R, F और G को निम्नानुसार परिभाषित किया गया है:

• ψ R φ ≡ ¬(¬ψ ¬ मेंφ) ( φ एक बार सहित और तब तक ट्रू रहता है ψ ट्रू हो जाता है। अगर ψ कभी ट्रू नहीं होता, φ हमेशा के लिए सच रहना चाहिए। ψ जारी करता है φ.)
• F ψ ≡ ट्रू U ψ (अंततः ψ ट्रू हो जाता है)
• G ψ ≡ फॉल्स R ψ ≡ ¬F ¬ψ (ψ हमेशा ट्रू रहता है)

तब तक कमजोर और मजबूत रिलीज

कुछ लेखक भी एक कमजोर जब तक बाइनरी ऑपरेटर को परिभाषित करते हैं, जिसे 'w' के रूप में परिभाषित किया जाता है, सिमेंटिक के साथ जब तक ऑपरेटर के समान होता है, लेकिन स्टॉप की स्थिति होने की आवश्यकता नहीं होती है (रिलीज के समान)। यह कभी-कभी उपयोगी होता है क्योंकि U और R दोनों को कमजोर के रूप में परिभाषित किया जा सकता है:

• ψ W φ ≡ (ψ U φ) ∨ G ψ ≡ ψ U (φ ∨ G ψ) ≡ φ आर (φ ∨ ψ)
• ψ U φ ≡ Fφ ∧ (ψ W φ)
• ψ आर φ ≡ φ W (φ ∧ ψ)

'मजबूत रिलीज' बाइनरी ऑपरेटर, एम निरूपित, जब तक कमजोर का दोहरा है। इसे जब तक ऑपरेटर के समान परिभाषित किया जाता है, ताकि रिलीज की स्थिति को किसी बिंदु पर रोकना पड़े। इसलिए, यह रिलीज़ ऑपरेटर से अधिक मजबूत है।

• ψ M φ ≡ ¬(¬ψ W ¬φ) ≡ (ψ R φ) ∧ F ψ ≡ ψ R (φ ∧ F ψ) ≡ φ U (ψ ∧ φ)

लौकिक संचालकों के शब्दार्थ चित्र के रूप में निम्नानुसार प्रस्तुत किए गए हैं।

शाब्दिक	प्रतीकात्मक	व्याख्या	आरेख
यूनरी ऑपरेटर्स :
X φ	$\bigcirc \varphi$	neXt: φ को अगले स्थिति में रखना है।
F φ	$\Diamond \varphi$	Finally: φ अंत में पकड़ है (कहीं बाद के रास्ते पर)।
G φ	$\Box \varphi$	Globally: φ को बाद के पूरे रास्ते पर पकड़ बनानी है।
बाइनरी ऑपरेटर्स :
ψ U φ	$\psi \;{\mathcal {U}}\,\varphi$	Until: ψ को कम से कम φ के सत्य होने तक बनाए रखना चाहिए , जिसे वर्तमान या भविष्य की स्थिति पर बनाए रखना चाहिए।
ψ R φ	$\psi \;{\mathcal {R}}\,\varphi$	Release: φ को तब तक सत्य होना चाहिए जब तक और उस बिंदु को सम्मिलित न कर लें जहां ψ पहले सत्य हो जाता है; यदि ψ कभी सत्य नहीं होता, तो φ को हमेशा सत्य रहना चाहिए।
ψ W φ	$\psi \;{\mathcal {W}}\,\varphi$	Weak until: ψ को कम से कम φ तक पकड़ना होगा ; अगर φ कभी सच नहीं होता, तो ψ को हमेशा के लिए सच रहना चाहिए।
ψ M φ	$\psi \;{\mathcal {M}}\,\varphi$	मजबूत रिलीज: φ को उस बिंदु तक और उस बिंदु तक सत्य होना चाहिए जहां ψ पहले सत्य हो जाता है, जो वर्तमान या भविष्य की स्थिति में होना चाहिए।

समानताएं

φ, ψ, और ρ को एल टी एल सूत्र होने दें। निम्नलिखित तालिकाएँ कुछ उपयोगी तुल्यताओं को सूचीबद्ध करती हैं जो सामान्य लॉजिकल ऑपरेटर्स के बीच मानक तुल्यताओं का विस्तार करती हैं।

Distributivity
X (φ ∨ ψ) ≡ (X φ) ∨ (X ψ)	X (φ ∧ ψ) ≡ (X φ) ∧ (X ψ)	X (φ U ψ)≡ (X φ) U (X ψ)
F (φ ∨ ψ) ≡ (F φ) ∨ (F ψ)	G (φ ∧ ψ) ≡ (G φ) ∧ (G ψ)
ρ U (φ ∨ ψ) ≡ (ρ U φ) ∨ (ρ U ψ)	(φ ∧ ψ) U ρ ≡ (φ U ρ) ∧ (ψ U ρ)

W और M दोहरे हैं
X स्व-द्वैत है	F और G दोहरे हैं	U और R द्दोहरे हैं	W और M दोहरे हैं
¬X φ ≡ X ¬φ	¬F φ ≡ G ¬φ	¬ (φ U ψ) ≡ (¬φ R ¬ψ)	¬ (φ W ψ) ≡ (¬φ M ¬ψ)
	¬G φ ≡ F ¬φ	¬ (φ R ψ) ≡ (¬φ U ¬ψ)	¬ (φ M ψ) ≡ (¬φ W ¬ψ)

विशेष लौकिक गुण
F φ ≡ F F φ	G φ ≡ G G φ	φ U ψ ≡ φ U (φ U ψ)
φ U ψ ≡ ψ ∨ ( φ ∧ X(φ U ψ) )	φ W ψ ≡ ψ ∨ ( φ ∧ X(φ W ψ) )	φ R ψ ≡ ψ ∧ (φ ∨ X(φ R ψ) )
G φ ≡ φ ∧ X(G φ)	F φ ≡ φ ∨ X(F φ)

नकारात्मक सामान्य रूप

एल टी एल के सभी सूत्र नकारात्मक सामान्य रूप में परिवर्तित किए जा सकते हैं, जहाँ

• सभी निषेध केवल परमाणु तर्कवाक्यों के सामने प्रकट होते हैं,
• केवल अन्य तार्किक संकारक 'true', 'false', ∧, और ∨ दिखाई दे सकते हैं, और
• केवल टेम्पोरल ऑपरेटर्स 'X', 'U' और 'R' दिखाई दे सकते हैं।

नकारात्मक प्रसार के लिए उपरोक्त तुल्यताओं का उपयोग करके, सामान्य रूप प्राप्त करना संभव है। यह सामान्य रूप 'R', 'true', 'false', और ∧ को सूत्र में प्रकट होने की अनुमति देता है, जो एल टी एल के मौलिक संचालक नहीं हैं। ध्यान दें कि नकारात्मक सामान्य रूप में परिवर्तन सूत्र की लंबाई को नहीं बढ़ाता है। यह सामान्य रूप Büchi automaton के रैखिक अस्थायी तर्क में उपयोगी है | एल टी एल सूत्र से Büchi automaton में अनुवाद।

अन्य लॉजिक्स के साथ संबंध

एल टी एल को ऑर्डर के ऑर्डर का मोनाडिक फर्स्ट-ऑर्डर लॉजिक दिखाया जा सकता है, FO[<]—एक परिणाम जिसे काम्प के प्रमेय के रूप में जाना जाता है— या समकक्ष रूप से स्टार-मुक्त भाषाओं के लिए। संगणना वृक्ष तर्क (CTL) और लीनियर टेम्पोरल लॉजिक (एल टी एल) दोनों ही CTL* के उपसमुच्चय हैं, लेकिन अतुलनीय हैं। उदाहरण के लिए,

• सीटीएल में कोई सूत्र एलटीएल सूत्र एफ (जी पी) द्वारा परिभाषित भाषा को परिभाषित नहीं कर सकता है।
• एलटीएल में कोई सूत्र उस भाषा को परिभाषित नहीं कर सकता है जिसे सीटीएल सूत्र एजी (पी → (EXq ∧ EX¬q)) या एजी (ईएफ (पी)) द्वारा परिभाषित किया गया है।

कम्प्यूटेशनल समस्याएं

एलटीएल फॉर्मूला के खिलाफ मॉडल जांच और संतुष्टि पीएसपीएसीई-पूर्ण समस्याएं हैं। एल टी एल संश्लेषण और एल टी एल जीतने की स्थिति के विरुद्ध खेलों के सत्यापन की समस्या 2-EXPTIME|2EXPTIME-पूर्ण है।

अनुप्रयोग

ऑटोमेटा-थ्योरिटिक लीनियर टेम्पोरल लॉजिक मॉडल चेकिंग

मॉडल जांच का एक महत्वपूर्ण तरीका एलटीएल ऑपरेटरों का उपयोग करके वांछित गुणों (जैसे ऊपर वर्णित) को व्यक्त करना है और वास्तव में जांच करें कि मॉडल इस संपत्ति को संतुष्ट करता है या नहीं। एक तकनीक बुच्ची ऑटोमेटन प्राप्त करना है जो मॉडल के समतुल्य है (एक ω-शब्द को ठीक से स्वीकार करता है यदि यह मॉडल है) और दूसरा एक जो संपत्ति की अस्वीकृति के बराबर है (एक ω-शब्द को ठीक से स्वीकार करता है यह नकारात्मक को संतुष्ट करता है संपत्ति) (cf. बुची ऑटोमेटन के लिए रैखिक लौकिक तर्क)। दो गैर-नियतात्मक बुची ऑटोमेटा का प्रतिच्छेदन खाली है अगर और केवल अगर मॉडल संपत्ति को संतुष्ट करता है।

औपचारिक सत्यापन में महत्वपूर्ण गुणों को व्यक्त करना

दो मुख्य प्रकार के गुण हैं जिन्हें रैखिक लौकिक तर्क का उपयोग करके व्यक्त किया जा सकता है: सुरक्षा संपत्ति गुण आमतौर पर कहते हैं कि कुछ बुरा कभी नहीं होता (G¬ϕ), जबकि जीवंतता गुण बताते हैं कि कुछ अच्छा होता रहता है (GFψ or G(ϕ →Fψ))। अधिक आम तौर पर, सुरक्षा गुण वे होते हैं जिनके लिए प्रत्येक प्रति उदाहरण में एक परिमित उपसर्ग होता है, हालांकि इसे एक अनंत पथ तक बढ़ाया जाता है, यह अभी भी एक प्रति उदाहरण है। जीवंत गुणों के लिए, दूसरी ओर, प्रत्येक परिमित पथ को अनंत पथ तक बढ़ाया जा सकता है जो सूत्र को संतुष्ट करता है।

विशिष्टता भाषा

रैखिक अस्थायी तर्क के अनुप्रयोगों में से एक वरीयता-आधारित योजना के उद्देश्य के लिए योजना डोमेन परिभाषा भाषा में वरीयताओं का विनिर्देश है।

एक्सटेंशन

पैरामीट्रिक लीनियर टेम्पोरल लॉजिक एल टी एल को टिल-मोडैलिटी पर वेरिएबल्स के साथ एक्सटेंड करता है।

यह भी देखें

• क्रिया भाषा
• मीट्रिक लौकिक तर्क
• सुरक्षा और सजीवता गुण

बाहरी संबंध

• A presentation of एल टी एल
• Linear-Time Temporal Logic and Büchi Automata
• एल टी एल Teaching slides of professor Alessandro Artale at the Free University of Bozen-Bolzano
• एल टी एल to Buchi translation algorithms a genealogy, from the website of Spot a library for model checking.