संगणना वृक्ष तर्क

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

कंप्यूटेशन (संगणना) ट्री तर्क को पहली बार 1981 में एडमंड एम क्लार्क और ई एलन एमर्सन द्वारा प्रस्तावित किया गया था, जिन्होंने इसका उपयोग तथाकथित समकालन रूपरेखा, अर्थात् समवर्ती प्रोग्राम के अमूर्तन को संश्लेषित करने के लिए किया था।

संगणना ट्री तर्क का सिंटेक्स

संगणना ट्री तर्क के लिए सुगठित सूत्रों की भाषा निम्नलिखित संदर्भ-मुक्त व्याकरण द्वारा उत्पन्न होती है:

${\begin{aligned}\phi &::=\bot \mid \top \mid p\mid (\neg \phi )\mid (\phi \land \phi )\mid (\phi \lor \phi )\mid (\phi \Rightarrow \phi )\mid (\phi \Leftrightarrow \phi )\\&\mid \quad {\mbox{AX }}\phi \mid {\mbox{EX }}\phi \mid {\mbox{AF }}\phi \mid {\mbox{EF }}\phi \mid {\mbox{AG }}\phi \mid {\mbox{EG }}\phi \mid {\mbox{A }}[\phi {\mbox{ U }}\phi ]\mid {\mbox{E }}[\phi {\mbox{ U }}\phi ]\end{aligned}}$

जहाँ $p$ परमाणु सूत्र के समुच्चय पर स्थित है। सभी संकारकों का उपयोग करना आवश्यक नहीं है – उदाहरण के लिए,$\{\neg ,\land ,{\mbox{AX}},{\mbox{AU}},{\mbox{EU}}\}$ संकारकों का पूरा समुच्चय सम्मिलित है, और अन्य को उनका उपयोग करके परिभाषित किया जा सकता है।

• ${\mbox{A}}$ का अर्थ है 'सभी पथों के साथ' (अनिवार्य रूप से)
• ${\mbox{E}}$ का अर्थ है 'कम से कम (वहाँ सम्मिलित है) पथ' (संभवतः)

उदाहरण के लिए, निम्नलिखित एक अच्छी तरह से निर्मित संगणना ट्री तर्क सूत्र है:

${\mbox{EF }}({\mbox{EG }}p\Rightarrow {\mbox{AF }}r)$

निम्नलिखित एक अच्छी तरह से निर्मित संगणना ट्री तर्क सूत्र नहीं है:

${\mbox{EF }}{\big (}r{\mbox{ U }}q{\big )}$

इस शृंखला के साथ समस्या यह है कि $U$ तभी हो सकता है $A$ या जब $E$ के साथ जोड़ा जाता है।

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

संक्रियक

तार्किक संक्रियक

तार्किक संकारक सामान्य : ¬, ∨, ∧, ⇒ और ⇔ हैं। इन संक्रियाओ के साथ संगणना ट्री तर्क सूत्र भी बूलियन स्थिरांक सत्य और असत्य (तर्क) का उपयोग कर सकते हैं।

टेम्पोरल (अस्थायी) संक्रियक

अस्थायी संचालक निम्नलिखित हैं:

• पथों पर परिमाणक
  • A Φ – सभी: Φ को वर्तमान स्थिति से प्रारंभ होने वाले सभी पथों पर प्रग्रहण करना होगा।
  • E Φ – सम्मिलित : वर्तमान स्थिति से प्रारंभ होने वाला कम से कम एक पथ सम्मिलित है जहां Φ धारण करता है।
