💻 computer science

The Bright Side of Timed Opacity

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

मूल लेखक: Étienne André, Sarah Dépernet, Engel Lefaucheux

प्रकाशित 2026-07-01

📖 6 मिनट में पढ़ें🧠 गहराई से पढ़ें

CC BY 4.0

मूल लेखक: Étienne André, Sarah Dépernet, Engel Lefaucheux

मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। ✨ नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें

कल्पना कीजिए कि एक उच्च-सुरक्षा वाली तिजोरी (एक Timed Automaton) है जहाँ एक विशिष्ट क्षण पर एक गुप्त क्रिया होती है। एक घुसपैठिया (Attacker) बाहर है, जो यह पता लगाने की कोशिश कर रहा है कि क्या वह गुप्त क्रिया हुई थी या नहीं। घुसपैठिया तिजोरी के अंदर नहीं देख सकता, लेकिन वह दरवाजों की "क्लिक" की आवाज़ सुन सकता है और वे क्लिक ठीक कब होती हैं, यह देख सकता है।

यह शोध पत्र, जिसका शीर्षक "The Bright Side of Timed Opacity" है, उस समस्या का समाधान करता है जिसे पहले हल करना असंभव माना जाता था: यह निर्धारित करना कि क्या कोई सिस्टम वास्तव में "ओपेक" (छिपा हुआ) है जब एक हमलावर घटनाओं के समय को सुनकर जानकारी जुटा रहा हो।

यहाँ इस शोध पत्र के निष्कर्षों का सरल उपमाओं (analogies) का उपयोग करके विवरण दिया गया है।

1. समस्या: "बहुत स्मार्ट" घुसपैठिया

2009 में, फ्रैंक कासेज़ नामक एक शोधकर्ता ने सिद्ध किया कि सामान्य टाइमड सिस्टम (timed systems) के लिए, आप एल्गोरिदम के माध्यम से यह निर्धारित नहीं कर सकते कि क्या एक हमलावर केवल घटनाओं के समय को सुनकर किसी रहस्य का पता लगा सकता है। यह एक जादूगर के जादू को समझने की असंभवता को साबित करने जैसा है, जब जादूगर अनंत समय और अनंत जटिलता का उपयोग कर सकता है। गणित कहता है: यह अनिर्णायक (undecidable) है। आप ऐसा कंप्यूटर प्रोग्राम नहीं लिख सकते जो हमेशा "हाँ" या "नहीं" में उत्तर दे सके।

इस शोध पत्र के लेखकों ने इस समस्या को तीन विशिष्ट तरीकों से नियमों को बदलकर "उज्ज्वल पक्ष" (bright side) खोजने का निर्णय लिया ताकि इसे हल करने योग्य बनाया जा सके।

2. योगदान एक: खेल के नियमों को स्पष्ट करना

समस्या को हल करने से पहले, लेखकों ने स्पष्ट किया कि "ओपेसिटी" (opacity) का वास्तव में क्या अर्थ है। उन्होंने तीन स्तरों की गोपनीयता की तुलना की:

एग्जिस्टेंशियल ओपेसिटी (Existential Opacity): "क्या कम से कम एक ऐसा गुप्त इवेंट है जो बिल्कुल एक सामान्य इवेंट जैसा दिखता है?" (गोपनीयता का सबसे कमजोर रूप)।
वीक ओपेसिटी (Weak Opacity): "यदि एक गुप्त घटना होती है, तो क्या हमलावर बता सकता है कि वह एक गुप्त घटना है?" (हमलावर यह अनुमान लगा सकता है कि वह गुप्त नहीं है, लेकिन वह निश्चित नहीं हो सकता कि वह गुप्त है)।
फुल ओपेसिटी (Full Opacity): "क्या हमलावर यह बता सकता है कि क्या कोई गुप्त घटना हुई है या नहीं?" (हमलावर पूरी तरह से अंधेरे में है)।

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

3. योगदान दो: तिजोरी को सरल बनाना (Subclasses)

