💻 computer science

Monitoring Data-aware Temporal Properties (Extended Version)

تقدم هذه الورقة إطار عمل جديداً، تم التحقق منه رسمياً، للمراقبة الاستباقية لخصائص الزمن الخطي المعززة بنظريات SMT (المعروفة بـ LTLfMT)، وذلك عبر الجمع بين الأساليب القائمة على الأوتوماتا والاستدلال الآلي، مما يحدد الأجزاء القابلة للتقرير ذات الصلولية للأنظمة المدركة للبيانات، ويبرهن على الجدوى من خلال تنفيذ نموذج أولي.

المؤلفون الأصليون: Alessandro Gianola, Marco Montali, Sarah Winkler

نُشر 2026-05-15

📖 5 دقيقة قراءة🧠 قراءة متعمّقة

CC BY 4.0

المؤلفون الأصليون: Alessandro Gianola, Marco Montali, Sarah Winkler

البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل

تخيل أنك تراقب آلة معقدة، "صندوق أسود" (مثل وكيل ذكاء اصطناعي متطور) وهو يؤدي مهمة ما. لا يمكنك رؤية ما بداخل الآلة للتحقق من مخططاتها أو شفرتها البرمجية، ولكن يمكنك مراقبة تدفق الإجراءات التي تتخذها. مهمتك هي العمل كـ "كلب حراسة" (Watchdog) لضمان التزام الآلة بالقواعد.

تقدم هذه الورقة البحثية نوعاً جديداً وذكياً للغاية من "كلاب الحراسة" لأنظمة الذكاء الاصطناعي التي تتعامل مع البيانات (مثل الأرقام، القوائم، أو سجلات قواعد البيانات) عبر الزمن.

إليك تفصيل عملهم باستخدام تشبيهات بسيية:

1. المشكلة: تحدي "البلورة السحرية"

معظم كلاب الحراسة التقليدية تشبه كاميرات المراقبة التي تنظر فقط إلى ما حدث بالفعل. إذا كسرت الآلة قاعدة ما، تكتشف الكاميرا ذلك وتطلق الإنذار.

ومع ذلك، يرى المؤلفون أنه في أنظمة الذكاء الاصطناعي المعقدة، أنت بحاجة إلى "بلورة سحرية". أنت لا تحتاج فقط لمعرفة ما إذا كانت الآلة قد كسرت قاعدة بالفعل، بل تريد معرفة ما إذا كانت محكوماً عليها بكسر القاعدة بغض النظر عما ستفعله لاحقاً.

التشبيه: تخيل متنزهاً يسير على حافة منحدر.
- كلب الحراسة القديم: "لم تسقط بعد، لذا أنت في أمان". (إنه ينظر فقط إلى الماضي).
- كلب الحراسة الجديد "الاستباقي": "على الرغم من أنك لم تسقط بعد، إلا أن المسار أمامك هو طريق مسدود. مهما كان الاتجاه الذي ستسلكه، سوف تسقط. أنا أعلن عن وقوعك في 'انتهاك دائم' الآن، قبل أن تخطو الخطوة الفعلية نحو الهاوية".

يُسمى هذا "المراقبة الاستباقية" (Anticipatory Monitoring). فهي تنظر إلى التاريخ وإلى جميع الاحتمالات المستقبلية لإعطاء حكم فوري.

2. التعقيد: البيانات + الزمن

الآلة لا تتحرك فحسب؛ بل تتخذ قرارات بناءً على البيانات.

المثال: فكر في "بوت" (برنامج آلي) لحجز تذاكر الحفلات الموسيقية. إنه يرى عرض تذاكر جديد كل ثانية. عليه أن يقرر: "هل أحتفظ بتذكرتي المحجوزة حالياً، أم أنتقل إلى هذه التذكرة الجديدة؟"
القاعدة: "اختر دائماً أرخص تذكرة للحفلة التي أريدها تحديداً".
التحدي: يجب على "البوت" مقارنة الأسعار (عمليات حسابية) والتحقق من أسماء الحفلات (بيانات) عند كل خطوة. إذا اختار البوت تذكرة بـ 100 دولار، بينما ظهرت لاحقاً تذكرة لنفس الحفلة بـ 50 دولاراً، فيجب على البوت أن ينتقل إليها. إذا لم يفعل، فهو يعتبر "مخالفاً".