• पथ-विशिष्ट परिमाणक
  • X φ – फिर: φ को अगली स्थिति में प्रग्रहण करना होगा (इस संक्रिया को कभी-कभी X के अतिरिक्त N उल्लेख किया जाता है)।
  • G φ – विश्व स्तर पर: φ को बाद के पूरे पथ पर प्रग्रहण करना होगा।
  • F φ – अंत में: φ को अंततः (बाद के पथ पर कहीं) प्रग्रहण होगा।
  • φ U ψ – जब तक: φ को कम से कम तब तक प्रग्रहण करना है जब तक कि किसी स्थान पर ψ प्रग्रहण न कर ले। इसका तात्पर्य है कि ψ भविष्य में सत्यापित किया जाएगा।
  • φ W ψ – जब तक दुर्बल: φ को तब तक प्रग्रहण करना होगा जब तक ψ प्रग्रहण न करे। U के साथ अंतर यह है कि इस बात की कोई गारंटी (प्रत्याभूति) नहीं है कि 'ψ को कभी सत्यापित किया जाएगा। W संक्रिया को कभी-कभी अतिरिक्त कहा जाता है।

संगणना ट्री तर्क* में, अस्थायी संक्रिया को स्वतंत्र रूप से मिश्रित किया जा सकता है। संगणना ट्री तर्क में, संक्रिया को सदैव दो में समूहीकृत किया जाना चाहिए: पथ संक्रिया के बाद एक स्थिति संक्रिया मे किया जाना चाहिए। नीचे दिए गए उदाहरण देखें। संगणना ट्री तर्क * संगणना ट्री तर्क की तुलना में कठिनता से अधिक अभिव्यंजक है।

संक्रियाओ का न्यूनतम समुच्चय

संगणना ट्री तर्क में संक्रियाओ के न्यूनतम समुच्चय होते हैं। केवल उन संक्रियाओ का उपयोग करने के लिए सभी संगणना ट्री तर्क सूत्रों को रूपांतरित किया जा सकता है। यह मॉडल जाँच में उपयोगी है। संक्रियाओ का एक न्यूनतम समुच्चय : {true, ∨, ¬, EG, EU, EX} है।

अस्थायी संक्रियाओ के लिए उपयोग किए जाने वाले कुछ परिवर्तन हैं:

• EFφ == E[trueU(φ)] (क्योंकि Fφ == [trueU(φ)] )
• AXφ == ¬EX(¬φ)
• AGφ == ¬EF(¬φ) == ¬ ई[trueU(¬φ)]
• AFφ == A[trueUφ] == ¬EG(¬φ)
• A[φUψ] == ¬( ई[(¬ψ)U¬(φ∨ψ)] ∨ EG(¬' 'ψ))

परिभाषा

संक्रमण प्रणाली पर संगणना ट्री तर्क सूत्रों की व्याख्या की जाती है। एक संक्रमण प्रणाली त्रिपक्षीय ${\mathcal {M}}=(S,{\rightarrow },L)$ है, जहाँ $S$ स्थितियों का समुच्चय है, ${\rightarrow }\subseteq S\times S$ संक्रमण संबंध है, जिसे क्रमिक माना जाता है, अर्थात प्रत्येक स्थिति का कम से कम एक आनुक्रमिक होता है, और $L$ एक लेबलिंग फ़ंक्शन है, जो स्थितिओ को प्रस्ताव पत्र प्रदान करता है। मान लीजिए ${\mathcal {M}}=(S,\rightarrow ,L)$ ऐसा संक्रमण मॉडल है

$s\in S,\phi \in F$ साथ जहां F की भाषा पर अच्छी तरह से गठित सूत्र ${\mathcal {M}}$ का समुच्चय है

फिर सिमेंटिक एंटेलमेंट (घटाव) $({\mathcal {M}},s\models \phi )$ के संबंध को $\phi$ पर पुनरावर्ती रूप से परिभाषित किया गया है :

