Value Functions for Temporal Logic: Optimal Policies and Safety Filters

ملخص تقني: دوال القيمة للمنطق الزمني: السياسات المثلى ومرشحات السلامة

بيان المشكلة
بينما تُعد معادلات بلمان (Bellman equations) لمسائل الوصول (reach)، والتجنب (avoid)، والوصول-التجنب (reach-avoid) الأساسية معروفة جيداً، إلا أن العلاقة بين أمثلية القيمة (value optimality) وأمثلية السياسة (policy optimality) تصبح دقيقة ومعقدة في الإعدادات غير المخصومة ذات الأفق اللانهائي (undiscounted infinite-horizon)، لا سيما بالنسبة للمواصفات الزمنية (Temporal Logic) المعقدة. تظهر حالة مرضية حرجة حيث يمكن لتعظيم دالة Q (Q-function) بشكل جشع (greedily) أن ينتج سياسات تؤدي إلى تأجيل إتمام المهمة إلى أجل غير مسمى في مسائل "الوصول-التجنب" (المكافئة لمواصفات حتى - Until)، حتى عندما تكون دالة القيمة نفسها مثالية. يحدث هذا لأن تسلسل الإجراءات الأمثل للمسارات اللانهائية هو بطبيعته غير ماركوفي (non-Markovian)؛ إذ قد يحتاج المدخل الأمثل إلى "التحول" من تعظيم القيمة الحالية إلى قيمة مكونة في رسم بياني تحليلي (decomposition graph) للوفاء بالمواصفات اللانهائية المتبقية. وتواجه الطرق الحالية، مثل توسيع الحالة (state-augmentation) للمسائل ذات الأهداف المزدوجة، صعوبة في التعميم لتشمل الصيغ التي تتضمن عمليات متداخلة من حتى (Until)، والتالي (Next)، وعالمياً (Globally)، وعالمياً-حتى (Globally-Until). علاوة على ذلك، هناك حاجة لمرشحات سلامة تضمن الوفاء بمواصفات المنطق الزمني المعقدة، بما يتجاوز مجرد مهام التجنب أو الوصول-التجنب البسيطة.

المنهجية
يقترح المؤلفون إطار عمل يعمم دوال القيمة وQ على تاريخ الحالات (state histories) للتعامل مع الطبيعة غير المار كوفية للمسألة. تعتمد المنهجية على التفكيك الجبري لدالة القيمة للمنطق الزمني إلى رسم بياني من دوال القيمة المكونة.

1. دوال القيمة غير المار كوفية: تُعرف الورقة دوال القيمة المثلى $V^*$ ودوال Q المثلى $Q$ على تاريخ الحالات $x_{0:t}$ بدلاً من الحالات الحالية فقط. وهذا يسمح للسياسة بمراعاة التاريخ المطلوب للوفاء بالقيود الزمنية.
2. الأنظمة المعززة زمنياً وزمن الشاهد (Witness Times): لمعالجة مشكلة التأجيل في مواصفات حتى ($U$)، يقدم المؤلفون نظاماً معززاً زمنياً مع مؤقت. ويُعرفون "زمن الشاهد الأمثل" $\sigma^*$، وهو أول زمن يحقق فيه المسار أفضل درجة متانة (robustness score). يسمح هذا ببناء سياسات تتحول من استراتيجية جشعة ذات أفق محدود (تعظيم دالة Q ضمن زمن الشاهد) إلى سياسة لاحقة (suffix policy) تحقق الجزء المتبقي من الصيغة الفرعية.
3. بناء السياسة التركيبي (Compositional Policy Construction): تبني الورقة سياسات مثلى لشريحة محددة من صيغ المنطق الزمني (التعريف 3)، والتي تشمل:
   • الصيغ الاقتراحية (Propositional formulas).
   • معاملات حتى ($p U \phi$)، والتالي ($X\phi$)، وعالمياً ($Gp$).
   • معاملات عالمياً-حتى ($G(\bigvee p_i U r_i)$)، والتي تشفر معايير قبول بوشي (Büchi acceptance criteria).
   • التشتت (Disjunctions) والاقتران الاقتراحي (Propositional conjunctions).
     يفترض البناء وجود سياسات مثلى للصيغ الفرعية (الافتراض 2) ويقوم بدمجها بشكل تكراري. وبالنسبة لـ عالمياً-حتى، تقوم السياسة بزيارة كل مكون "حتى" بالتتابع لضمان الزيارات اللانهائية لمجموعات الحالات المطلوبة.
