Complete Supermartingale Certificates for $\omega$-Regular Properties

ملخص تقني: شهادات السوبرمارتينجال الكاملة لخصائص $\omega$-المنتظمة

بيان المشكلة
تتناول الورقة البحثية التحقق الرسمي من الأنظمة الاحتمالية التي تُنمذج كسلاسل ماركوف متجانسة زمنياً عبر فضاءات حالات عامة (قد تكون غير قابلة للعد). وتستهدف الورقة تحديداً التحقق من خصائص التفاعلية (Reactivity Properties)، وهي فئة من الخصائص الزمنية التي تشمل المنطق الزمني الخطي (LTL) وتُعبر عن اللغات $\omega$-المنتظمة. تُعرف التفاعلية بأنها اقتران منتهٍ لشروط قبول "ستريت" (Streett acceptance conditions)، حيث يتطلب كل شرط إما زيارة مجموعة من الحالات $A$ لعدد من المرات المحدودة، أو زيارة مجموعة من الحالات $B$ لعدد لا نهائي من المرات ($Fin(A) \cup Inf(B)$).

بينما تم إثبات أن شهادات السوبرمارتينجال (Supermartingale certificates) هي أدوات سليمة وكاملة لـ التوقف شبه المؤكد (Almost-sure termination) (وهي خاصية تفاعلية محددة)، إلا أن قواعد الإثبات الحالية للتفاعلية العامة وخصائص $\omega$-المنتظمة تعاني من قصور حرج: فهي توفر فقط شروطاً كافية. وبناءً على ذلك، قد تفشل هذه القواعد في إثبات صحة الأنظمة التي تحقق الخاصية بالفعل. علاوة على ذلك، فإن المحاولات السابقة لتحقيق الاكتمال للتفاعلية اعتمدت على دالات قيم قادرة على التعبير عن توزيعات عشوائية اختيارية، مما يجعلها صعبة الأتمتة. تسعى هذه الورقة إلى بناء قواعد إثبات تكون سليمة وكاملة (وتحديداً ذات قيم قياسية/scalar-valued) للتفاعلية، بحيث تكون قابلة للتطبيق على فضاءات الحالات ذات اللانهاية القابلة للعد وفضاءات الحالات العامة القابلة للقياس.

المنهجية: تفكيك المناطق الماصة (Absorbing-Region Decomposition)
تتمثل المساهمة التقنية الجوهرية في منهجية تعمل على تفكيك أي خاصية تفاعلية إلى مجموعة من الالتزامات البسيطة والمستقلة. يعتمد هذا التفكيك على تحديد نوعين من المناطق لكل زوج "ستريت" $(A_i, B_i)$:

1. ثابت عالمي ($I$): منطقة في فضاء الحالات يظل النظام داخلها باحتمالية عالية (أو باحتمالية 1 في حالة شبه التأكد).
2. مناطق امتصاص ($J_i$): لكل زوج $i$، توجد منطقة $J_i \subseteq I \setminus A_i$ تعمل كـ "فخ" حيث تكون احتمالية العودة إلى $A_i$ أقل تماماً من 1.

يعمل التفكيك على اختزال التحقق من خاصية التفاعلية العالمية إلى ثلاثة أنواع متميزة من الالتزامات:

• السلامة النوعية (Qualitative Safety): ضمان أنه لكل $i$، تكون احتمالية العودة من $J_i$ إلى $A_i$ محدودة من الأسفل بأقل من 1 (أي أن $J_i$ منطقة امتصاص بالنسبة لـ $A_i$).
• التوقف شبه المؤكد (Almost-Sure Termination): ضمان أنه من أي حالة في الثابت $I$، يتوقف النظام شبه مؤكد في اتحاد مجموعة الهدف $B_i$، والمنطقة الماصة $J_i$، ومتمم الثابت $I^c$.
• السلامة الكمية (Quantitative Safety): وضع حد أدنى لاحتمالية بقاء النظام داخل الثابت $I$ إلى الأبد.

يثبت المؤلفون أنه لأي سلسلة ماركوف متجانسة زمنياً تحقق خاصية تفاعلية، توجد دائماً مناطق امتصاص وثابت مناسب. في الحالة الكمية العامة، يمكن اختيار الثابت بحيث تقترب احتمالية الثبات فيه من احتمالية الخاصية التفاعلية ضمن قيمة $\epsilon$ اختيارية. وفي حالة شبه التأكد، يمكن اختيار الثابت بحيث يمثل الخاصية بدقة.