1. ${\Big (}({\mathcal {M}},s)\models \top {\Big )}\land {\Big (}({\mathcal {M}},s)\not \models \bot {\Big )}$
2. ${\Big (}({\mathcal {M}},s)\models p{\Big )}\Leftrightarrow {\Big (}p\in L(s){\Big )}$
3. ${\Big (}({\mathcal {M}},s)\models \neg \phi {\Big )}\Leftrightarrow {\Big (}({\mathcal {M}},s)\not \models \phi {\Big )}$
4. ${\Big (}({\mathcal {M}},s)\models \phi _{1}\land \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s)\models \phi _{1}{\big )}\land {\big (}({\mathcal {M}},s)\models \phi _{2}{\big )}{\Big )}$
5. ${\Big (}({\mathcal {M}},s)\models \phi _{1}\lor \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s)\models \phi _{1}{\big )}\lor {\big (}({\mathcal {M}},s)\models \phi _{2}{\big )}{\Big )}$
6. ${\Big (}({\mathcal {M}},s)\models \phi _{1}\Rightarrow \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s)\not \models \phi _{1}{\big )}\lor {\big (}({\mathcal {M}},s)\models \phi _{2}{\big )}{\Big )}$
7. ${\bigg (}({\mathcal {M}},s)\models \phi _{1}\Leftrightarrow \phi _{2}{\bigg )}\Leftrightarrow {\bigg (}{\Big (}{\big (}({\mathcal {M}},s)\models \phi _{1}{\big )}\land {\big (}({\mathcal {M}},s)\models \phi _{2}{\big )}{\Big )}\lor {\Big (}\neg {\big (}({\mathcal {M}},s)\models \phi _{1}{\big )}\land \neg {\big (}({\mathcal {M}},s)\models \phi _{2}{\big )}{\Big )}{\bigg )}$
8. ${\Big (}({\mathcal {M}},s)\models AX\phi {\Big )}\Leftrightarrow {\Big (}\forall \langle s\rightarrow s_{1}\rangle {\big (}({\mathcal {M}},s_{1})\models \phi {\big )}{\Big )}$
9. ${\Big (}({\mathcal {M}},s)\models EX\phi {\Big )}\Leftrightarrow {\Big (}\exists \langle s\rightarrow s_{1}\rangle {\big (}({\mathcal {M}},s_{1})\models \phi {\big )}{\Big )}$
10. ${\Big (}({\mathcal {M}},s)\models AG\phi {\Big )}\Leftrightarrow {\Big (}\forall \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\forall i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}$
11. ${\Big (}({\mathcal {M}},s)\models EG\phi {\Big )}\Leftrightarrow {\Big (}\exists \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\forall i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}$
12. ${\Big (}({\mathcal {M}},s)\models AF\phi {\Big )}\Leftrightarrow {\Big (}\forall \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}$
13. ${\Big (}({\mathcal {M}},s)\models EF\phi {\Big )}\Leftrightarrow {\Big (}\exists \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}$
14. ${\bigg (}({\mathcal {M}},s)\models A[\phi _{1}U\phi _{2}]{\bigg )}\Leftrightarrow {\bigg (}\forall \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\Big (}{\big (}({\mathcal {M}},s_{i})\models \phi _{2}{\big )}\land {\big (}\forall (j<i)({\mathcal {M}},s_{j})\models \phi _{1}{\big )}{\Big )}{\bigg )}$
15. ${\bigg (}({\mathcal {M}},s)\models E[\phi _{1}U\phi _{2}]{\bigg )}\Leftrightarrow {\bigg (}\exists \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\Big (}{\big (}({\mathcal {M}},s_{i})\models \phi _{2}{\big )}\land {\big (}\forall (j<i)({\mathcal {M}},s_{j})\models \phi _{1}{\big )}{\Big )}{\bigg )}$

संगणना ट्री तर्क की विशेषता

उपरोक्त नियम 10-15 मॉडल में संगणना पथों को संदर्भित करते हैं और अंततः ''कम्प्यूटेशन ट्री'' की विशेषता हैं; वे दिए गए स्थिति $s$ में अधिकतम रूप से गहन गणना ट्री की प्रकृति के बारे में दावा कर रहे हैं।

सिमेंटिक समकक्ष

