Ternary Logic Encodings of Temporal Behavior Trees with Application to Control Synthesis

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

1. بيان المشكلة

تتطلب الأنظمة ذاتية القيادة طرقًا قوية لنمذجة المهام وتخليق التحكم. وبينما توفر المنطق الزمني الإشاري (STL) تعبيرًا غنيًا لتحديد السلوكات المكانية والزمانية، إلا أنها تواجه صعوبة في التخطيط طويل الأمد وآليات التراجع المعقدة (مثل: "إذا فشلت المهمة أ، جرب ب"). توفر أشجار السلوك (BTs) واجهة رسومية حدسية ونمطية لمثل هذه الاستراتيجيات الهرمية، لكنها تفتقر إلى نماذج رسمية صارمة لـ تخليق التحكم الصحيح بالبناء (correct-by-construction control synthesis).

تعتمد النهج الحالية لترسيم أشجار السلوك (أو ما يعرف بـ Temporal Behavior Trees أو TBTs) على التحليل اللاحق (post-hoc) أو إصلاح المسارات باستخدام المنطق البولياني (Boolean logic). تفشل هذه الطرق في التقاط الطبيعة الديناميكية لتنفيذ أشجار السلوك، وتحديدًا حالة "الجريان" (Running)، حيث لا تكون المهمة مستوفاة تمامًا ولا فاشلة تمامًا. علاوة على ذلك، فإن تشفيرات STL القياسية لتخليق التحكم غالبًا ما تفترض مسارات لانهائية أو تتطلب معرفة الأفق الزمني بأكمله، مما يجعلها غير مناسبة لتحليل المسارات الجزئية أو الأنظمة التي تعاني من عدم اليقين.

التحدي الجوهري: كيف يمكن ترميز أشجار السلوك ومعاملاتها الزمنية رسميًا في إطار رياضي مناسب لـ التحسين ذي الأعداد الصحيحة المختلطة (mixed-integer optimization) الذي يأخذ في الاعتبار:

1. منطق الحالات الثلاث لأشجار السلوك (نجاح، فشل، جريان).
2. المسارات الجزئية حيث يكون المستقبل غير معروف.
3. عدم يقين النظام (القياسات التي ليست صادقة ولا كاذبة بشكل واضح).

2. المنهجية

يقترح المؤلفون إطار عمل يعيد صياغة TBTs باستخدام منطق كليين القوي ($K_3$)، وهو نظام منطق ثلاثي، ويقوم بتشفير هذه الدلالات في قيود البرمجة الخطية ذات الأعداد الصحيحة المختلطة (MILP).

أ. أساس المنطق الثلاثي ($K_3$)

بدلاً من المنطق البولياني القياسي (صواب/خطأ)، قدم المؤلفون قيمة ثالثة، وهي "غير معروف" ($U$)، لتمثيل حالة "الجريان" لعقدة شجرة السلوك أو قياسات النظام غير المحددة.

• قيم الحقيقة: $\{F, U, T\}$ تقابل $\{-1, 0, +1\}$.
• العمليات المنطقية: محددة عبر جداول جبر كليين (على سبيل المثال، $T \land U = U$، و $F \lor U = U$).
• الأهمية: يسمح هذا للنظام بالتعامل مع الحالات التي لم يستوفِ فيها المسار المواصفات بعد أو لم ينتهكها بعد، مما يتيح التفكير في المسارات الجزئية.

ب. المنطق الزمني الإشاري الثلاثي (Ternary STL)

قام المؤلفون بتوسيع دلالات STL لتعمل على $K_3$ والمسارات الجزئية (آفاق زمنية نهائية $t_2$).

• المحمولات الإشارية (Signal Predicates): محددة بعتبة عدم يقين $\delta$. إذا كان $f(x_t) \ge \delta$، فالقيمة هي $T$؛ وإذا كان $f(x_t) \le -\delta$، فالقيمة هي $F$؛ وإذا كان $-\delta < f(x_t) < \delta$، فالقيمة هي $U$.
• المعاملات الزمنية: تمت إعادة تعريف معاملي "دائمًا" ($\square$) و"في وقت ما" ($\diamond$) للتعامل مع العلاقة بين نافذة البحث (الفاصل الزمني المطلوب من المعامل) والأفق الجزئي (طول المسار المعروف حاليًا).
  • إذا كانت نافذة البحث تقع بالكامل داخل الأفق، تُطبق المنطق القياسي.
  • إذا تجاوزت النافذة الأفق، تكون النتيجة $U$ (غير معروف)، ما لم يحدث "اختصار" (على سبيل المثال، إذا واجه الاقتران $F$ مباشرة، مما يجعل التعبير بأكمله $F$ بغض النظر عن المستقبل المجهول).

ج. التشفيرات ذات الأعداد الصحيحة المختلطة

طور البحث تشفيرات محددة لترجمة قواعد المنطق الثلاثي هذه إلى قيود لبرنامج التربيع الخطي ذي الأعداد الصحيحة المختلطة (MIQP).