चूंकि सामान्य समस्या हल करने योग्य नहीं है, इसलिए लेखकों ने पूछा: "क्या होगा यदि हम तिजोरी को सरल बना दें?" उन्होंने यह देखने के लिए सिस्टम के विभिन्न सरल संस्करणों का परीक्षण किया कि क्या समस्या हल करने योग्य हो जाती है।

"एक-क्रिया" (One-Action) वाली तिजोरी: कल्पना कीजिए कि एक तिजोरी केवल एक प्रकार की आवाज़ (जैसे, एक एकल "बीप") करती है।
- परिणाम: अभी भी हल करने योग्य नहीं। केवल एक ध्वनि होने के बावजूद, समय के अंतर इतने जटिल होते हैं कि वे एक ऐसे गुप्त रहस्य को छिपा सकते हैं जिसे पकड़ा नहीं जा सकता।
"एक-घड़ी" (One-Clock) वाली तिजोरी: कल्पना कीजिए कि तिजोरी में केवल एक टाइमर है।
- परिणाम: हल करने योग्य नहीं यदि तिजोरी शांत चालें (जैसे, एक शांत "टिक" जिसे कोई नहीं सुनता) चल सकती है।
- परिणाम: हल करने योग्य यदि तिजोरी शांत चालें नहीं चल सकती है। यदि प्रत्येक क्रिया एक ध्वनि उत्पन्न करती है, तो गणित काम करता है।
"डिस्क्रीट टाइम" (Discrete Time) वाली तिजोरी: कल्पना कीजिए कि तिजोरी केवल पूर्ण सेकंड (1, 2, 3) में टिक-टिक करती है, न कि सेकंड के अंशों (1.1, 1.11) में।
- परिणाम: हल करने योग्य। वास्तविक समय की अनंत सटीकता को हटाकर, समस्या प्रबंधनीय हो जाती है।
"ऑब्जर्वेबल" (Observable) वाली तिजोरी: कल्पना कीजिए कि एक तिजोरी जहाँ हर बार जब टाइमर रीसेट होता है, तो एक लाइट चमकती है।
- परिणाम: हल करने योग्य। यदि हमलावर देख सकता है कि टाइमर कब रीसेट होते हैं, तो सिस्टम इतना पूर्वानुमानित हो जाता है कि गोपनीयता की जांच की जा सके।

4. योगदान तीन: "सीमित बजट" वाला घुसपैठिया (मुख्य सफलता)

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

लेखकों ने एक नया नियम प्रस्तावित किया: हमलावर के पास केवल एक सीमित बजट है। वे या तो पहले N घटनाओं को सुन सकते हैं, या वे N विशिष्ट समय पर सिस्टम की जाँच कर सकते हैं।

उन्होंने सीमित बजट के लिए तीन परिदृश्यों का परीक्षण किया:

पहली N घटनाएँ: हमलावर पहले 5 क्लिक सुनता है और फिर रुक जाता है।
निश्चित चेकपॉइंट्स: हमलावर पहले से तय करता है, "मैं 10:00, 10:05 और 10:10 पर सिस्टम की जाँच करूँगा।"
डायनेमिक स्ट्रैटेजी (Dynamic Strategy): हमलावर स्मार्ट है। वे पहली घटना को सुनते हैं, जो उन्होंने सुना उसके आधार पर तय करते हैं कि अगली बार कब जाँच करनी है, और यह प्रक्रिया N बार दोहराते हैं।

खोज: तीनों मामलों में, सबसे जटिल तिजोरियों (पूर्ण क्लास ऑफ टाइमड ऑटोमेटा) के साथ भी, समस्या हल करने योग्य हो जाती है।