सूत्र $\phi$ और $\psi$ सिमेंटिक के समतुल्य कहा जाता है यदि किसी मॉडल में कोई स्थिति जो एक को पूरा करता है वह दूसरे को भी पूरा करता है। इसे $\phi \equiv \psi$ निरूपित है।

यह देखा जा सकता है कि A और E दोहरे हैं, क्रमशः सार्वभौमिक और अस्तित्वगत संगणना पथ परिमाणक हैं:

$\neg A\Phi \equiv E\neg \Phi$.

इसके अतिरिक्त, G और F भी हैं।

इसलिए संगणना ट्री तर्क में डी मॉर्गन के नियमों का इंस्टेंस तैयार किया जा सकता है:

$\neg AF\phi \equiv EG\neg \phi$

$\neg EF\phi \equiv AG\neg \phi$

$\neg AX\phi \equiv EX\neg \phi$

ऐसी पहचानों का उपयोग करके यह दिखाया जा सकता है कि संगणना ट्री तर्क अस्थायी संकारकों का एक उपसमुच्चय पर्याप्त है यदि इसमें $EU$ सम्मिलित है, कम से कम एक $\{AX,EX\}$ और कम से कम एक $\{EG,AF,AU\}$ और बूलियन संकारक है।

नीचे दी गई महत्वपूर्ण तुल्यताओं को विस्तार नियम कहा जाता है; वे समय में अपने आनुक्रमिक के प्रति संगणना ट्री तर्क संयोजन के सत्यापन को प्रकट करने की स्वीकृति देते हैं।

$AG\phi \equiv \phi \land AXAG\phi$

$EG\phi \equiv \phi \land EXEG\phi$

$AF\phi \equiv \phi \lor AXAF\phi$

$EF\phi \equiv \phi \lor EXEF\phi$

$A[\phi U\psi ]\equiv \psi \lor (\phi \land AXA[\phi U\psi ])$

$E[\phi U\psi ]\equiv \psi \lor (\phi \land EXE[\phi U\psi ])$

उदाहरण

मान लीजिए P का अर्थ है कि मुझे चॉकलेट पसंद है और Q का अर्थ है कि बाहर गर्मी है।

• AG.P

"मैं अब से चॉकलेट पसंद करूंगा, चाहे कुछ भी हो जाए।

• EF.P

"यह संभव है कि मुझे कम से कम एक दिन के लिए चॉकलेट पसंद हो।"

• AF.EG.P

"यह सदैव संभव है (AF) कि मैं एकाएक शेष समय के लिए चॉकलेट पसंद करना प्रारंभ कर दूंगा।" (ध्यान दें: न केवल मेरे शेष जीवन, क्योंकि मेरा जीवन सीमित है, जबकि G अनंत है)।

• EG.AF.P

भविष्य में क्या होता है (E) के आधार पर, यह संभव है कि बाकी समय (G) के लिए, मुझे कम से कम एक (AF) चॉकलेट पसंद करने वाला दिन अभी भी मुझसे आगे की प्रत्याभूति दी जाएगी। हालाँकि, यदि कभी कुछ गलत हो जाता है, तो सभी शर्त बंद हो जाते हैं और इस बात की कोई प्रत्याभूति नहीं है कि मुझे कभी चॉकलेट पसंद आएगी या नहीं।

निम्नलिखित दो उदाहरण संगणना ट्री तर्क और संगणना ट्री तर्क* के बीच अंतर दिखाते हैं, क्योंकि वे जब तक संक्रिया को किसी भी पथ संक्रिया (A या E) के साथ योग्य नहीं होने की स्वीकृति देते हैं:

• AG(PUQ)

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

• EF((EX.P)U(AG.Q))

"यह संभव है कि: अंततः ऐसा समय आएगा जब यह सदैव के लिए गर्म हो जाएगा (AG.Q) और उस समय से पहले मुझे अगले दिन (EX.P) चॉकलेट पसंद करने का सदैव कोई तरीका होगा।"

