মেটাস্টেবল ব্যর্থতার জন্য একটি নীতিভিত্তিক সমাধানের আমার অনুসন্ধান আমাকে স্ব-স্থিতিশীলতায় ফিরিয়ে এনেছে। একটি সাম্প্রতিক গবেষণাপত্র সমস্যাটিকে স্ব-স্থিতিশীল সিস্টেমের সংযোজনের সাথে সম্পর্কিত করেছে, কিন্তু সাহিত্য অনুসন্ধান কোনো উপকারী কিছু দেয়নি। ২০০০-এর দশকের গোড়ার দিকে স্তরযুক্ত স্থিতিশীলতা ইতিমধ্যেই বিদ্যমান ছিল, এবং তারপর থেকে মৌলিক কিছু যোগ করা হয়নি বলে মনে হয়।

আমি একটি নির্দিষ্ট উদাহরণ ব্যবহার করে সমস্যাটি আক্রমণ করেছি: চুক্তিসহ দুটি উপাদান হিসাবে একটি পুনঃপ্রচেষ্টা ঝড়ের নির্ভর-গ্যারান্টি TLA+ মডেল। সেই মডেলটি মেটাস্টেবল ব্যর্থতা পুনরুৎপাদন করে কারণ সংযোজন ভাল অবস্থা থেকে কাজ করেছিল কিন্তু ব্যর্থ হয়েছিল যখন একটি বড় ধাক্কা ভিত্তি কেসটি সরিয়ে দেয়। প্রতিটি অবস্থা থেকে নির্ভর-গ্যারান্টি সংযোজন খুঁজতে গিয়ে Kim, Arcak এবং Seshia-এর ২০১৭ সালের নিয়ন্ত্রণ তত্ত্বের একটি গবেষণাপত্র, "A Small Gain Theorem for Parametric Assume-Guarantee Contracts" পাওয়া গেল। এই গবেষণাপত্রটি মোটামুটি আমার যা চাই তা করে: স্তর বা ব্লকিং ছাড়াই দুটি উপাদানের মধ্যে বৃত্তাকার যুক্তি নিষ্কাশন। কিন্তু এটির গুরুতর সীমাবদ্ধতা রয়েছে। একটি উপাদান সংকেতের উপর একটি ইনপুট-আউটপুট সম্পর্ক, এবং চুক্তিগুলি একটি ইনপুট সীমাকে একটি আউটপুট সীমার সাথে সম্পর্কিত করে। এই স্মৃতিহীন দৃষ্টিভঙ্গি পূর্ববর্তী রাউন্ড থেকে জমা হওয়া ব্যাকলগ প্রকাশ করতে পারে না, যা সারিগুলিকে বাদ দেয়। এটির স্থিতিশীলতার সাথে কোনো সংযোগও নেই।

তবুও, স্ব-স্থিতিশীলতা এবং মেটাস্টেবিলিটির একটি সংযোজন তত্ত্বের দিকে কিছু টুকরো চুরি করার মতো। নীচে আমি এটি কাজ করার চেষ্টা করি... কিছুটা অসফলভাবে।

আমাদের মূল মডেলে, পুনঃপ্রচেষ্টাকারীর গ্যারান্টি শর্তসাপেক্ষ ছিল: "যদি সারিটি 6-এর নীচে থাকে, আমি কোনো পুনঃপ্রচেষ্টা পাঠাই না"। প্যারামেট্রিক অনুমান-গ্যারান্টি গবেষণাপত্রের বড় ধারণা হল সর্বত্র কভার করে এমন চুক্তির একটি পরিবার লেখা। ধ্রুবক: S=3 সার্ভার ক্ষমতা, A_max=2 নতুন আগমন, T=2 টাইমআউট, লেটেন্সি থ্রেশহোল্ড S·T=6। এটি দেয় λ(L) = ⌊(L-6)/2⌋। পুরানো চুক্তিটি শীর্ষ সারি: λ(6)=0। প্রতিটি সারি একটি প্রতিশ্রুতি পায়, তাই আমরা সাধারণ চুক্তির একটি বান্ডেল পাই, প্রতিটি মন্দতা স্তর p-এর জন্য একটি: φ_a = ∨_p ψ_a(p); φ_g = ∧_p (ψ_a(p) ⇒ ψ_g(λ(p)))। অনুমান দিকটি একটি বিচ্ছেদ কারণ স্তরগুলি বিকল্প। গ্যারান্টি দিকটি একটি সংযোজন; বাধ্যবাধকতাগুলি সঞ্চয়ী। যে সারিগুলির শর্ত মিথ্যা তাদের কোনো খরচ নেই; নেস্টেড স্তর মানে সবচেয়ে কঠোরটি জয়ী হয়।

মূল সত্তা: ব্যক্তি: Kim, Arcak, Seshia