क्यों? क्योंकि हमलावर की स्मृति सीमित है। एक बार जब वे सुनना बंद कर देते हैं, तो भविष्य की अनंत जटिलता मायने नहीं रखती। लेखकों ने यह जाँचने के लिए एक गणितीय विधि बनाई कि क्या "रहस्य" उस सीमित विंडो के भीतर छिपा हुआ है।
जटिलता (Complexity): हल करने योग्य होने के बावजूद, यह कंप्यूटर के लिए एक बहुत कठिन समस्या है (इसे Co-NEXPTIME-complete के रूप में वर्गीकृत किया गया है), जिसका अर्थ है कि इसके लिए बहुत अधिक कंप्यूटिंग शक्ति की आवश्यकता होती है, लेकिन यह सैद्धांतिक रूप से हल करने योग्य है।

5. "उज्ज्वल पक्ष" का सारांश

यह शोध पत्र अनिवार्य रूप से कहता है:

यदि आप एक जटिल, वास्तविक समय के सिस्टम में एक अनंत धैर्य रखने वाले हमलावर से एक रहस्य छिपाने की कोशिश करते हैं, तो आप यह सिद्ध नहीं कर सकते कि वह सुरक्षित है।
हालाँकि, यदि आप हमलावर की सुनने की क्षमता को सीमित करते हैं (समय, घटनाओं की संख्या, या उनकी रणनीति द्वारा), तो आप गणितीय रूप से सिद्ध कर सकते हैं कि सिस्टम सुरक्षित है या नहीं।

लेखकों ने केवल यह नहीं कहा कि "यह संभव है"; उन्होंने इन सीमित-बजट परिदृश्यों में गोपनीयता की जाँच करने के लिए सटीक गणितीय रेसिपी (एल्गोरिदम) भी प्रदान की, जिससे एक असंभव समस्या को एक बहुत ही कठिन लेकिन हल करने योग्य समस्या में बदल दिया गया।

तकनीकी सारांश: टाइमड ओपेसिटीिटी (Timed Opacity) का उज्ज्वल पक्ष

1. समस्या विवरण (Problem Statement)

यह शोध पत्र टाइमड ऑटोमेटा (TAs) के लिए टाइमड ओपेसिटी (timed opacity) समस्या को संबोधित करता है। टाइमड ओपेसिटीिटी, उन प्रणालियों में "निजी" (private) स्थानों के संबंध में सूचना रिसाव (information leakage) की अनुपस्थिति को औपचारिक रूप देती है जहाँ एक हमलावर (attacker) कुछ कार्यों (actions) को उनके टाइमस्टैम्प के साथ देखता है। मुख्य सुरक्षा लक्ष्य यह सुनिश्चित करना है कि हमलावर निश्चितता के साथ यह निष्कर्ष न निकाल सके कि सिस्टम के निष्पादन (execution) के दौरान किसी निजी स्थान का दौरा किया गया था या नहीं।

यह समस्या कैसेज़ (Cassez [Cas09]) के मौलिक कार्य से प्रेरित है, जिसने स्थापित किया था कि सामान्य TAs के लिए टाइमड ओपेसिटीिटी अनिर्धारणीय (undecidable) है, और विशेष रूप से इवेंट-रिकॉर्डिंग ऑटोमेटा (ERAs) के प्रतिबंधित उपवर्ग के लिए भी। यह अनिर्धारणीयता हमलावर द्वारा टाइमस्टैम्प को सह-संबंधित करने के लिए आवश्यक अनबाउंड मेमोरी (unbounded memory) और TAs के अनंत स्टेट स्पेस (infinite state space) से उत्पन्न होती है। लेखक इस समस्या के "उज्ज्वल पक्षों" (bright sides) को खोजने का लक्ष्य रखते हैं, जिसके लिए या तो सिस्टम मॉडल या हमलावर की क्षमताओं को प्रतिबंधित किया जाता है ताकि निर्धारणीयता (decidability) को पुनः प्राप्त किया जा सके।

लेखक निजी रन ( $Tr_{priv}$ ) और सार्वजनिक रन ( $Tr_{pub}$ ) द्वारा उत्पन्न ट्रेसों के सेट के बीच संबंध के आधार पर ओपेसिटीिटी के तीन वेरिएंट्स को परिभाषित करते हैं:

$\exists$ -opacity: निजी और सार्वजनिक रन के बीच कम से कम एक साझा ट्रेस मौजूद है (सबसे कमजोर रूप)।
Weak opacity: प्रत्येक निजी ट्रेस एक सार्वजनिक ट्रेस भी है ( $Tr_{priv} \subseteq Tr_{pub}$ )।
Full opacity: निजी और सार्वजनिक ट्रेस के सेट समान हैं ( $Tr_{priv} = Tr_{pub}$ )।

2. कार्यप्रणाली (Methodology)

लेखक ऑटोमेटा-सैद्धांतिक निर्माण (automata-theoretic constructions), शास्त्रीय TA समस्याओं (reachability, language inclusion) में न्यूनीकरण (reductions), और जटिलता विश्लेषण (complexity analysis) के संयोजन का उपयोग करते हैं।

2.1. इंटर-रिड्यूसिबिलिटी फ्रेमवर्क (Inter-reducibility Framework)

एक मौलिक पद्धतिगत योगदान ओपेसिटीिटी वेरिएंट्स और शास्त्रीय TA समस्याओं के बीच इंटर-रिड्यूसिबिलिटी (inter-reducibility) की स्थापना है:

Weak बनाम Full Opacity: इसे निजी और सार्वजनिक रन को बदलने वाले एक निर्माण के माध्यम से इंटर-रिड्यूसिबल सिद्ध किया गया है (Theorem 4.5)। यह लेखकों को निर्धारणीयता प्रमाणों के लिए एक वेरिएंट (आमतौर पर weak opacity) पर ध्यान केंद्रित करने की अनुमति देता है।
$\exists$ -opacity बनाम Reachability: इसे इंटर-रिड्यूसिबल सिद्ध किया गया है। चूंकि TAs के लिए reachability, PSPACE-complete है, यह $\exists$ -opacity की जटिलता को स्थापित करता है।
Weak Opacity बनाम Language Inclusion: इसे इंटर-रिड्यूसिबल सिद्ध किया गया है। चूंकि सामान्य TAs के लिए language inclusion अनिर्धारणीय है, यह सामान्य मामले में weak/full opacity की अनिर्धारणीयता की व्याख्या करता है।

2.2. उपवर्ग विश्लेषण (Subclass Analysis)

लेखक TAs के विशिष्ट उपवर्गों के लिए ओपेसिटीिटी का विश्लेषण करते हैं:

One-action TAs: अल्फाबेट के आकार को कम करना।
One-clock TAs: घड़ियों (clocks) की संख्या को कम करना, $\epsilon$ -ट्रांजिशन के साथ और बिना।
Discrete Time TAs: क्लॉक वैल्यूएशन को रियल नंबर्स ( $\mathbb{R}_{\ge 0}$ ) के बजाय नेचुरल नंबर्स ( $\mathbb{N}$ ) तक सीमित करना।
Observable ERAs (oERAs): एक नया उपवर्ग जहाँ क्लॉक को रीसेट करने वाले सभी एक्शन अवलोकन योग्य (observable) हैं (कोई छिपे हुए $\epsilon$ -ट्रांजिशन नहीं जो क्लॉक को रीसेट करते हैं)।

2.3. हमलावर बजट में कमी (Attacker Budget Reduction)

TAs के पूर्ण वर्ग को संभालने के लिए, लेखक हमलावर के "बजट" को सीमित करने वाली एक नई कार्यप्रणाली पेश करते हैं। वे टाइम सिलेक्शन फंक्शन्स ( $\sigma$ ) को परिभाषित करते हैं जो यह निर्धारित करते हैं कि हमलावर सिस्टम का अवलोकन कब करता है। तीन विशिष्ट सेटिंग्स का विश्लेषण किया गया है:

