Time-Varying Reach-Avoid Control Certificates for Stochastic Systems

إليك ملخص تقني مفصل لورقة البحث بعنوان "شهادات التحكم المتغيرة زمنياً للوصول-التجنب للأنظمة العشوائية" (Time-Varying Reach-Avoid Control Certificates for Stochastic Systems).

1. صياغة المشكلة

تتناول الورقة مشكلة "الوصول-التجنب" (Reach-Avoid) للأنظمة العشوائية ذات الزمن المنفصل والفضاء المستمر ذات الديناميكيات متعددة الحدود. يتم تعريف النظام كالتالي:
$$x_{k+1} = f(x_k, u_k, w_k)$$
حيث $x$ هو الحالة، و$u$ هو مدخل التحكم، و$w$ هو اضطراب عشوائي مستقل ومتماثل التوزيع (i.i.d.).

الهدف هو ضمان أن المسارات التي تبدأ من مجموعة أولية $X_0$ تصل إلى مجموعة الهدف $X_r$ خلال أفق زمني $H$ (محدود أو غير محدود) مع تجنب مجموعة غير آمنة $X_u$ (حيث $X_u = X \setminus X_s$، و$X_s$ هي المجموعة الآمنة).

تعالج الورقة مشكلتين محددتين:

1. التحقق (Verification): بالنظر إلى متحكم $\pi$، التحقق مما إذا كان احتمال استيفاء خاصية الوصول-التجنب لا يقل عن عتبة $\delta$.
2. تخليق التحكم (Control Synthesis): تخليق متحكم تغذية راجعة $\pi^*$ يعظم الحد الأدنى لاحتمال الوصول-التجنب.

التحديات: المشكلة غير قابلة للحل حسابياً بسبب فضاءات الحالة/الأفعال المستمرة، والديناميكيات غير الخطية، واللايقين العشوائي، والحاجة إلى التفكير في الأمان والوصول في آن واحد. تعتمد الطرق الحالية غالباً على التجريد المحدود (مما يؤدي إلى لعنة الأبعاد) أو التعلم العميق (الذي يفتقر إلى الضمانات الرسمية).

2. المنهجية

يقترح المؤلفون إطار عمل قائماً على الشهادات (Certificate-based framework) يستند إلى البرمجة الديناميكية (DP) وتحسين مجموع المربعات (SOS).

أ. شهادات الوصول-التجنب

بدلاً من حساب دالة القيمة بدقة (وهو أمر مستعصٍ)، يقدم المؤلفون دوالاً حقيقية (شهادات) توفر حداً أدنى محافظاً لاحتمال الوصول-التجنب. يقترحون صيغتين:

1. الشهادات المتغيرة زمنياً ($R(x, k)$):

   • قابلة للتطبيق في كل من الآفاق المحدودة وغير المحدودة.
   • تتطور الشهادة عبر الخطوات الزمنية $k$.
   • الشروط: يجب أن تحقق الدالة الشروط الحدية على $X_r$ (الهدف)، و$X_u$ (غير الآمن)، و$X_0$ (الأولي)، بالإضافة إلى متباينة تكرارية تتضمن القيمة المتوقعة للخطوة التالية.
   • الاسترخاء (Relaxation): للتعامل مع صعوبة فرض دوال المؤشر الدقيقة (0 أو 1) باستخدام كثيرات حدود مستمرة، قدم المؤلفون متغيرات إضافية ($\alpha, \beta$) لتخفيف القيود. يضمن ذلك بقاء مسألة التحسين قابلة للحل.
   • النتيجة: يتم خفض احتمال الوصول-التجنب بـ $\gamma - (\alpha_H + \sum \beta_i)$.

2. الشهادات الثابتة زمنياً ($R(x)$):

   • تستخدم دالة واحدة لجميع الخطوات الزمنية.
   • أبسط حسابياً ولكنها قد تكون أكثر تحفظاً.
   • للآفاق غير المحدودة، تعتمد على خصائص تشبه "المرتسمات الفائقة" (supermartingale).
   • النتيجة: يتم خفض الاحتمال بـ $\gamma - \alpha - H\beta$ (للحالات المحدودة) أو $\gamma - \alpha$ (للحالات غير المحدودة).

ب. إطار تحسين مجموع المربعات (SOS Optimization)

لجعل التحسين الدالي قابلاً للحل حسابياً، يقيد المؤلفون الشهادات (والمتحكمات) لتكون دوال متعددة الحدود.