अन्य तर्क के साथ संबंध

संगणना ट्री तर्क (सीटीएल) का एक उपसमुच्चय है और साथ ही मॉडल μ गणना है। संगणना ट्री तर्क एलुर, हेनजिंगर और कुफरमैन के प्रत्यावर्ती समय अस्थायी तर्क (एटीएल) का भी एक अंश है।

संगणना ट्री तर्क (सीटीएल) और रैखिक अस्थायी तर्क (एलटीएल) दोनों ही संगणना ट्री तर्क* के उपसमुच्चय हैं। संगणना ट्री तर्क और रैखिक अस्थायी तर्क समतुल्य नहीं हैं और उनके पास एक सामान्य उपसमुच्चय है, जो संगणना ट्री तर्क और रैखिक अस्थायी तर्क दोनों का उपयुक्त उपसमुच्चय है।

• FG.P रैखिक अस्थायी तर्क में सम्मिलित है लेकिन संगणना ट्री तर्क में नहीं है।
• AG(P⇒((EX.Q)∧(EX¬Q))) और AG.EF.P संगणना ट्री तर्क में सम्मिलित हैं लेकिन रैखिक अस्थायी तर्क में नहीं है।

एक्सटेंशन

संगणना ट्री तर्क को दूसरे क्रम के परिमाणीकरण $\exists p$ और $\forall p$ परिमाणित संगणना ट्री तर्क (क्यूसीटीएल) के लिए के साथ बढ़ाया गया है इसमे दो सिमेंटिक हैं:

• ट्री सिमेंटिक्स हम कंप्यूटेशन ट्री के नोड्स को लेबल करते हैं। QCTL* = QCTL = MSO पर ट्री है। मॉडल की जाँच और संतुष्ट टॉवर पूर्ण हैं।
• संरचना सिमेंटिक हम स्थितिओ को लेबल करते हैं। QCTL* = QCTL = MSO पर ग्राफ (असतत गणित) है। मॉडल की जाँच पीएसपीएसीई-पूर्ण है लेकिन संतुष्टि अनिर्णायक है।

परिमाणित बूलियन सूत्र समाधानकर्ता का लाभ उठाने के लिए, संरचना सिमेंटिक के साथ परिमाणित संगणना ट्री तर्क की मॉडल-जाँच समस्या से टीक्यूबीएफ (सत्य परिमाणित बूलियन सूत्र) तक लघुकरण प्रस्तावित की गई है।

यह भी देखें

• संभाव्य संगणना ट्री तर्क

• निष्पक्ष कम्प्यूटेशनल ट्री तर्क

• रैखिक अस्थायी तर्क

संदर्भ

• E.M. Clarke; E.A. Emerson (1981). "Design and synthesis of synchronisation skeletons using branching time temporal logic" (PDF). Logic of Programs, Proceedings of Workshop, Lecture Notes in Computer Science. Springer, Berlin. 131: 52–71.
• Michael Huth; Mark Ryan (2004). Logic in Computer Science (Second Edition). Cambridge University Press. p. 207. ISBN 978-0-521-54310-1.
• Emerson, E. A.; Halpern, J. Y. (1985). "Decision procedures and expressiveness in the temporal logic of branching time". Journal of Computer and System Sciences. 30 (1): 1–24. doi:10.1016/0022-0000(85)90001-7.
• Clarke, E. M.; Emerson, E. A. & Sistla, A. P. (1986). "Automatic verification of finite-state concurrent systems using temporal logic specifications". ACM Transactions on Programming Languages and Systems. 8 (2): 244–263. doi:10.1145/5397.5399.
• Emerson, E. A. (1990). "Temporal and modal logic". In Jan van Leeuwen (ed.). Handbook of Theoretical Computer Science, vol. B. MIT Press. pp. 955–1072. ISBN 978-0-262-22039-2.

बाहरी संबंध

• Teaching slides of संगणना ट्री तर्क