Quantitative Monitoring of Signal First-Order Logic

إليك ملخص تقني مفصل لورقة البحث بعنوان "المراقبة الكمية للمنطق من الدرجة الأولى للإشارات" (Quantitative Monitoring of Signal First-Order Logic).

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

تتضمن التحقق في وقت التشغيل (Runtime verification) فحص تنفيذات النظام مقابل مواصفات صورية. وبينما يُستخدم المنطق الزمني للإشارة (STL) على نطاق واسع للإشارات المستمرة، فإنه يفتقر إلى القدرة التعبيرية لنمذجة سلوكيات الأنظمة الهجينة المعقدة، مثل خصائص الاستقرار المحدود (على سبيل المثال، "بعد حدوث اضطراب، يجب أن تعود الإشارة إلى قيمة محددة خلال نافذة زمنية"). تم تقديم المنطق من الدرجة الأولى للإشارة (SFO) لمعالجة ذلك عبر الجمع بين المنطق من الدرجة الأولى والحساب الخطي ورموز الدوال غير المفسرة، مما يسمح بالكمّ (quantification) فوق كل من متغيرات الزمن والقيمة.

ومع ذلك، كانت هناك فجوتان حرجتان في SFO:

1. الافتقار إلى الدلالات الكمية: كانت تعريفات SFO الحالية بولية بحتة (مُحققة/منتهكة). وفي الأنظمة المستمرة، غالبًا ما تكون النتائج الثنائية غير كافية؛ إذ يحتاج المهندسون إلى معرفة مدى جودة تحقيق المواصفات (المتانة/robustness) لاتخاذ قرارات تحكم أفضل.
2. الافتقار إلى أدوات المراقبة عبر الإنترنت (Online Monitoring): غالبًا ما تعتمد صيغ SFO الكاملة على سلوك مستقبلي غير محدود، مما يجعلها غير مناسبة للمراقبة عبر الإنترنت (في الوقت الفعلي). علاوة على ذلك، لم تكن هناك أداة موجودة للقيام بالمراقبة عبر الإنترنت لـ SFO، ناهيك عن المراقبة الكمية.

2. المنهجية

يقترح المؤلفون إطار عمل لـ المراقبة الكمية عبر الإنترنت لـ SFO. يتكون نهجهم من أربعة ركائز تقنية رئيسية:

أ. الدلالات الكمية القائمة على المتانة (Robustness-Based Quantitative Semantics)

يحدد البحث دلالات جديدة لـ SFO تمنح قيمة متانة $\mu(w, \nu, \phi) \in \mathbb{R} \cup \{-\infty, +\infty\}$ لأثر الإشارة $w$ والتقييم $\nu$.

• التفسير: تشير القيمة الموجبة إلى التحقق (المقدار = درجة التحقق)، بينما تشير القيمة السالبة إلى الانتهاك (المقدار = درجة الانتهاك).
• التعريف العودي (Recursive Definition):
  • المحمولات الذرية ($\theta_1 < \theta_2$): المتانة هي الفرق $\llbracket \theta_2 \rrbracket - \llbracket \theta_1 \rrbracket$.
  • النفي ($\neg \phi$): المتانة هي $-\mu(\phi)$.
  • الفصل ($\phi_1 \lor \phi_2$): المتانة هي $\max(\mu(\phi_1), \mu(\phi_2))$.
  • التكميم الوجودي ($\exists x \in I. \phi$): المتانة هي الحد الأعلى (supremum) لـ $\mu(\phi)$ عبر الفترة $I$.
• السلامة (Soundness): تم إثبات سلامة الدلالات بالنسبة للدلالات البولية: $\mu > 0 \implies$ مُحققة؛ $\mu < 0 \implies$ منتهكة.

ب. جزء الزمن الماضي وعملية "التحويل للماضي" (Past-Time Fragment and Pastification)

لتمكين المراقبة عبر الإنترنت، حدد المؤلفون جزءًا من المنطق يسمى المنطق من الدرجة الأولى للإشارة للزمن الماضي (pSFO). تكون الصيغة ضمن pSFO إذا كانت جميع عمليات الوصول إلى الإشارة عند الزمن $t$ تشير فقط إلى أزمنة $\le t$.

• صيغ الاستجابة المحدودة: ركز المؤلفون على الصيغ حيث تكون مكممات الزمن محدودة (مثل $\exists s \in [0, 10]$).
• إجراء التحويل للماضي (Pastification Procedure): قدموا خوارزمية لتحويل صيغة SFO ذات الاستجابة المحدودة إلى صيغة pSFO متكافئة في التحقق. يتضمن ذلك حساب أفق أمامي ($H^+$)، وهو أقصى إزاحة مستقبلية مطلوبة من قبل الصيغة. من خلال إزاحة الزمن المرجعي إلى الوراء بمقدار $H^+$، يتم تحويل عمليات الوصول المستقبلية للإشارة إلى عمليات وصول ماضية، مما يسمح للمراقب بالعمل دون الحاجة للنظر إلى المستقبل.

ج. خوارما المراقبة عبر الإنترنت متعدد الأوجه (Polyhedral Online Monitoring Algorithm)

تحسب الخوارزمية الأساسية قيم المتانة رمزياً باستخدام متعدد الأوجه المحدب (Convex Polyhedra).

