2025-11-15T12:40:11.869613

Formally Verified Certification of Unsolvability of Temporal Planning Problems

Wang, Abdulaziz

We present an approach to unsolvability certification of temporal planning. Our approach is based on encoding the planning problem into a network of timed automata, and then using an efficient model checker on the network followed by a certificate checker to certify the output of the model checker. Our approach prioritises trustworthiness of the certification: we formally verify our implementation of the encoding to timed automata using the theorem prover Isabelle/HOL and we use an existing certificate checker (also formally verified in Isabelle/HOL) to certify the model checking result.

academic

समय-आधारित नियोजन समस्याओं की अघुलनशीलता का औपचारिक रूप से सत्यापित प्रमाणन

मूल जानकारी

पेपर ID: 2510.10189
शीर्षक: समय-आधारित नियोजन समस्याओं की अघुलनशीलता का औपचारिक रूप से सत्यापित प्रमाणन
लेखक: डेविड वांग, मोहम्मद अब्दुलअज़ीज़ (किंग्स कॉलेज लंदन, यूनाइटेड किंगडम)
वर्गीकरण: cs.LO (कंप्यूटर विज्ञान में तर्क), cs.AI (कृत्रिम बुद्धिमत्ता)
प्रकाशन तिथि: 11 अक्टूबर 2025 (arXiv प्रीप्रिंट)
पेपर लिंक: https://arxiv.org/abs/2510.10189

सारांश

यह पेपर समय-आधारित नियोजन समस्याओं की अघुलनशीलता के प्रमाणन के लिए एक विधि प्रस्तुत करता है। यह विधि नियोजन समस्याओं को समय स्वचालितों के नेटवर्क में एन्कोड करने, नेटवर्क पर कुशल मॉडल चेकर का उपयोग करने, और फिर प्रमाणपत्र चेकर का उपयोग करके मॉडल चेकर के आउटपुट को प्रमाणित करने पर आधारित है। यह विधि प्रमाणन की विश्वसनीयता को प्राथमिकता देती है: समय स्वचालितों के एन्कोडिंग के कार्यान्वयन को Isabelle/HOL प्रमेय प्रमाणक के साथ औपचारिक रूप से सत्यापित करता है, और मॉडल चेकिंग परिणामों को प्रमाणित करने के लिए मौजूदा प्रमाणपत्र चेकर (समान रूप से Isabelle/HOL में औपचारिक रूप से सत्यापित) का उपयोग करता है।

अनुसंधान पृष्ठभूमि और प्रेरणा

मूल समस्या

इस अनुसंधान द्वारा समाधान की जाने वाली मूल समस्या समय-आधारित नियोजन समस्याओं की अघुलनशीलता का प्रमाणन है। समय-आधारित नियोजन एक समृद्ध नियोजन रूप है जो क्रियाओं को अवधि और समवर्ती निष्पादन की अनुमति देता है, जो शास्त्रीय नियोजन की तुलना में अधिक जटिल है।

समस्या की महत्ता

विश्वसनीयता आवश्यकता: मौजूदा नियोजन प्रणालियाँ एल्गोरिथ्म और कार्यान्वयन स्तर पर अत्यंत जटिल हैं, उनके आउटपुट की विश्वसनीयता में सुधार महत्वपूर्ण है
प्रमाणन कठिनाई: हल करने योग्य समस्याओं के विपरीत (जिन्हें योजना को निष्पादित करके सत्यापित किया जा सकता है), अघुलनशीलता या इष्टतमता के दावे को संक्षिप्त प्रमाणपत्र प्राप्त करना कठिन है
घातीय जटिलता: सबसे खराब स्थिति में, ऐसे प्रमाणपत्र नियोजन कार्य के आकार के सापेक्ष घातीय रूप से बढ़ सकते हैं

मौजूदा विधियों की सीमाएँ

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

अनुसंधान प्रेरणा

यह पेपर एन्कोडिंग रूपांतरण विधि अपनाता है: समय-आधारित नियोजन समस्याओं को अन्य कम्प्यूटेशनल समस्याओं (समय स्वचालितों) में एन्कोड करता है जिनके लिए व्यावहारिक प्रमाणन एल्गोरिथ्म पहले से मौजूद हैं, और प्रमेय प्रमाणक के माध्यम से संपूर्ण एन्कोडिंग प्रक्रिया और प्रमाणपत्र चेकर को औपचारिक रूप से सत्यापित करता है, प्रमाणन की विश्वसनीयता सुनिश्चित करता है।

मुख्य योगदान

