এই পত্রিকায় সময়গত পরিকল্পনা সমস্যার অসমাধানযোগ্যতার প্রমাণপত্রকরণের একটি পদ্ধতি প্রস্তাব করা হয়েছে। এই পদ্ধতিটি পরিকল্পনা সমস্যাগুলিকে সময়গত স্বয়ংক্রিয় নেটওয়ার্কে এনকোড করার উপর ভিত্তি করে তৈরি, তারপর নেটওয়ার্কে দক্ষ মডেল চেকার ব্যবহার করা হয়, এবং পরবর্তীতে প্রমাণপত্র চেকার ব্যবহার করে মডেল চেকারের আউটপুট প্রমাণীকরণ করা হয়। এই পদ্ধতিটি প্রমাণপত্রকরণের বিশ্বাসযোগ্যতাকে অগ্রাধিকার দেয়: ইসাবেল/এইচওএল উপপাদ্য প্রমাণকারী ব্যবহার করে সময়গত স্বয়ংক্রিয় এনকোডিং বাস্তবায়নের আনুপচারিক যাচাইকরণ করা হয়, এবং বিদ্যমান প্রমাণপত্র চেকার (একইভাবে ইসাবেল/এইচওএলে আনুপচারিকভাবে যাচাইকৃত) ব্যবহার করে মডেল চেক ফলাফল প্রমাণীকরণ করা হয়।
এই গবেষণা যে মূল সমস্যাটি সমাধান করতে চায় তা হল সময়গত পরিকল্পনা সমস্যার অসমাধানযোগ্যতার প্রমাণপত্রকরণ। সময়গত পরিকল্পনা একটি সমৃদ্ধ পরিকল্পনা ফর্ম যা ক্রিয়াকলাপগুলিকে স্থায়িত্ব এবং সমসাময়িক সম্পাদন অনুমতি দেয়, যা ধ্রুবক পরিকল্পনার তুলনায় আরও জটিল।
১. বিশ্বাসযোগ্যতার প্রয়োজনীয়তা: বিদ্যমান পরিকল্পনা ব্যবস্থা অ্যালগরিদম এবং বাস্তবায়ন স্তরে অত্যন্ত জটিল, তাদের আউটপুটের বিশ্বাসযোগ্যতা বৃদ্ধি করা অত্যন্ত গুরুত্বপূর্ণ ২. প্রমাণপত্রকরণের কঠিনতা: সমাধানযোগ্য সমস্যার বিপরীতে (যা পরিকল্পনা সম্পাদন করে যাচাই করা যায়), অসমাধানযোগ্যতা বা সর্বোত্তমতার দাবি সংক্ষিপ্ত প্রমাণপত্র পেতে কঠিন ३. সূচকীয় জটিলতা: সর্বোচ্চ ক্ষেত্রে, এই ধরনের প্রমাণপত্র পরিকল্পনা কাজের আকারের সাপেক্ষে সূচকীয়ভাবে বৃদ্ধি পেতে পারে
१. আনুপচারিক নিশ্চয়তার অভাব: বিদ্যমান সময়গত পরিকল্পনা অসমাধানযোগ্যতা সনাক্তকরণ পদ্ধতিতে আনুপচারিক সঠিকতার নিশ্চয়তা নেই २. উচ্চ জটিলতা: অত্যাধুনিক সময়গত পরিকল্পনা অ্যালগরিদম কৌশল অত্যন্ত জটিল, তাদের জন্য ব্যবহারিক অসমাধানযোগ্যতা প্রমাণপত্রকরণ স্কিম ডিজাইন করা কঠিন ३. যাচাইকরণ শূন্যতা: ধ্রুবক পরিকল্পনার ইতিমধ্যে বিদ্যমান আনুপচারিক যাচাইকরণ কাজের তুলনায়, সময়গত পরিকল্পনা ক্ষেত্রে এই দিকে একটি শূন্যতা রয়েছে
এই পত্রিকা এনকোডিং রূপান্তর পদ্ধতি গ্রহণ করে: সময়গত পরিকল্পনা সমস্যাগুলিকে ইতিমধ্যে ব্যবহারিক প্রমাণপত্রকরণ অ্যালগরিদম সহ অন্যান্য গণনামূলক সমস্যায় (সময়গত স্বয়ংক্রিয়) এনকোড করা হয়, এবং উপপাদ্য প্রমাণকারী ব্যবহার করে সম্পূর্ণ এনকোডিং প্রক্রিয়া এবং প্রমাণপত্র চেকার আনুপচারিকভাবে যাচাই করা হয়, প্রমাণপত্রকরণের বিশ্বাসযোগ্যতা নিশ্চিত করে।
१. আনুপচারিকভাবে যাচাইকৃত এনকোডিং পদ্ধতি: প্রথমবারের মতো হেইনজ এবং অন্যদের সময়গত পরিকল্পনা থেকে সময়গত স্বয়ংক্রিয়তার এনকোডিং আনুপচারিকভাবে যাচাই করা হয়েছে २. প্রকৌশল বাস্তবায়ন: উইমার এবং ভন মিউটিয়াস সিস্টেমের সাথে সামঞ্জস্যপূর্ণ সময়গত স্বয়ংক্রিয় ফর্ম্যাট তৈরি করতে এনকোডিং অভিযোজিত করা হয়েছে ३. সরলীকৃত শব্দার্থ ডিজাইন: বিদ্যমান কাজের চেয়ে সহজ সময়গত পরিকল্পনা শব্দার্থ ডিজাইন করা হয়েছে, গাণিতিক যুক্তির জন্য সুবিধাজনক, এবং বিদ্যমান শব্দার্থের সাথে সমতা প্রমাণ করা হয়েছে ४. সম্পূর্ণ প্রমাণপত্রকরণ কাঠামো: সময়গত পরিকল্পনা সমস্যা থেকে সময়গত স্বয়ংক্রিয় মডেল চেকিং পর্যন্ত সম্পূর্ণ বিশ্বাসযোগ্য প্রমাণপত্রকরণ শৃঙ্খল নির্মাণ করা হয়েছে ५. তাত্ত্বিক সঠিকতা নিশ্চয়তা: ইসাবেল/এইচওএলে এনকোডিংয়ের সঠিকতা প্রমাণ করা হয়েছে, শক্তিশালী তাত্ত্বিক নিশ্চয়তা প্রদান করে
ইনপুট: সময়গত পরিকল্পনা সমস্যা P = ⟨P, A, I, G⟩
আউটপুট: অসমাধানযোগ্যতার আনুপচারিক প্রমাণপত্র (যদি সমস্যা সত্যিই অসমাধানযোগ্য হয়)
সীমাবদ্ধতা শর্তাবলী:
পত্রিকা প্রথমে সময়গত পরিকল্পনার আনুপচারিক শব্দার্থ সংজ্ঞায়িত করে:
স্ন্যাপশট ক্রিয়া (সংজ্ঞা १):
h ≡ ⟨pre(h), adds(h), dels(h)⟩
স্থায়ী ক্রিয়া (সংজ্ঞা २):
a ≡ ⟨a⊢, a⊣, over_all(a), L(a), U(a)⟩
যেখানে a⊢ এবং a⊣ যথাক্রমে শুরু এবং শেষ স্ন্যাপশট ক্রিয়া।
পরিবর্তনশীল ডিজাইন (সংজ্ঞা २४):
ঘড়ি ডিজাইন (সংজ্ঞা २५):
প্রধান স্বয়ংক্রিয় (সংজ্ঞা २६): সম্পূর্ণ পরিকল্পনা প্রক্রিয়ার অবস্থা রূপান্তর নিয়ন্ত্রণ করে, প্রাথমিকীকরণ এবং লক্ষ্য পরীক্ষা অন্তর্ভুক্ত।
ক্রিয়া স্বয়ংক্রিয় (সংজ্ঞা २७): প্রতিটি ক্রিয়া একটি স্বয়ংক্রিয়ের সাথে সামঞ্জস্যপূর্ণ, নিম্নলিখিত মূল রূপান্তর অন্তর্ভুক্ত:
প্রধান স্বয়ংক্রিয় এবং সমস্ত ক্রিয়া স্বয়ংক্রিয় একটি সময়গত স্বয়ংক্রিয় নেটওয়ার্কে একত্রিত করা হয় (সংজ্ঞা २८), প্রাথমিক কনফিগারেশন সমস্ত স্বয়ংক্রিয় নিষ্ক্রিয় অবস্থায় সেট করা হয়।
१. সমসাময়িক সম্পাদন সমর্থন: হেইনজ এবং অন্যদের বৈশ্বিক লক ব্যবহারের বিপরীতে, এই পত্রিকা সমসাময়িক স্ন্যাপশট ক্রিয়া সম্পাদন অনুমতি দিতে ঘড়ি সীমাবদ্ধতা ব্যবহার করে २. তাৎক্ষণিক ক্রিয়া প্রক্রিয়াকরণ: iea রূপান্তর যোগ করার মাধ্যমে শূন্য স্থায়িত্বের তাৎক্ষণিক ক্রিয়া সমর্থন করে ३. আনুপচারিক যাচাইকরণ: প্রথমবারের মতো এই ধরনের এনকোডিংয়ের জন্য মেশিন-চেক করা সঠিকতা প্রমাণ প্রদান করে ४. শব্দার্থ সরলীকরণ: আনুপচারিক যুক্তির জন্য আরও উপযুক্ত সময়গত পরিকল্পনা শব্দার্থ ডিজাইন করা হয়েছে
| উপাদান | কোড লাইন |
|---|---|
| বিমূর্ত সময়গত পরিকল্পনা শব্দার্থ আনুপচারিকীকরণ | ~७,२०० |
| মুন্তা ব্যবহার করে সময়গত স্বয়ংক্রিয় নেটওয়ার্ক সংজ্ঞা | ~८०० |
| উপপাদ্য १ এবং সম্পর্কিত লেম্মার প্রমাণ | ~८,५०० |
| তালিকা সম্পর্কিত লেম্মা | ~१,५०० |
| মোট | ~१८,००० |
সম্পর্কিত আনুপচারিক কাজের স্কেলের সাথে তুলনা:
উপপাদ্য १ (প্রধান সঠিকতা উপপাদ্য): যদি পরিকল্পনা π বৈধ এবং স্ব-অতিক্রমণ মুক্ত হয় (valid(π) ∧ no_self_overlap(π)), তাহলে দাবি A ⊨ EF(loc(AM) = goal) সত্য।
প্রমাণ কাঠামো: १. লেম্মা १: সমান্তরাল পরিকল্পনা চালানো অনুকরণ করার নির্মাণ २. লেম্মা २: প্রাথমিক কনফিগারেশন থেকে এনকোডেড অবস্থায় পৌঁছানোযোগ্যতা ३. লেম্মা ३: চূড়ান্ত অবস্থা থেকে লক্ষ্য কনফিগারেশনে রূপান্তর
१. সম্পূর্ণতা প্রমাণ: এনকোডিংয়ের সম্পূর্ণতা সফলভাবে প্রমাণ করা হয়েছে, অর্থাৎ প্রতিটি বৈধ পরিকল্পনা সংশ্লিষ্ট সময়গত স্বয়ংক্রিয় নেটওয়ার্কে একটি বৈধ চলা খুঁজে পায় २. মেশিন চেক: সমস্ত প্রমাণ ইসাবেল/এইচওএলের মেশিন চেক পাস করেছে, সর্বোচ্চ স্তরের বিশ্বাসযোগ্যতা নিশ্চয়তা প্রদান করে ३. মডুলার ডিজাইন: প্রমাণ কাঠামো মডুলার, বোঝা এবং রক্ষণাবেক্ষণ সহজ করে
এনকোডিং বাস্তবায়ন বিদ্যমান যাচাইকৃত প্রমাণপত্র চেকারের সাথে সামঞ্জস্যপূর্ণ ফর্ম্যাটে অভিযোজিত হয়েছে, একটি সম্পূর্ণ সম্পাদনযোগ্য প্রমাণপত্রকরণ শৃঙ্খল গঠন করে।
१. সম্ভাব্যতা যাচাইকরণ: সময়গত পরিকল্পনা অসমাধানযোগ্যতার আনুপচারিক প্রমাণপত্রকরণ সম্ভব প্রমাণ করেছে २. তাত্ত্বিক নিশ্চয়তা: উপপাদ্য প্রমাণকারীর মাধ্যমে শক্তিশালী সঠিকতা নিশ্চয়তা প্রদান করেছে ३. প্রকৌশল বাস্তবায়ন: সম্পূর্ণ প্রমাণপত্রকরণ সরঞ্জাম শৃঙ্খল সফলভাবে নির্মাণ করেছে
१. ইনপুট সীমাবদ্ধতা: বর্তমানে শুধুমাত্র ইতিমধ্যে উদাহরণকৃত সময়গত পরিকল্পনা সমস্যা ইনপুট হিসাবে গ্রহণ করে २. শব্দার্থ সাবসেট: সমর্থিত শব্দার্থ যাচাইকৃত পরিকল্পনা যাচাইকারীর একটি সাবসেট ३. সম্পাদনযোগ্যতা: প্রমাণপত্রকরণ প্রক্রিয়া এখনও সম্পূর্ণরূপে সম্পাদনযোগ্য নয়
१. সমতা প্রমাণ: এই পত্রিকার শব্দার্থ এবং বিদ্যমান যাচাইকারীর শব্দার্থের সমতা আনুপচারিকভাবে প্রমাণ করার পরিকল্পনা করছে २. সম্পাদনযোগ্য বাস্তবায়ন: সম্পাদনযোগ্য প্রমাণপত্র চেকার বিকাশ করা ३. উদাহরণকরণ যাচাইকরণ: উদাহরণকরণ অ্যালগরিদম, যেমন হেলমার্টের ডেটালগ সমাধানকারী আনুপচারিকভাবে যাচাই করা ४. সীমাবদ্ধতা শিথিলকরণ: স্ব-অতিক্রমণ মুক্ত শর্ত শিথিল করার সম্ভাবনা অধ্যয়ন করা
१. তাত্ত্বিক কঠোরতা: প্রথমবারের মতো সময়গত পরিকল্পনা অসমাধানযোগ্যতা প্রমাণপত্রকরণের জন্য মেশিন-চেক করা আনুপচারিক প্রমাণ প্রদান করেছে २. প্রকৌশল সম্পূর্ণতা: শুধুমাত্র তাত্ত্বিক কাঠামো প্রদান করে না, বরং বিদ্যমান সরঞ্জামগুলির সাথে একীকরণ বাস্তবায়ন করেছে ३. পদ্ধতি উদ্ভাবনী:
१. ব্যবহারিক সীমাবদ্ধতা:
१. একাডেমিক অবদান:
२. ব্যবহারিক মূল্য:
३. পুনরুৎপাদনযোগ্যতা: খোলা উৎস ইসাবেল/এইচওএলের উপর ভিত্তি করে, তাত্ত্বিকভাবে সম্পূর্ণরূপে পুনরুৎপাদনযোগ্য
१. গুরুত্বপূর্ণ সিস্টেম: উচ্চ বিশ্বাসযোগ্যতা নিশ্চয়তা প্রয়োজন এমন পরিকল্পনা অ্যাপ্লিকেশন (যেমন বিমান চলাচল, চিকিৎসা ডিভাইস) २. গবেষণা সরঞ্জাম: সময়গত পরিকল্পনা গবেষণার জন্য আনুপচারিক যাচাইকরণ অবকাঠামো প্রদান করে ३. শিক্ষা উদ্দেশ্য: আনুপচারিক পদ্ধতি এবং পরিকল্পনা অ্যালগরিদম শিক্ষার জন্য কেস স্টাডি হিসাবে ४. সরঞ্জাম উন্নয়ন: বিশ্বাসযোগ্য পরিকল্পনা সরঞ্জাম বিকাশের জন্য তাত্ত্বিক ভিত্তি প্রদান করে
মূল সংদর্ভগুলির মধ্যে রয়েছে:
এই পত্রিকা সময়গত পরিকল্পনার আনুপচারিক যাচাইকরণ ক্ষেত্রে গুরুত্বপূর্ণ অবদান রাখে, যদিও ব্যবহারিক দিক থেকে উন্নতির জায়গা রয়েছে, তবে এর তাত্ত্বিক কঠোরতা এবং পদ্ধতি উদ্ভাবনী এই ক্ষেত্রের উন্নয়নের জন্য একটি দৃঢ় ভিত্তি স্থাপন করেছে।