• التمثيل: يتم تمثيل الإشارات والصيغ كقوائم من متعددات الأوجه المحدبة المعرفة بقيود خطية على متغيرات الزمن والقيمة.
• العمليات الرمزية:
  • الحساب: يُترجم إلى تقاطعات وإسقاطات لمتعددات الأوجه.
  • الروابط البولية: يتم التعامل معها عبر تقسيم الحالات (مثلاً $v_1 \ge v_2$ مقابل $v_1 < v_2$) لحساب أقصى متانة.
  • المكممات: يتم التعامل معها عبر التعظيم البارامتري (Parametric Maximization). لحساب $\sup_{x \in I} \mu(\phi)$، تقوم الخوارزمية بإلغاء المتغير المكمّم عبر إيجاد الحد الأقصى لدالة خطية (affine) فوق مجال متعدد الأوجه. يتم تحقيق ذلك باستخدام إجراء متخصص (PlpMaximize) يحلل ميل الدالة الهدف بالنسبة لحدود متعدد الأوجه.
• إدارة الذاكرة: يحافظ المراقب على نافذة منزلقة من تاريخ الإشارة تتوافق مع الأفق الخلفي ($H^-$) للصيغة، مع التخلص من البيانات القديمة لضمان استخدام محدود للذاكرة.

د. التنفيذ

قام المؤلفون بتنفيذ أداة نموذجية بلغة بايثون باستخدام SymPy للحساب الرمزي و Parma Polyhedra Library (PPL) لعمليات متعدد الأوجه. تدعم الأداة تحليل صيغ SFO، وتنفيذ عملية التحويل للماضي، وتشغيل خوارزمية المراقبة عبر الإنترنت على الإشارات ذات الخطوط المتعددة (piecewise-linear).

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

1. أول دلالات كمية كاملة لـ SFO: تعميم SFO البولي إلى إطار عمل قائم على المتانة، مما يسمح بتقييم دقيق للإشارات ذات القيم الحقيقية.
2. إجراء التحويل للماضي (Pastification): طريقة مبتكرة لتحويل صيغ SFO ذات الاستجابة المحدودة إلى أجزاء زمنية ماضية، مما يسد الفجوة بين التعبير المنطقي والقدرة على المراقبة عبر الإنترنت.
3. خوارزمية مراقبة فعالة عبر الإنترنت: خوارزمية مراقبة رمزية تحسب قيم المتانة لصيغ pSFO عبر تمثيلات متعددة الأوجه للإشارات ذات الخطوط المتعددة.
4. النموذج الأولي والاختبارات المرجعية: أول نموذج أولي متاح علناً للمراقبة الكمية لـ SFO عبر الإنترنت، والذي تم التحقق من صحته مقابل معايير الأنظمة السيبرانية الفيزيائية الواقعية.

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

قيم المؤلفون أداتهم باستخدام معيارين:

• تجنب العوائق الديناميكية: طائرة بدون طيار (درون) تتنقل في بيئة حضرية مع وجود عوائق.
  • الخصائص: سرعة آمنة، سلاسة الحركة (قيود المشتقات)، والتباعد عن العوائق.
  • الأداء: حسبت المراقبة قيم المتانة في زمن يتراوح بين 0.002 ثانية و 0.021 ثانية لكل جزء (فترة أخذ العينات 0.1 ثانية). هذا أسرع بكثير من حلقة التحكم، مما يثبت الجدوى لاتخاذ قرارات التحكم في الوقت الفعلي.
• التحكم في الارتفاع: نموذج مبسط لطائرة مقاتلة من طراز F-16.
  • الخصائص: ارتفاع آمن، سرعة جوية آمنة، واستعادة الارتفاع (خاصية استقرار محدودة معقدة ذات مكممات متداخلة).
  • الأداء: بالنسبة لخاصية الاستعادة المعقدة (التي تتطلب أفقاً زمنياً قدره 20 ثانية)، استغرقت المراقبة ~0.21 ثانية لكل جزء (فترة أخذ العينات 0.033 ثانية). ورغم أنها أبطأ قليلاً من حلقة التحكم، إلا أنها سريعة بما يكفي لتقديم تحذيرات وقت التشغيل والإشراف.
• القابلية للتوسع: تُظهر النتائج أن النهج يتوسع جيداً مع تعقيد المواصفات، بما في ذلك المكممات المتداخلة والروابط البولية، رغم أن وقت التشغيل يزدزد مع حجم الأفق الخلفي.

5. الأهمية

تمثل هذه الورقة تقدماً كبيراً في مجال التحقق في وقت التشغيل للأنظمة الهجينة:

• القدرة التعبيرية: تتيح مراقبة الخصائص المعقدة (مثل الاستقرار المحدود وقيود التوقيت النسبية) التي يستحيل التعبير عنها في STL أو المنطق الخالي من المكممات.
• العملية: من خلال توفير أول مراقب كمي عبر الإنترنت لـ SFO، فإنها تنقل المنطق من التعبير النظري إلى التطبيق العملي في الأنظمة السيبرانية الفيزيائية (CPS).
• التغذية الراجعة للتحكم: توفر المخرجات الكمية (قيم المتانة) تغذية راجعة قابلة للتنفيذ يمكن استخدامها في تخليق المتحكمات (controller synthesis)، أو مكافآات التعلم المعزز، أو فرض القواعد في وقت التشغيل (الدرع/shielding)، متجاوزة مجرد التحقق من النجاح أو الفشل.
• تأسيس للعمل المستقبلي: تضع الورقة أساساً دلالياً وخوارزمياً لدمج SFO في أطر عمل أوسع مثل فرض القواعد في وقت التشغيل والمراقبة اللامركزية.