औपचारिक रूप से सत्यापित एन्कोडिंग विधि: पहली बार Heinz आदि के समय-आधारित नियोजन से समय स्वचालितों के एन्कोडिंग को औपचारिक रूप से सत्यापित किया
इंजीनियरिंग कार्यान्वयन: Wimmer और von Mutius प्रणाली के साथ संगत समय स्वचालितों प्रारूप का उत्पादन करने के लिए एन्कोडिंग को अनुकूलित किया
सरलीकृत शब्दार्थ डिजाइन: मौजूदा कार्य की तुलना में सरल समय-आधारित नियोजन शब्दार्थ डिजाइन किया, गणितीय तर्क को सुविधाजनक बनाया, और मौजूदा शब्दार्थ के साथ समतुल्यता साबित की
संपूर्ण प्रमाणन ढांचा: समय-आधारित नियोजन समस्या से समय स्वचालितों मॉडल चेकिंग तक एक संपूर्ण विश्वसनीय प्रमाणन श्रृंखला का निर्माण किया
सैद्धांतिक सही होने की गारंटी: Isabelle/HOL में एन्कोडिंग की सही होने को साबित किया, मजबूत सैद्धांतिक गारंटी प्रदान की

विधि विवरण

कार्य परिभाषा

इनपुट: समय-आधारित नियोजन समस्या P = ⟨P, A, I, G⟩

P: प्रस्तावों का समुच्चय
A: अवधि क्रियाओं का समुच्चय
I: प्रारंभिक स्थिति
G: लक्ष्य शर्त

आउटपुट: अघुलनशीलता का औपचारिक प्रमाणपत्र (यदि समस्या वास्तव में अघुलनशील है)

बाधा शर्तें:

क्रियाओं के पास प्रारंभ और समाप्ति स्नैपशॉट क्रियाएँ हैं
अपरिवर्तनीय शर्तें और शेड्यूलिंग बाधाएँ समर्थित हैं
पारस्परिक बहिष्कार बाधाएँ और अवधि सीमाएँ संतुष्ट करते हैं

मॉडल आर्किटेक्चर

1. समय-आधारित नियोजन औपचारिकीकरण

पेपर पहले समय-आधारित नियोजन का औपचारिक शब्दार्थ परिभाषित करता है:

स्नैपशॉट क्रिया (परिभाषा 1):

h ≡ ⟨pre(h), adds(h), dels(h)⟩

अवधि क्रिया (परिभाषा 2):

a ≡ ⟨a⊢, a⊣, over_all(a), L(a), U(a)⟩

जहाँ a⊢ और a⊣ क्रमशः प्रारंभ और समाप्ति स्नैपशॉट क्रियाएँ हैं।

2. समय स्वचालितों एन्कोडिंग

चर डिजाइन (परिभाषा 24):

प्रत्येक प्रस्ताव p के लिए: बाइनरी चर vp (सत्य मान एन्कोड करने के लिए) और लॉक काउंटर lp (p को सत्य रखने वाली सक्रिय क्रियाओं को रिकॉर्ड करने के लिए)
aa: सक्रिय क्रियाओं की कुल संख्या
ps: नियोजन स्थिति (0=शुरू नहीं, 1=नियोजन में, 2=पूर्ण)

घड़ी डिजाइन (परिभाषा 25):

प्रत्येक क्रिया a को दो घड़ियाँ आवंटित की जाती हैं: ca⊢ (प्रारंभ के बाद का समय रिकॉर्ड करने के लिए) और ca⊣ (समाप्ति के बाद का समय रिकॉर्ड करने के लिए)

मुख्य स्वचालित (परिभाषा 26): संपूर्ण नियोजन प्रक्रिया के स्थिति संक्रमण को नियंत्रित करता है, जिसमें आरंभीकरण और लक्ष्य जाँच शामिल है।

क्रिया स्वचालित (परिभाषा 27): प्रत्येक क्रिया के लिए एक स्वचालित, निम्नलिखित मुख्य संक्रमण सहित:

sea: क्रिया प्रारंभ के प्रभाव का अनुप्रयोग
se'a: अपरिवर्तनीय शर्त लॉकिंग
eea: समाप्ति से पहले की तैयारी
ee'a: क्रिया समाप्ति के प्रभाव का अनुप्रयोग
iea: तत्काल क्रिया प्रसंस्करण

3. नेटवर्क निर्माण

मुख्य स्वचालित और सभी क्रिया स्वचालितों को समय स्वचालितों नेटवर्क में संयोजित करता है (परिभाषा 28), प्रारंभिक कॉन्फ़िगरेशन सभी स्वचालितों को निष्क्रिय स्थिति में सेट करता है।

तकनीकी नवाचार बिंदु

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

प्रयोगात्मक सेटअप

औपचारिक सत्यापन पर्यावरण

प्रमेय प्रमाणक: Isabelle/HOL
प्रमाणपत्र चेकर: Wimmer और von Mutius का सत्यापित प्रमाणपत्र चेकर
लक्ष्य गुण: पहुँच योग्यता जाँच A ⊨ EF(loc(AM) = goal)

कोड आकार सांख्यिकी

घटक	कोड पंक्तियाँ
अमूर्त समय-आधारित नियोजन शब्दार्थ औपचारिकीकरण	~7,200
Munta का उपयोग करके समय स्वचालितों नेटवर्क परिभाषा	~800
प्रमेय 1 और संबंधित लेम्मा का प्रमाण	~8,500
सूची संबंधित लेम्मा	~1,500
कुल	~18,000