لقد ابتكر المؤلفون لغة (مجموعة من القواعد) لوصف هذه القواعد المعقدة المعتمدة على البيانات. ويسمونها LTLMTf.

3. الحل: "الخريطة العكسية"

واجه المؤلفون مشكلة ضخمة: التنبؤ بالمستقبل لآلة ذات احتمالات لانهائية هو أمر مستحيل عادةً (رياضياً يُعرف بأنه "غير قابل للتقرير" أو Undecidable). الأمر يشبه محاولة التنبؤ بكل حركة ممكنة في لعبة شطرنج لا تنتهي أبداً.

لحل هذه المشكلة، بنوا "خريطة عكسية" (أداة تقنية تسمى مخطط إمكانية الوصول المشترك - Coreachability Graph).

التشبيه: بدلاً من محاولة تخمين كل مسار قد يسلكه المتنزه للأمام، تخيل أنك تبدأ من خط النهاية (الهدف) وتعمل طريقك للخلف.
1. تقوم بتحديد النقاط التي ينهي فيها المتنزه رحلته بنجاح.
2. تسأل: "ما هي الشروط التي يجب أن تتحقق الآن للوصول إلى تلك النقاط الجيدة؟"
3. تستمر في المشي للخلف، لتنشئ خريطة لـ "المناطق الآمنة" و"مناطق الخطر".

من خلال بناء هذه الخريطة بشكل عكسي، يمكنهم النظر إلى موقع المتنزه الحالي ومعرفة فوراً: "هل هناك أي مسار للأمام يؤدي إلى النجاح؟"

إذا كانت الإجابة نعم: النظام آمن حالياً، لكنه قد يفشل لاحقاً (الرضا الحالي - Current Satisfaction).
إذا كانت الإجابة لا: النظام آمن حالياً، لكنه سيفشل مهما حدث (الانتهاك الدائم - Permanent Violation - ملاحظة: وفقاً لمنطق الورقة، هذا يعني أنه سيقع في انتهاك لا مفر منه).

تصحيح بشأن الأحكام:
تحدد الورقة أربعة حالات لكلب الحراسة:

الرضا الحالي (CS): أنت جيد الآن، ولكن قد تخطئ لاحقاً.
الرضا الدائم (PS): أنت جيد الآن، ومضمون أن تظل جيداً بغض النظر عما يحدث لاحقاً.
الانتهاك الحالي (CV): لقد أخطأت، ولكن يمكنك إصلاح الأمر لاحقاً.
الانتهاك الدائم (PV): لقد أخطأت، ولا توجد طريقة لإصلاح ذلك. اللعبة انتهت.

الجزء "الاستباقي" هو القدرة على رصد حالة الانتهاك الدائم (PV) فوراً، بدلاً من الانتظار حتى ينهار النظام.

4. الخدعة السحرية: "إكمال النموذج" (Model Completion)

كيف جعلوا هذه الخريطة العكسية ممكنة دون الضياع في رياضيات لانهائية؟ استخدموا خدعة رياضية تسمى "إكمال النموذج" (Model Completion).

التشبيه: تخيل أنك تحاول حل متاهة، لكن المتاهة تستمر في بناء جدران جديدة.
- وجد المؤلفون طريقة لـ "تنعيم" المتاهة. لقد أثبتوا أنه بالنسبة لأنواع معينة من القواعد (تحديداً تلك التي تتعلق بـ قواعد البيانات والحساب مثل الجمع والطرح)، يمكنك التعامل مع المتاحة المتنامية كما لو كانت ثابتة وذات حجم يمكن التحكم فيه.
- حددوا "مناطق آمنة" من القواعد (مثل DB-LTLf-MC) حيث تكون الرياضيات فيها منطقية ومنتظمة. في هذه المناطق، تكون "الخريطة العكسية" مضمونة بأن تكون محدودة وقابلة للحل.

5. النتيجة: نموذج أولي يعمل

لم يكتفوا بكتابة النظرية فقط؛ بل بنوا أداة نموذجية تسمى MONTHE.