प्रथम $N$ अवलोकन (First $N$ observations): हमलावर केवल पहले $N$ अवलोकन योग्य कार्यों को देखता है।
$N$ स्टैटिक टाइमस्टैम्प ( $N$ static timestamps): हमलावर $N$ समय बिंदुओं का पूर्व-चयन करता है और प्रत्येक के बाद होने वाले पहले एक्शन को देखता है।
$N$ डायनेमिक टाइमस्टैम्प ( $N$ dynamic timestamps): हमलावर पिछले अवलोकनों के आधार पर अगले अवलोकन समय को अनुकूल रूप से (adaptively) चुनता है।

इन बाउंडेड सेटिंग्स के लिए निर्धारणीयता सिद्ध करने के लिए, लेखक एक "टिक" (tick) निर्माण पेश करते हैं। इसमें TA को एक ग्लोबल "टिक" क्लॉक और सहायक क्लॉक्स के साथ बढ़ाना शामिल है ताकि टाइमड वर्ड्स के इक्विवेलेंस क्लास (इंटीग्रल पार्ट्स और फ्रैक्शनल पार्ट्स के सापेक्ष क्रम के आधार पर) को एक अनटाइमड (untimed) ट्रेस में एनकोड किया जा सके। यह बाउंडेड ऑब्जर्वेशन के लिए टाइमड लैंग्वेज इनक्लूजन समस्या को परिमित रेगुलर ऑटोमेटा (विशेष रूप से, $N$ -bounded भाषाओं) के लिए लैंग्वेज इनक्लूजन समस्या में बदल देता है।

3. मुख्य योगदान और परिणाम (Key Contributions and Results)

3.1. इंटर-रिड्यूसिबिलिटी और जटिलता (Inter-reducibility and Complexity)

Weak और Full Opacity की समानता: लेखक सिद्ध करते हैं कि weak opacity को निर्धारित करना, full opacity को निर्धारित करने के बहुपद रूप से समतुल्य (polynomially equivalent) है। यह उपवर्गों के विश्लेषण को सरल बनाता है।
$\exists$ -opacity की जटिलता: यह सामान्य TAs के लिए PSPACE-complete है। One-clock TAs के लिए, लेखक सिद्ध करते हैं कि यह अभी भी PSPACE-complete रहता है (Theorem 5.1), जो पिछले अनुमानों को परिष्कृत करता है।

3.2. उपवर्गों में निर्धारणीयता (Decidability in Subclasses)

यह शोध पत्र weak/full opacity के लिए निर्धारणीयता और अनिर्धारणीयता के बीच एक सटीक सीमा खींचता है:

अनिर्धारणीय (Undecidable):
- Single action वाले TAs (बिना $\epsilon$ -ट्रांजिशन के भी) (Theorem 5.2)।
- दो या अधिक क्लॉक्स वाले TAs (Theorem 5.7)।
- $\epsilon$ -ट्रांजिशन के साथ एक क्लॉक वाले TAs (Theorem 5.4)।
निर्धारणीय (Decidable):
- $\epsilon$ -ट्रांजिशन के बिना एक क्लॉक वाले TAs: Non-primitive recursive जटिलता के साथ निर्धारणीय (Theorem 5.5)।
- Discrete time पर TAs: EXPSPACE-complete जटिलता के साथ निर्धारणीय (Corollary 5.14)।
- Observable ERAs (oERAs): PSPACE-complete जटिलता के साथ निर्धारणीय (Theorem 5.16)।

नोट: यह शोध पत्र यह भी स्थापित करता है कि discrete-time TAs के लिए टाइमड लैंग्वेज इनक्लूजन EXPSPACE-complete है, जो कि एक ज्ञात परिणाम है लेकिन जिसकी सटीक जटिलता अज्ञात थी।

3.3. सीमित हमलावर बजट (Limited Attacker Budget - मुख्य योगदान)

सबसे महत्वपूर्ण योगदान यह प्रमाण है कि यदि हमलावर का अवलोकन बजट $N$ अवलोकनों तक सीमित है, तो ओपेसिटीिटी पूरे TA वर्ग के लिए निर्धारणीय (decidable) हो जाती है।

