Modelling and Model-Checking a ROS2 Multi-Robot System using Timed Rebeca

रोबोटिक्स की दुनिया में, एक ऐसी मशीन बनाना जो चल सके और सोच सके, अपने आप में एक कठिन कार्य है। लेकिन ऐसी मशीनों की एक टीम बनाना जो एक-दूसरे से टकराए बिना मिलकर काम कर सके, यह एक बिल्कुल अलग तरह की चुनौती है। इन मशीनों को अक्सर स्वायत्त मोबाइल रोबोट (autonomous mobile robots) कहा जाता है, जिन्हें दीवारों, लोगों और एक-दूसरे से बचते हुए विशिष्ट गंतव्यों तक पहुँचने के लिए डिज़ाइन किया गया है। उन्हें चलाने वाला सॉफ़्टवेयर अविश्वसनीय रूप से जटिल होता है, जो यह समझने के लिए लेज़र जैसे सेंसरों से प्राप्त डेटा के निरंतर प्रवाह पर निर्भर करता है कि वे कहाँ हैं और उनके आसपास क्या है। चूँकि ये रोबोट एक निरंतर भौतिक दुनिया में काम करते हैं, इसलिए उनकी गति सुचारू और तरल होती है, जो सेकंड के सूक्ष्म अंशों और मिलीमीटर की दूरी में बदलती रहती है। हालाँकि, उन्हें नियंत्रित करने वाले कंप्यूटर 'डिस्क्रीट स्टेप्स' (discrete steps) में सोचते हैं, यानी वे जानकारी को समय के अलग-अलग हिस्सों में प्रोसेस करते हैं। भौतिकी की सुचारू वास्तविकता और कोड के चरण-दर-चरण तर्क के बीच का यह अंतर एक खतरनाक 'ब्लाइंड स्पॉट' पैदा करता है। यदि सॉफ़्टवेयर पूरी तरह से ट्यून नहीं है, तो एक रोबोट इतनी तेज़ी से चल सकता है कि उसके सेंसर बाधा को पकड़ न पाएं, या दो रोबोट ठीक उसी क्षण एक ही चौराहे पर पहुँच सकते हैं, जिससे एक 'डेडलॉक' (deadlock) की स्थिति पैदा हो सकती है जहाँ कोई भी आगे नहीं बढ़ पाता।

इसे हल करने के लिए, शोधकर्ताओं को वास्तविक मशीनों को चालू करने से पहले हर उस संभावित परिदृश्य का परीक्षण करने के तरीके की आवश्यकता है जिसका सामना एक रोबोट टीम कर सकती है। यहीं पर 'फॉर्मल वेरिफिकेशन' (formal verification) नामक एक क्षेत्र आता है। केवल एक सिमुलेशन को कुछ बार चलाकर और उम्मीद करने के बजाय कि सब ठीक रहेगा, फॉर्मल वेरिफिकेशन एक सिस्टम द्वारा लिए जा सकने वाले हर एक पथ की जांच करने के लिए गणितीय तर्क का उपयोग करता है। यह एक सरल लेकिन शक्तिशाली प्रश्न पूछता है: क्या घटनाओं का कोई भी ऐसा क्रम संभव है, चाहे वह कितना भी असंभावित क्यों न हो, जो सिस्टम को विफल कर दे? रोबोट की एक टीम के लिए, इसका अर्थ है यह सिद्ध करना कि वे कभी आपस में नहीं टकराएंगे, कभी भी हमेशा के लिए फंसेंगे नहीं, और हमेशा अपने लक्ष्यों तक पहुँचेंगे। चुनौती हमेशा यह रही है कि वास्तविक रोबोट एक निरंतर दुनिया में चलते हैं, जबकि इन गणितीय प्रमाणों के लिए दुनिया को निश्चित चरणों के ग्रिड में विभाजित करना आवश्यक होता है। यदि चरण बहुत बड़े हैं, तो प्रमाण छोटी लेकिन महत्वपूर्ण दुर्घटनाओं को छोड़ देता है। यदि चरण बहुत छोटे हैं हैं, तो कंप्यूटर संभावनाओं की विशाल संख्या से अभिभूत हो जाता है और गणना पूरी नहीं कर पाता।