المساهمات والنتائج الرئيسية

1. نظريات التفكيك: تثبت الورقة أن كل خاصية تفاعلية تقبل التفكيك إلى التزامات سلامة نوعية، وتوقف شبه مؤكد، وسلامة كمية.

   • النظرية 3.7 (السلامة): إذا قبلت سلسلة ماركوف ثابتاً $I$ ومناطق امتصاص $J_i$ تحقق شروطاً محددة، فإن احتمالية تحقيق الخاصية التفاعلية هي على الأقل احتمالية البقاء في $I$ للأبد.
   • النظرية 3.12 ($\epsilon$-الاكتمال): لأي خاصية تفاعلية باحتمالية $p > 0$، ولأي $\epsilon > 0$، يوجد ثابت ومناطق امتصاص بحيث تكون احتمالية الثبات لا تقل عن $p - \epsilon$.
   • النظرية 3.14 (الاكتمال شبه المؤكد): إذا تحققت الخاصية التفاعلية شبه مؤكد (احتمالية 1)، يوجد ثابت ومناطق امتصاص بحيث تكون احتمالية الثبات هي 1 تماماً.

2. التطبيق باستخدام شهادات السوبرمارتينجال: يقوم المؤلفون بتطبيق هذا التفكيك باستخدام قواعد إثبات سليمة وكاملة موجودة مسبقاً للتوقف شبه المؤكد على فضاءات الحالات ذات اللانهاية القابلة للعد. ومن خلال الجمع بين هذه القواعد والنتائج القياسية للسلامة الكمية، يستنتجون قاعدتين جديدتين للإثبات (قاعدة الإثبات رقم 1 وقاعدة الإثبـاث رقم 2) للتفاعلية.

   • تستخدم هذه القواعد شهادات سوبرمارتينجال ذات قيم قياسية (دالات قيمة) لالتزامات السلامة والتوقف.
   • النظريات 4.4–4.6 و4.8–4.10: تثبت هذه النظريات أن قواعد الإثبات الجديدة سليمة و$\epsilon$-كاملة للتفاعلية الكمية، وكاملة تماماً للتفاعلية شبه المؤكدة، وتحديداً لفضاءات الحالات ذات اللانهاية القابلة للعد.

3. دحض العمل السابق: توضح الورقة أن شهادات السوبرمارتينجال السابقة لخصائص $\omega$-المنتظمة غير كاملة. باستخدام مثال "كازينو الإقراض" (Lending Casino)، تظهر الورقة حالة يحقق فيها النظام خاصية تفاعلية بشكل شبه مؤكد، ولكن الوقت المتوقع للوصول إلى حالة حرجة هو مالانهاية، مما يؤدي إلى فشل القواعد السابقة (التي تعتمد على القيم المتوقعة النهائية). يعالج التفكيك المقترح هذا الأمر من خلال فصل التزام السلامة (احتمالية العودة المحدودة) عن التزام التوقف.

الأهمية والادعاءات
تدعي الورقة أنها تقدم أول شهادات سوبرمارتينجال سليمة وكاملة لخصائص $\omega$-المنتظمة شبه المؤكدة، وأول شهادات سليمة و$\epsilon$-كاملة للخصائص $\omega$-المنتظمة الكمية على سلاسل ماركوف متجانسة زمنياً ذات فضاءات حالات قابلة للعد لا نهائياً.

تكمن الأهمية في سد الفجوة بين التحليل العشوائي ونظرية اللغات الشكلية. من خلال إثبات أن التفاعلية يمكن تفكيكها إلى التوقف والسلامة، تمكن المؤلفون من أتمتة التحقق من الخصائص $\omega$-المنتظمة المعقدة باستخدام التقنيات الموجودة للشهادات ذات القيم القياسية. ويشير المؤلفون إلى أنه بينما تنطبق ضمانات الاكتمال الخاصة بهم حالياً على فضاءات الحالات ذات اللانهاية القابلة للعد، فإن استراتيجية التفكيك الأساسية صالحة لفضاءات الحالات العامة، مما يشير إلى أن توسيع الاكتمال ليشمل الفضاءات غير القابلة للعد يختزل في مشكلة شهادة التوقف شبه المؤكد عبر الفضاءات العامة. لا تدعي الورقة حل مسألة تخليق (synthesis) هذه الشهادات تلقائياً، بل توفر الأساس النظري للقيام بذلك.