• التحقق: يتم ترجمة شروط الشهادات إلى قيود البرمجة شبه المحددة (SDP) باستخدام استرخاءات SOS ونظرية "بوتينار" للمواضع (Putinar's Positivstellensatz). يحول هذا المسألة إلى مسألة تحسين محدبة.
• التخليق المشترك: بالنسبة لتخليق المتحكم، يصيغ المؤلفون مسألة (min-max) (تقليل عبر بارامترات المتحكم، وتعظيم عبر أسوأ الحالات الممكنة للحالات). يستخدمون استرخاء SOS مزدوج (بناءً على مصفوفات العزوم) لتحويل هذه المسألة غير المحدبة (min-max) إلى برنامج SOS محدب. يتيح ذلك التخليق المشترك للمتحكم الأمثل والشهادة الخاصة به.

3. المساهمات الرئيسية

1. إطار عمل موحد للشهادات: صياغة مبتكرة لشهادات الوصول-التجنب للأنظمة العشوائية تغطي كل من الحالات المتغيرة زمنياً والثابتة زمنياً، وهي قابلة للتطبيق في كل من الآفاق المحدودة وغير المحدودة.
2. التخليق المحدب: طريقة لتخليق متحكم التغذية الراجعة والشهادة بشكل مشترك باستخدام تحسين SOS، مما يتجنب الحاجة إلى الاستدلالات غير المحدبة أو التحقق من التعلم العميق.
3. حدود أكثر دقة عبر الاسترخاء: إن إدخال المتغيرات الإضافية ($\alpha, \beta$) يسمح بصيغ SOS قابلة للحل تكون أقل تحفظاً من مقاربات دوال الحاجز الصارمة السابقة (مثل [8]، [19]).
4. تحليل القابلية للتوسع: توضح الورقة أنه بينما تكون الشهادات الثابتة زمنياً أقل تكلفة حسابياً لكل خطوة، فإن الشهادات المتغيرة زمنياً توفر حدوداً احتمالية أكثر دقة وقابلية أفضل للتوسع في الأنظمة عالية الأبعاد باستخدام كثيرات حدود ذات درجات أقل عبر خطوات زمنية متعددة.

4. النتائج التجريبية

تم التحقق من إطار العمل على عدة نماذج مرجعية، بما في ذلك الأنظمة الخطية (1D/2D/3D)، والخرائط الانكماشية، ونموذج طائرة، وأنظمة درجة حرارة الغرفة.

• المقارنة مع أحدث ما توصل إليه العلم:
  • مقابل [8] (ثابت زمنياً، أفق غير محدود): حققت الطريقة المقترحة حدود احتمالية أعلى بكثير (على سبيل المثال، 0.96 مقابل 0.16 في نظام خطي 1D) ونجحت في الحالات التي فشلت فيها [8].
  • مقابل [19] (أفق محدود): وفرت صياغة المتغيرات الزمنية المقترحة حدوداً أكثر دقة بشكل كبير عند درجات متعددة حدود أقل.
• المتغيرة زمنياً مقابل الثابتة زمنياً:
  • المتغيرة زمنياً: قدمت باستمرار احتمالات حد أدنى أعلى. في الأنظمة عالية الأبعاد (مثل طائرة ثلاثية الأبعاد 3D)، حققت شهادة متغيرة زمنياً بدرجة 6 حداً قدره 0.98، بينما تطلبت النهج الثابت زمنياً درجة 24 لتحقيق حد غير ضئيل.
  • المقايضة: تفرض الشهادات المتغيرة زمنياً تكاليف حسابية أعلى بسبب عدد الخطوات الزمنية، لكنها تتجنب الانفجار الأسي للمتغيرات المرتبط بالدرجات العالية لكثيرات الحدود المطلوبة في المنهج الثابت زمنياً.
• تخليق التحكم: نجح التخليق المشترك في تصميم متحكمات رفعت احتمالات الوصول من قرب الصفر (في حالة الحلقة المفتوحة) إلى أكثر من 0.95 في سيناريوهات مختلفة.

5. الأهمية

يملأ هذا العمل الفجوة بين التحقق الرسمي وتخليق التحكم للأنظمة العشوائية ذات الفضاءات المستمرة.

• الصرامة النظرية: يوفر ضمانات احتمالية رسمية دون اللجوء إلى تقسيم فضاء الحالة (discretization)، وهو أمر بالغ الأهمية للأنظمة عالية الأبعاد.
• العملية: من خلال الاستفيد من تحسين SOS المحدب، يقدم بديلاً قابلاً للتنفيذ حسابياً للطرق غير المحدبة أو التعلم العميق، والتي تفتقر غالباً إلى ضمانات أمان يمكن التحقق منها.
• المرونة: القدرة على الاختيار بين الشهادات المتغيرة زمنياً (أكثر دقة، وأعلى تكلفة) والثابتة زمنياً (أقل دقة، وأقل تكلفة) تسمح للممارسين بضبط النهج بناءً على قيود النظام المحدد والموارد الحسابية المتاحة.

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