तुलनात्मक बेंचमार्क

संबंधित औपचारिक कार्य के आकार के साथ तुलना:

सत्यापित SAT-आधारित नियोजक: ~17,500 पंक्तियाँ
सत्यापित शास्त्रीय नियोजन सत्यापक: ~3,000 पंक्तियाँ
सत्यापित समय-आधारित PDDL नियोजन सत्यापक: ~6,500 पंक्तियाँ

प्रयोगात्मक परिणाम

मुख्य सैद्धांतिक परिणाम

प्रमेय 1 (मुख्य सही होने की प्रमेय): यदि योजना π वैध है और स्व-अतिव्यापी नहीं है (valid(π) ∧ no_self_overlap(π)), तो दावा A ⊨ EF(loc(AM) = goal) सत्य है।

प्रमाण संरचना:

लेम्मा 1: समानांतर योजना के निष्पादन को प्रेरित करने वाले अनुकरण का निर्माण
लेम्मा 2: प्रारंभिक कॉन्फ़िगरेशन से एन्कोडेड स्थिति तक पहुँच योग्यता
लेम्मा 3: अंतिम स्थिति से लक्ष्य कॉन्फ़िगरेशन तक संक्रमण

औपचारिक सत्यापन उपलब्धियाँ

संपूर्णता प्रमाण: एन्कोडिंग की संपूर्णता को सफलतापूर्वक साबित किया, अर्थात् प्रत्येक वैध योजना संबंधित समय स्वचालितों नेटवर्क में एक वैध निष्पादन पाती है
मशीन जाँच: सभी प्रमाण Isabelle/HOL की मशीन जाँच से गुजरते हैं, विश्वसनीयता की सर्वोच्च स्तर की गारंटी प्रदान करते हैं
मॉड्यूलर डिजाइन: प्रमाण संरचना मॉड्यूलर है, समझ और रखरखाव को सुविधाजनक बनाता है

इंजीनियरिंग कार्यान्वयन सत्यापन

एन्कोडिंग कार्यान्वयन को मौजूदा सत्यापित प्रमाणपत्र चेकर के साथ संगत प्रारूप में अनुकूलित किया गया है, एक संपूर्ण निष्पादन योग्य प्रमाणन श्रृंखला बनाता है।

निष्कर्ष और चर्चा

मुख्य निष्कर्ष

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

सीमाएँ

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

भविष्य की दिशाएँ

समतुल्यता प्रमाण: इस पेपर के शब्दार्थ और मौजूदा सत्यापक शब्दार्थ के बीच समतुल्यता को औपचारिक रूप से साबित करने की योजना
निष्पादन योग्य कार्यान्वयन: निष्पादन योग्य प्रमाणपत्र चेकर विकसित करना
उदाहरणीकरण सत्यापन: उदाहरणीकरण एल्गोरिथ्म को औपचारिक रूप से सत्यापित करना, जैसे Helmert का डेटालॉग सॉल्वर
बाधा शिथिलीकरण: स्व-अतिव्यापी शर्त को शिथिल करने की संभावना का अनुसंधान

गहन मूल्यांकन

शक्तियाँ

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

कमियाँ

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

प्रभाव

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

लागू परिस्थितियाँ

महत्वपूर्ण प्रणालियाँ: उच्च विश्वसनीयता गारंटी की आवश्यकता वाली नियोजन अनुप्रयोग (जैसे एयरोस्पेस, चिकित्सा उपकरण)
अनुसंधान उपकरण: समय-आधारित नियोजन अनुसंधान के लिए औपचारिक सत्यापन बुनियादी ढाँचा प्रदान करता है
शैक्षणिक उद्देश्य: औपचारिक विधियों और नियोजन एल्गोरिथ्म शिक्षण के लिए केस स्टडी के रूप में
उपकरण विकास: विश्वसनीय नियोजन उपकरण विकास के लिए सैद्धांतिक आधार प्रदान करता है

संदर्भ

मुख्य संदर्भ साहित्य में शामिल हैं:

Abdulaziz & Koller (2022): समय-आधारित नियोजन का औपचारिक शब्दार्थ और सत्यापक
Heinz et al. (2019): समय-आधारित नियोजन से समय स्वचालितों का एन्कोडिंग
Wimmer & von Mutius (2020): समय स्वचालितों के सत्यापित प्रमाणपत्र चेकर
Abdulaziz & Kurz (2023): सत्यापित SAT-आधारित नियोजन प्रणाली

यह पेपर समय-आधारित नियोजन के औपचारिक सत्यापन क्षेत्र में महत्वपूर्ण योगदान देता है। हालाँकि व्यावहारिक पहलुओं में सुधार की गुंजाइश है, लेकिन इसकी सैद्धांतिक कठोरता और विधि नवाचार इस क्षेत्र के विकास के लिए एक मजबूत आधार प्रदान करते हैं।