اختبروا الأداة على مثال تذاكر الحفلات الموسيقية.
نجحت الأداة في مراقبة "بوت التذاكر" واستطاعت أن تقول فوراً: "مهلاً، لقد اختار البوت تذكرة بـ 100 دولار، لكن سعر الحفلة هو 50 دولاراً. إنه في حالة انتهاك دائم الآن لأنه لن يجد تذكرة الـ 50 دولاراً إذا استمر في تجاهل البيانات".

ملخص

هذه الورقة البحثية تتعلق ببناء حارس أمن شديد اليقظة لأنظمة الذكاء الاصطناعي.

الحارس القديم: "لم تكسر القواعد بعد".
الحارس الجديد: "أنا أرى المستقبل. أنت تكسر القواعد الآن، ولا توجد طريقة لإصلاح ذلك. أنا أصنفك كـ 'منتهك بشكل دائم' فوراً".

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

ملخص تقني: مراقبة الخصائص الزمنية المدركة للبيانات

تعريف المشكلة

يتناول البحث تحدي التحقق من التشغيل الاستباقي (anticipatory runtime verification) للأنظمة الذكية المعقدة والديناميكية التي تكون فيها المواصفات الداخلية غير قابلة للوصول (الأنظمة الصندوقية السوداء). وتكون طرق التحقق التقليدية في وقت التصميم، مثل فحص النماذج (model checking)، غير قابلة للتطبيق غالباً في هذه السيناريوهات. وبينما يوفر التحقق من التشغيل (Runtime Verification - RV) حلاً عبر مراقبة آثار التنفيذ، إلا أن النهج الحالية تواجه عقبتين رئيسيتين:

الطبيعة الاقتراضية (Propositional Nature): لا يمكن لمنطق الزمن الخطي فوق المسارات المحدودة ( $L_f L T$ ) القياسي التعبير عن الخصائص التي تتضمن بيانات مهيكلة (مثل الحساب، المجموعات، أو الدوال غير المفسرة)، وهي أمور منتشرة في وكلاء الذكاء الاصطنيعي الحديثة والعمليات التجارية.
نقص الاستباق (Lack of Anticipation): معظم المراقبين يقيمون فقط بادئة الأثر (trace prefix) المرئية حتى الآن. إنهم يفشلون في اكتشاف الانتهاكات التي أصبحت حتمية بغض النظر عن كيفية استمرار الأثر (على سبيل المثال، إذا كان النظام قد التزم بالفعل بحالة تجعل هدفاً مستقبلياً مستحيلاً).

يركز المؤلفون على $LTLMT_f$ (منطق الزمن الخطي فوق المسارات المحدودة المدمج مع النظريات)، والذي يثري $LTL_f$ بنظريات SMT التعسفية. المشكلة المحددة هي المراقبة الاستباقية: تحديد حالة المراقبة لخاصية $\psi$ بعد أثر $\tau$ من خلال النظر في $\tau$ وجميع امتداداتها المحدودة الممكنة. تُعرف حالات المراقبة كالتالي:

الرضا الحالي (Current Satisfaction - CS): الأثر $\tau$ يحقق $\psi$ ، ولكن من الممكن حدوث انتهاك في بعض الامتدادات.
الرضا الدائم (Permanent Satisfaction - PS): الأثر $\tau$ يحقق $\psi$ ، ولا يمكن لأي امتداد أن ينتهكه.
الانتهاك الحالي (Current Violation - CV): الأثر $\tau$ ينتهك $\psi$ ، ولكن من الممكن تحقيق الرضا في بعض الامتدادات.
الانتهاك الدائم (Permanent Violation - PV): الأثر $\tau$ ينتهك $\psi$ ، ولا يمكن لأي امتداد أن يحقق الرضا.

مشكلة المراقبة العامة لـ $LTLMT_f$ غير قابلة للتقرير (undecidable)، خاصة عند التعامل مع الحساب الخطي على الأعداد الحقيقية. يهدف البحث إلى تحديد أجزاء (fragments) قابلة للتقرير وذات صلة عملية من هذا المنطق.

المنهجية