4. ترشيح السلامة (Safety Filtering): يوضح المؤلفون أن دالة Q يمكن أن تعمل كمرشح سلامة. حيث يُعرفون مجموعة الفشل التي لا يمكن فيها تحقيق المواصفات بمتانة غير سالبة. ويُقترح مخطط تدخل هو الأقل تقييداً: إذا كان إجراء السياسة الاسمية (nominal policy) يؤدي إلى قيمة Q غير سالبة (مما يشير إلى قابلية التحقيق في المستقبل)، فإنه يُسمح به؛ وإلا، ينتقل النظام إلى الإجراء الذي يعظم دالة Q. وتحت افتراضات محددة (مثل غياب معاملات حتى غير المحدودة)، يضمن هذا المرشح الوفاء بالمواصفات.

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

1. تعميم دوال القيمة: تعمم الورقة دالة القيمة المثلى ودالة Q على تاريخ الحالات (التعريف 1) وتعرف الأمثلية على التاريخ (التعريف 2)، مما يعالج الطبيعة غير المار كوفية لمسائل المنطق الزمني ذات الأفق اللانهائي.
2. السياسات المثلى التركيبية: بالنسبة لفئة واسعة من صيغ المنطق الزمني (التعريف 3)، يبني المؤلفون سياسات مثلى تركيبية لمقياس المتانة المرتبط بها (النظريات 1-8). ويتضمن ذلك التعامل مع مشكلة التأجيل في مواصفات حتى وعالمياً-حتى.
3. مرشحات السلامة الأقل تقييداً: توضح الورقة أن دالة Q عبر (التواريخ التي قد تكون غير مثلى) توفر مرشح سلامة أقل تقييداً للسياسة الاسمية (النظريات 9، 10). يضمن هذا المرشح الوفاء بالمواصفات مع احترام المسار السابق للسياسة الاسمية، بشرما كانت الصيغة تستوفي قيوداً هيكلية معينة.

النتائج والتجارب
تتحقق الورقة من إطار العمل المقترح من خلال البراهيا النظرية وتجربتين برمجيتين/عتادية:

• بيئة الشبكة ثنائية الوكيل (Two-Agent GridWorld): يحل المؤلفون مسألة مشتركة من الحالة-الفعل رباعية الأبعاد بمواصفات معقدة تتضمن قيود الوصول المحدودة زمنياً، والسلامة، والحيوية. ويظهرون أن السياسة المشتقة ($\pi_{spec}$) توجه النظام بنجاح لتحقيق المواصفات. علاوة على ذلك، عند استخدامها كمرشح لسياسات اسمية لـ "القهوة" و"الشاي" (اللذين يفشل كل منهما بمفرده في تحقيق المواصفات المشتركة)، يضمن المرشح تحقيق المهمة المعقدة للنظام المشترك، بينما يؤدي مرشح "السلامة فقط" التقليدي إلى حالة جمود وفشل.
• طائرة بدون طيار أحادية الوكيل (Single-Agent Drone): باستخدام طائرة "Crazyflie" بدون طيار، يوضح المؤلفون السياسة في مهمة ملاحة مع عوائق. يوجه مرشح المنطق الزمني المقترح الطائرة بنجاح إلى موقع العمل مع الوفاء بمواصفات زمنية معقدة (مثل الدوران عبر مناطق محددة، وتجنب الجدران). وفي المقابل، فإن السياسة الاسمية غير المفلترة أو المرشح القائم على قيود السلامة فقط يؤدي إلى وقوع الطائرة في فخ أو اصطدامها.

الأهمية
تزعم الورقة أنها تقدم نهجاً عملياً لتوليد سياسات مثلى لقيمة فئة واسعة من صيغ المنطق الزمني من خلال توسيع نتائج التفكيك الحديثة. تكمر أهميتها الرئيسية في حل المشكلة المرضية حيث يفشل تعظيم Q الجشع في المهام ذات الأفق اللانهائي، وفي توفير آلية لتخليق مرشحات سلامة تضمن تحقيق المهام المعقدة، وليس السلامة فحسب. ومن خلال توسيع نطاق الصيغ القابلة للحل لتشمل مواصفات حتى المتداخلة وعالمياً-حتى، يعمل هذا العمل على سد الفجوة بين وصول هاميلتون-جاكوبي (Hamilton-Jacobi reachability) والتعلم المعزز (Reinforcement Learning) للمهام الزمنية المعقدة والحساسة للسلامة.