• متغيرات القرار: أعداد صحيحة ثلاثية $z \in \{-1, 0, +1\}$ تمثل استيفاء صيغة معينة عند خطوة زمنية محددة.
• استراتيجية التشفير:
  • المحمولات (Predicates): مشفرة باستخدام متغيرات ثنائية لفرض القيود الخطية على الحالة $x_t$ بالنسبة لـ $\delta$.
  • الروابط المنطقية: تُستخدم عمليات الحد الأدنى (Min) والحد الأقصى (Max) لتشفير $\land$ (التقاطع/الحد الأدنى) و $\lor$ (الاتحاد/الحد الأقصى) فوق المجموعة الثلاثية.
  • معاملات TBT (التتابع/الاختيار):
    • التتابع ($\rightarrow$): يتطلب استيفاء الصيغ الفرعية بالتتابع. يبحث التشفير عن نقطة انقسام $\tau$ حيث يحقق الجزء الأول $\phi_1$ والجزء المتبقي يحقق $\phi_2$.
    • الاختيار ($?$): يتطلب استيفاء صيغة فرعية واحدة على الأقل. يبحث التشفير عن نقطة انقسام حيث يحقق الجزء الأول $\phi_1$ أو يحقق الجزء المتبقي $\phi_2$.
• التعقيد: يشير المؤلفون إلى أنه بينما تكون تشفيرات STL القياسية خطية في التعقيد الزمني $O(T)$، فإن تشفيرات TBT التي تتضمن $k$ من الصيغ الفرعية تتوسع كـ $O(T^{k+1})$ بسبب البحث المتداخل عبر انقسامات الوقت.

د. مشكلة تخليق التحكم

يصيغ إطار العمل مشكلة تحكم أمثل للأنظمة الخطية ذات الزمن المنفصل:
$$\min \sum u_t^T R u_t$$
بشرط:

• ديناميكيات النظام ($x_{t+1} = Ax_t + Bu_t$).
• قيود المدخلات.
• قيد استيفاء TBT: يجب أن يستوفي المسار المُخلق صيغة TBT $\phi$ بدءًا من $t^*$.

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

1. ترسيم أشجار السلوك في $K_3$: قامت الورقة بتجسيد الترسيم الرسمي لأشجار السلوك باستخدام المنطق الثلاثي، مع ربط حالة "الجريان" صراحةً بقيمة الحقيقة "غير معروف".
2. دلالات STL الثلاثية: حددت الدلالات النوعية لـ STL عبر المسارات الجزئية باستخدام $K_3$، مما يسمح بتقييم الصيغ حتى عندما لا يكون الأفق الكامل معروفًا أو عندما تكون القياسات غير مؤكدة.
3. تشفيرات الأعداد الصحيحة المختلطة: قدم المؤلفون أول تشفيرات خطية للأعداد الصحيحة المختلطة لمعاملات TBT (التتابع والاختيار) عبر المنطق الثلاثي، مما يتيح تخليق التحكم الصحيح بالبناء.
4. إثبات الفائدة: تم التحقق من إطار العمل من خلال دراستي حالة لحل مسائل التحكم الأمثل للأنظمة الديناميكية الخطية، مما يثبت أن TBTs يمكن أن تولد مسارات قابلة للتنفيذ ومثالية تتعامل مع منطق التراجع المعقد.

4. النتائج ودراسات الحالة

تحقق المؤلفون من إطار العمل باستخدام حلل Gurobi في سيناريوهين:

• دراسة الحالة 1: المكامل المزدوج ذو الزمن المنفصل (روبوت متنقل)

  • المهمة: التنقل إلى الهدف (أ)، ثم فحص البطارية. إذا كانت $\ge 80\%$، اذهب إلى الهدف (ب)؛ وإلا، اذهب إلى الهدف (ج) (الشاحن) ثم الهدف (ب).
  • النتيجة: نجح الحل في تخليق مسارات لحالتين مختلفتين من حالة البطارية الأولية.
    • بطارية عالية: توجه الروبوت من (أ) $\to$ (ب).
    • بطارية منخفضة: توجه الروبوت من (أ) $\to$ (ج) $\to$ (ب).
  • الأداء: تم الحل للوصول إلى الأمثلية العالمية في حوالي 97 ثانية لأفق مكون من 25 خطوة.

• دراسة الحالة 2: التخطيط متعدد الوكلاء

  • المهمة: يجب على ثلاثة وكلاء الوصول بالتتابع إلى أهداف محددة مع تجنب العوائق والحفاظ على مسافة فصل دنيا.
  • النتيجة: قام النظام بتخليق مسارات حيث قام الوكلاء بـ الانتظار في طابور (queuing) بشكل طبيعي للمرور عبر ممرات ضيقة لتلبية قيود السلامة.
  • الأداء: تم الحل لـ 3 وكلاء عبر أفق مكون من 20 خطوة في حوالي 307 ثوانٍ.

5. الأهمية والتأثير

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

باختصار، تقدم الورقة طريقة رياضية صارمة لترجمة مواصفات أشجار السلوك عالية المستوى والنمطية إلى مسائل تحسين، مما يمكّن الأنظمة ذاتية القيادة من توليد استراتيجيات تحكم مثالية وآمنة وقوية تتكيف مع الإخفاقات وعدم اليقين.