يجمع الإطار المقترح بين الأساليب القائمة على الأوتوماتا (automata-theoretic methods) للاستدلال الزمني وتقنيات الاستدلال الآلي (SMT) لجانب البيانات.

1. المنطق والدلالات

يعرف المؤلفون $LTLMT_f$ فوق توقيع متعدد الفئات $\Sigma$ يحتوي على متغيرات البيانات، الدوال، والمحمولات (predicates). هناك خيار دلالي رئيسي في التعامل مع النموذج الأساسي $M$ :

الامتداد المحافظ (Conservative Extension): النموذج الذي يقوم عليه الأثر ليس ثابتاً؛ بل إن استمرار الأثر يوفر امتداداً للنموذج (عبر التضمين/embeddings). الحقائق حول العناصر التي تمت رؤيتها سابقاً تظل ثابتة، ولكن يمكن إدخال عناصر وحقائق جديدة. وهذا يتوافق مع سيناريوهات مثل أنظمة التذاكر حيث تكون الأسعار الماضية ثابتة، ولكن تظهر تذاكر جديدة.
عامل النظر للخلف (Lookback Operator): يستخدم المنطق عامل "النظر للخلف" ( $\triangleleft$ ) للإشارة إلى القيمة السابقة للمتغير، بدلاً من عامل "النظر للأمام".

2. بناء الأوتوماتا

لأي خاصية $LTLMT_f$ خالية من المكممات (quantifier-free) (يُشار إليها بـ dataLTLf)، يقوم المؤلفون ببناء أوتوماتا محدودة غير حتمية (NFA)، $N_\psi$ .

تتكون الأبجدية $\Theta$ من مجموعات من صيغ المنطق من الدرجة الأولى (FO) (ونفيها) الموجودة في الخاصية.
تتبع الـ NFA التطور الزمني للخاصية، وتقبل الكلمات التي تتوافق مع الآثار التي تحقق الخاصية.
يتم فرض قيد "النظر للخلف الآمن" (safe lookback) لضمان أن متغيرات النظر للخلف لا تقيد الحالة الابتدائية للأثر.

3. رسوم الوصول الأساسية (Coreachability Graphs) والارتداد (Regression)

للتعامل مع جانب البيانات وتحديد الحالات الاستباقية، يقدم المؤلفون رسم الوصول الأساسي ( $CG^+$ ) ورسم عدم الوصول الأساسي المزدوج ( $CG^-$ ).

الارتداد (Regression): الآلية الأساسية هي عملية regress التي تنشر التزامات التحقق للخلف عبر انتقالات الـ NFA. بالنظر إلى صيغة الحالة $\phi$ وقيد الانتقال $C$ ، تقوم regress( $\phi$ , $C$ ) بحساب الشرط المطلوب على الحالة السابقة لتحقيق $\phi$ بعد تطبيق $C$ .
إكمال النموذج (Model Completion): لضمان أن ينتج الارتداد صيغاً خالية من المكممات (وهو أمر ضروري للتقريرية)، يعتمد الإطار على كون النظرية $T$ تمتلك إكمال نموذج $T^*$ . يسمح هذا بحذف المكممات الوجودية (existential quantifiers) التي تظهر أثناء الارتداد، وتحويلها إلى صيغ مكافئة خالية من المكممات في $T^*$ .
بناء الرسم البياني: العقد في الرسم البياني هي أزواج $(q, \phi)$ ، حيث $q$ هي حالة NFA و $\phi$ هي صيغة خالية من المكممات تمثل الشرط المطلوب للوصول إلى حالة نهائية (أو غير نهائية) من $q$ .

4. خوارزمية المراقبة

تعمل إجراءات MONITOR كما يلي:

حساب الـ NFA $N_\psi$ ورسوم الوصول الأساسية $CG^+$ و $CG^-$ .
محاكاة الأثر $\tau$ على $N_\psi$ لتحديد الحالة الحالية $q$ .
تقييم التعيين الأخير $\alpha_n$ $α_{n}$ مقابل الصيغ المرتبطة بالحالة $q$ $q$ :
- إذا كانت $q$ حالة قبول: تحقق مما إذا كان $EXTVIOL(q)$ (شرط حدوث انتهاك مستقبلي) متحققاً. إذا نعم $\leftarrow$ CS؛ إذا لا $\leftarrow$ PS.
- إذا كانت $q$ حالة عدم قبول: تحقق مما إذا كان $EXTSAT(q)$ (شرط حدوث رضا مستقبلي) متحققاً. إذا نعم $\leftarrow$ CV؛ إذا لا $\leftarrow$ PV.

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