सेटिंग्स: यह परिणाम तीनों हमलावर मॉडलों के लिए मान्य है: प्रथम $N$ इवेंट्स, $N$ स्टैटिक टाइमस्टैम्प, और $N$ डायनेमिक टाइमस्टैम्प।
जटिलता: तीनों सेटिंग्स के लिए निर्णय समस्या Co-NEXPTIME-complete है (Theorem 6.19, Corollary 6.20, Theorem 6.31, Theorem 6.33)।
तंत्र (Mechanism): प्रमाण "टिक" निर्माण पर निर्भर करता है जो टाइमड समस्या को $N$ -bounded टाइमड भाषाओं के समावेश (inclusion) में कम करता है, जिसे Co-NEXPTIME-complete दिखाया गया है।

3.4. संयुक्त प्रतिबंध (Combined Restrictions)

लेखक मॉडल प्रतिबंधों (जैसे, one-clock, discrete time) को हमलावर बजट के साथ मिलाकर भी विश्लेषण करते हैं।

One-action TAs के लिए $N$ अवलोकनों के साथ, समस्या Co-NEXPTIME-complete बनी रहती है।
One-clock TAs के लिए $N$ अवलोकनों के साथ, समस्या PSPACE-hard है और Co-NEXPTIME में है (Theorem 6.35)।
oERAs के लिए $N$ अवलोकनों के साथ, समस्या PSPACE-complete है (Theorem 6.37)।

4. महत्व और दावे (Significance and Claims)

यह शोध पत्र दावा करता है कि यह Cassez [Cas09] के नकारात्मक परिणामों से आगे बढ़कर, टाइमड ओपेसिटीिटी के निर्धारणीयता परिदृश्य (decidability landscape) का एक व्यापक लक्षण वर्णन प्रदान करता है।

सीमा को स्पष्ट करना: यह कार्य उन न्यूनतम स्थितियों (जैसे, एक-क्लॉक TAs में $\epsilon$ -ट्रांजिशन की उपस्थिति, या क्रियाओं की संख्या) की सटीक पहचान करता है जो अनिर्धारणीयता को ट्रिगर करती हैं।
व्यावहारिक निर्धारणीयता: एक सीमित हमलावर बजट (परिमित अवलोकन) की अवधारणा पेश करके, लेखक यह प्रदर्शित करते हैं कि ओपेसिटीिटी पूरे टाइमड ऑटोमेटा वर्ग के लिए निर्धारणीय है, बशर्ते हमलावर के पास अनबाउंड घटनाओं का अनुक्रम देखने की क्षमता न हो। यह वास्तविक परिदृश्यों को मॉडल करता जहाँ हमलावरों के पास सीमित संसाधन या निगरानी क्षमताएं होती हैं।
जटिलता की सटीकता (Complexity Tightness): यह शोध पत्र विभिन्न सेटिंग्स के लिए सटीक जटिलता वर्गों (PSPACE, EXPSPACE, Co-NEXPTIME) को प्रदान करता है, जो ओपेसिटीिटी के सत्यापन की कम्प्यूटेशनल लागत की समझ को परिष्कृत करता है।
पद्धतिगत नवाचार: "टिक" निर्माण और टाइम सिलेक्शन फंक्शन्स का उपयोग आंशिक अवलोकन (partial observation) के तहत टाइमड सिस्टम का विश्लेषण करने के लिए नए उपकरण प्रदान करता है, जो डेंस-टाइम सिमेंटिक्स (dense-time semantics) और परिमित-अवस्था सत्यापन तकनीकों (finite-state verification techniques) के बीच के अंतर को पाटता है।

लेखक निष्कर्ष निकालते हैं कि जबकि अत्यधिक अभिव्यंजक सेटिंग्स (अनबाउंड अवलोकन के साथ सामान्य TAs) में अनिर्धारणीयता बनी रहती है, हमलावर की शक्ति को एक परिमित बजट तक सीमित करने से एक मजबूत, निर्धारणीय ढांचा प्राप्त होता है जो पूर्ण TA औपचारिकता (formalism) के लिए लागू करने योग्य है।