इस अंतर को पाटने के लिए स्वीडन के मालेर्डलेन यूनिवर्सिटी और के sense टीएच रॉयल इंस्टीट्यूट ऑफ टेक्नोलॉजी की शोधकर्ताओं की एक टीम ने एक नया तरीका विकसित किया है। उन्होंने एक प्रणाली बनाई है जो इंजीनियरों को 'टाइम्ड रेबेका' (Timed Rebeca) नामक एक विशेष मॉडलिंग भाषा का उपयोग करके एक मल्टी-रोबोट टीम को डिज़ाइन करने की अनुमति देती है, जो प्रत्येक रोबोट को संदेशों पर प्रतिक्रिया करने वाले एक स्वतंत्र अभिनेता (actor) के रूप में मानती है। इस मॉडल की सुरक्षा सुनिश्चित करने के लिए कंप्यूटर द्वारा कठोरता से जाँच की जाती है। महत्वपूर्ण रूप से, टीम ने रोबोट के लिए वास्तविक सॉफ़्टवेयर को 'रोस2' (ROS2) नामक एक मानक प्रणाली का उपयोग करके लिखा, जिससे यह सुनिश्चित हुआ कि गणितीय मॉडल और वास्तविक कोड पूरी तरह से संरेखित हों। उन्होंने केवल रोबोट का सिमुलेशन नहीं किया; उन्होंने मॉडल का एक ऐसा संस्करण बनाया जो कंप्यूटर द्वारा जांचा जाने के लिए पर्याप्त अमूर्त (abstract) था, लेकिन मशीनों के वास्तविक भौतिक विज्ञान को दर्शाने के लिए पर्याप्त विस्तृत भी था। ऐसा करके, वे उन दुर्लभ और खतरनाक विफलताओं की भविष्यवाणी कर सके जिन्हें मानक सिमुलेशन अक्सर छोड़ देते हैं।

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

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

उनके प्रयोगों के परिणाम चौंकाने वाले थे। उन मामलों में जहाँ रोबकों को सुरक्षित गति और विविध प्रतीक्षा समय के साथ प्रोग्राम किया गया था, मॉडल चेकर ने पुष्टि की कि सभी पाँच रोबोट बिना किसी टक्कर या फंसे बिना अपने गंतव्य तक पहुँच जाएंगे। शोधकर्ताओं ने फिर वास्तविक ROS2 कोड को एक सिमुलेशन में चलाया, और रोबोट ठीक वैसा ही व्यवहार कर रहे थे जैसा उनके मॉडल ने भविष्यवाणी की थी, वे भीड़भाड़ वाले स्थान में सफलतापूर्वक नेविगेट कर रहे थे। हालाँकि, जब उन्होंने खतरनाक स्थिति पैदा करने के लिए पैरामीटर्स को बदला—जैसे कि सभी रोबोटों को बिल्कुल एक ही गति पर चलाना या स्कैन दर को गति के लिए बहुत कम सेट करना—तो मॉडल चेकर ने तुरंत एक खामी ढूंढ ली। इसने घटनाओं के एक विशिष्ट क्रम की पहचान की जो टक्कर का कारण बनेगा। जब उन्होंने इन्हीं खतरनाक सेटिंग्स के साथ वास्तविक कोड चलाया, तो सिमुलेशन ठीक उसी तरह क्रैश हो गया जैसा मॉडल ने भविष्यवाणी की थी। एक परीक्षण में, मॉडल ने कुछ हज़ार स्टेट्स की खोज के बाद ही टक्कर का पता लगा लिया, जबकि वास्तविक सिमुलेशन पाँच में से तीन बार विफल रहा, जिससे पुष्टि हुई कि खतरा वास्तविक और अनुमानित था।

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

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

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