صياغة المراقبة الاستباقية لـ $LTLMT_f$ : هذا هو العمل الأول الذي يعرف ويعالج مشكلة المراقبة الاستباقية للخصائص الزمنية المدركة للبيانات فوق المسارات المحدودة المعززة بنظريات SMT.
إطار عمل مبتكر: يقدم المؤلفون إطاراً تأسيسياً يجمع بين الاستدلال الزمني القائم على NFA والاستدلال القائم على SMT للبيانات. الابتكار التقني الرئيسي هو استخدام إكمال النموذج للتعامل مع حذف المكممات أثناء الارتداد الخلفي لالتزامات التحقق، مما يسمح ببناء رسوم وصول أساسية منتهية.
تحديد الأجزاء القابلة للتقرير: يحدد البحث أجزاءً محددة وذات صلة عملية من $LTLMT_f$ $L T L M T_{f}$ حيث تكون مشكلة المراقبة قابلة للحل (مضمونة الإنهاء):
- DB-LTLf: الخصائص التي تجمع بين مراجع قواعد البيانات (الممثلة عبر المساواة والدوال غير المفسرة - EUF) مع الحساب، تحت قيود هيكلية معينة.
- التواقيع اللا-دورية (Acyclic Signatures): تضمن عدداً محدوداً من الحدود (terms).
- قيود الرتابة (Monotonicity Constraints - MCs): تقيد الحساب في عمليات مقارنة بسيطة ( $=, \neq, \leq, <$ ) بين الحدود، وهو أمر شائع في مراقبة العمليات التجارية.
- الإنهاء المحلي (Local Finiteness): شرط أوسع يضمن عدداً محدوداً من الصيغ غير المتكافئة.
- النظر للخلف المحدود (Bounded Lookback): قيد نحوي على تفاعل القيود في الخاصية، مما يعمم مفهوم "حرية التغذية الراجعة" (feedback freedom).
نموذج أولي للتنفيذ: يتم إثبات جدوى النهج من خلال MONTHE، وهو أداة نموذجية مبنية بلغة Python تستخدم محلل SMT المسمى CVC5 للتعامل مع البيانات وحذف المكممات.

النتائج والتقييم

النتائج النظرية: يقدم البحث براهين رسمية لصحة خوارزمية المراقبة (المبرهنة 18) ويثبت قابلية التقرير للأجزاء المحددة (المبرهنات 19–24).
التطبيق العملي: يُظهر الإطار قدرته على تغطية العمليات التجارية المدركة للبيانات والأنظمة الديناميكية التي تعمل فوق قواعد بيانات للقراءة فقط (مثل مثال التذاكر حيث يختار الوكيل أرخص تذكرة).
التقييم الأولي: يذكر المؤلفون تجارب أولية باستخدام أداة MONTHE. نجحت الأداة في معالجة الخصائص والآثار، مع إخراج حالة المراقبة الصحيحة. ويوصف التقييم بأنه أولي، مع ترك التقييم التجريبي المكثف للعمل المستقبلي.

الأهمية والادعاءات

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

يؤكد المؤلفون أنه بينما تعتبر المراقبة الاستباقية العامة غير قابلة للتقرير، فإن تحديدهم لـ DB-LTLf (الذي يجمع بين الحساب مع مراجع قواعد البيانات) يوفر "نقطة مثالية" (sweet spot) من حيث القدرة التعبيرية والتقريرية. وهذا مهم بشكل خاص لـ:

العمليات التجارية المدركة للبيانات: حيث تعتمد الانتقالات على قيم قواعد البيانات وقيود حسابية.
الأنظمة الديناميكية: حيث يتفاعل الوكلاء مع قواعد بيانات للقراءة فقط (مثل أسواق التذاكر، أنظمة المخزون).

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