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

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

संगणना ट्री तर्क को पहली बार 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$ जहां एफ की नियमित भाषा पर अच्छी तरह से गठित सूत्र का समुच्चय है ${\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$ यह देखा जा सकता है कि ए और ई दोहरे हैं, क्रमशः अमूर्तन्वभौमिक और अस्तित्वगत गणना पथ क्वांटिफायर हैं: $\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 का अर्थ है कि बाहर गर्मी है।

• एजी.पी

मुझे अभी से चॉकलेट पसंद आएगी, चाहे कुछ भी हो जाए।

• ईएफ.पी

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

• एएफ.ईजी.पी

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

• ईजी.एएफ.पी

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

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

• एजी (पीयूक्यू)

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

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

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

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

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

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

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

एक्सटेंशन

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

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

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

यह भी देखें

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

निष्पक्ष कम्प्यूटेशनल वृक्ष तर्क तर्क

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

संदर्भ

• 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 संगणना ट्री तर्क