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

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

CTL को पहली बार 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$. CTL एक सिस्टम की अवस्थाओं के बारे में बयान देने के लिए अपने बिल्डिंग ब्लॉक्स के रूप में फर्स्ट-ऑर्डर लॉजिक#शब्दावली का उपयोग करता है। इन प्रस्तावों को फिर तार्किक संचालकों और लौकिक लॉजिक्स का उपयोग करके सूत्रों में संयोजित किया जाता है।

ऑपरेटरों

तार्किक ऑपरेटर

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

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

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

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

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

ऑपरेटरों का न्यूनतम सेट

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

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

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

== सीटीएल == के शब्दार्थ

परिभाषा

संक्रमण प्रणाली पर CTL सूत्रों की व्याख्या की जाती है। एक संक्रमण प्रणाली एक ट्रिपल है ${\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) ).

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

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

कंप्यूटेशन ट्री लॉजिक (CTL) और लीनियर टेम्पोरल लॉजिक (LTL) दोनों ही CTL* के सबसेट हैं। सीटीएल और रैखिक लौकिक तर्क समतुल्य नहीं हैं और उनके पास एक सामान्य उपसमुच्चय है, जो सीटीएल और एलटीएल दोनों का उचित उपसमुच्चय है।

• FG.P LTL में मौजूद है लेकिन CTL में नहीं है।
• AG(P⇒((EX.Q)∧(EX¬Q))) और AG.EF.P CTL में मौजूद हैं लेकिन LTL में नहीं।

एक्सटेंशन

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

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

QBF सॉल्वरों का लाभ उठाने के लिए, संरचना शब्दार्थ के साथ QCTL की मॉडल-जाँच समस्या से 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 CTL