التحقق الرسمي من شهادة عدم قابلية حل مسائل التخطيط الزمني

المعلومات الأساسية

• معرّف الورقة: 2510.10189
• العنوان: التحقق الرسمي من شهادة عدم قابلية حل مسائل التخطيط الزمني
• المؤلفون: ديفيد وانج، محمد عبد العزيز (كلية الملك بلندن، المملكة المتحدة)
• التصنيف: cs.LO (المنطق في علوم الحاسوب)، cs.AI (الذكاء الاصطناعي)
• تاريخ النشر: 11 أكتوبر 2025 (نسخة أولية على arXiv)
• رابط الورقة: https://arxiv.org/abs/2510.10189

الملخص

تقترح هذه الورقة منهجية لشهادة عدم قابلية حل مسائل التخطيط الزمني. تعتمد المنهجية على ترميز مسائل التخطيط كشبكات آلات زمنية، ثم استخدام فاحص نماذج فعّال على الشبكة، متبوعاً باستخدام فاحص الشهادات للتحقق من مخرجات فاحص النماذج. تعطي المنهجية الأولوية للموثوقية المعتمدة: يتم استخدام مثبت النظريات Isabelle/HOL للتحقق الرسمي من تنفيذ ترميز الآلات الزمنية، واستخدام فاحص شهادات موجود (يتم التحقق منه رسمياً أيضاً في Isabelle/HOL) للتحقق من نتائج فحص النماذج.

الخلفية البحثية والدافع

المشكلة الأساسية

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

أهمية المشكلة

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

قيود الطرق الموجودة

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

الدافع البحثي

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

المساهمات الأساسية

1. طريقة ترميز مُحققة رسمياً: أول تحقق رسمي لترميز Heinz وآخرين للتخطيط الزمني إلى آلات زمنية
2. التنفيذ الهندسي: تكييف الترميز لإنتاج صيغة آلات زمنية متوافقة مع نظام Wimmer و von Mutius
3. تصميم دلالات مبسطة: تصميم دلالات تخطيط زمني أبسط من الأعمال الموجودة، مما يسهل الاستدلال الرياضي، وإثبات التكافؤ مع الدلالات الموجودة
4. إطار عمل شهادة كامل: بناء سلسلة شهادة موثوقة كاملة من مسائل التخطيط الزمني إلى فحص نماذج الآلات الزمنية
5. ضمانات الصحة النظرية: إثبات صحة الترميز في Isabelle/HOL، مما يوفر ضمانات نظرية قوية

شرح الطريقة

تعريف المهمة

الإدخال: مسألة تخطيط زمني P = ⟨P, A, I, G⟩

• P: مجموعة القضايا
• A: مجموعة الإجراءات ذات المدة
• I: الحالة الأولية
• G: شروط الهدف

الإخراج: شهادة رسمية لعدم القابلية للحل (إذا كانت المسألة فعلاً غير قابلة للحل)

شروط القيد:

• الإجراءات لها إجراءات لقطة البداية والنهاية
• دعم شروط عدم التغيير وقيود الجدولة
• الامتثال لقيود الاستبعاد المتبادل وحدود المدة

معمارية النموذج

1. إضفاء الطابع الرسمي على التخطيط الزمني

تحدد الورقة أولاً دلالات التخطيط الزمني الرسمية:

إجراءات اللقطة (التعريف 1):

h ≡ ⟨pre(h), adds(h), dels(h)⟩

الإجراءات ذات المدة (التعريف 2):

a ≡ ⟨a⊢, a⊣, over_all(a), L(a), U(a)⟩

حيث a⊢ و a⊣ هما إجراءات لقطة البداية والنهاية على التوالي.

2. ترميز الآلات الزمنية

تصميم المتغيرات (التعريف 24):

• لكل قضية p: متغير ثنائي vp (ترميز القيمة الحقيقية) وعداد القفل lp (تسجيل عدد الإجراءات النشطة التي تتطلب p أن تكون صحيحة)
• aa: تسجيل إجمالي الإجراءات النشطة
• ps: حالة التخطيط (0=لم تبدأ، 1=قيد التخطيط، 2=مكتملة)

تصميم الساعات (التعريف 25):

• لكل إجراء a يتم تخصيص ساعتين: ca⊢ (تسجيل الوقت بعد البداية) و ca⊣ (تسجيل الوقت بعد النهاية)

الآلة الرئيسية (التعريف 26): التحكم في تحولات الحالة لعملية التخطيط بأكملها، بما في ذلك التهيئة والتحقق من الهدف.

آلات الإجراءات (التعريف 27): كل إجراء يقابل آلة، تحتوي على التحولات الرئيسية التالية:

• sea: تطبيق تأثيرات بدء الإجراء
• se'a: قفل شروط عدم التغيير
• eea: التحضير قبل النهاية
• ee'a: تطبيق تأثيرات نهاية الإجراء
• iea: معالجة الإجراءات الفورية

3. بناء الشبكة

دمج الآلة الرئيسية وجميع آلات الإجراءات في شبكة آلات زمنية (التعريف 28)، مع تعيين التكوين الأولي لجميع الآلات في حالة غير نشطة.

نقاط الابتكار التقني

1. دعم التنفيذ المتزامن: بخلاف Heinz وآخرين الذين استخدموا أقفالاً عامة، تستخدم هذه الورقة قيود الساعات للسماح بتنفيذ إجراءات لقطة متزامنة
2. معالجة الإجراءات الفورية: دعم الإجراءات ذات المدة الصفرية من خلال إضافة تحول iea
3. التحقق الرسمي: أول توفير لإثبات صحة معتمد على الآلة لهذا النوع من الترميز
4. تبسيط الدلالات: تصميم دلالات تخطيط زمني أكثر ملاءمة للاستدلال الرسمي

إعداد التجارب

بيئة التحقق الرسمي

• مثبت النظريات: Isabelle/HOL
• فاحص الشهادات: فاحص الشهادات المُحقق من قبل Wimmer و von Mutius
• الخاصية المستهدفة: فحص القابلية للوصول A ⊨ EF(loc(AM) = goal)

إحصائيات حجم الكود

المقارنة مع الأعمال ذات الصلة

مقارنة الحجم مع الأعمال الرسمية ذات الصلة:

• مخطط قائم على SAT مُحقق: ~17,500 سطر
• فاحص تخطيط كلاسيكي مُحقق: ~3,000 سطر
• فاحص تخطيط زمني PDDL مُحقق: ~6,500 سطر

نتائج التجارب

النتائج النظرية الرئيسية

النظرية 1 (نظرية الصحة الرئيسية): إذا كانت الخطة π صحيحة وخالية من التداخل الذاتي (valid(π) ∧ no_self_overlap(π))، فإن الادعاء A ⊨ EF(loc(AM) = goal) يكون صحيحاً.

هيكل الإثبات:

1. المساعدة 1: بناء محاكاة تحفز الخطة المتوازية
2. المساعدة 2: القابلية للوصول من التكوين الأولي إلى الحالة المرمزة
3. المساعدة 3: التحول من الحالة النهائية إلى التكوين الهدف

نتائج التحقق الرسمي

1. إثبات الاكتمال: إثبات ناجح لاكتمال الترميز، أي أن كل خطة صحيحة يمكن العثور عليها في تشغيل صحيح في شبكة الآلات الزمنية المقابلة
2. الفحص الآلي: تم فحص جميع الإثباتات بواسطة Isabelle/HOL، مما يوفر أعلى مستويات ضمان الموثوقية
3. التصميم المعياري: هيكل الإثبات معياري، مما يسهل الفهم والصيانة

التحقق من التنفيذ الهندسي

تم تكييف تنفيذ الترميز ليكون متوافقاً مع صيغة فاحص الشهادات المُحقق الموجود، مما يشكل سلسلة شهادة قابلة للتنفيذ كاملة.

الأعمال ذات الصلة

شهادة التخطيط الكلاسيكي

• صمم Eriksson وآخرون مخططات شهادة مختصرة لعدم القابلية للحل للتخطيط الكلاسيكي
• قدم Abdulaziz و Lammich فاحص تحقق رسمي للتخطيط الكلاسيكي

التخطيط الزمني وفحص النماذج

• نفذ Dierks وآخرون تقليصاً ثابتاً لمجموعة فرعية من PDDL إلى آلات زمنية
• عرّف Heinz وآخرون ترميزاً صريحاً لمسائل التخطيط الزمني إلى آلات زمنية
• درس Gigante وآخرون تعقيد التخطيط الزمني على المستوى النظري

طرق التحقق الرسمي

• طور Abdulaziz و Kurz نظاماً معتمداً على SAT للتخطيط باستخدام طريقة مماثلة
• استخدم Kumar وآخرون و Leroy طريقة التحقق التدريجي من الترميز في التحقق من المترجمات

الخلاصة والمناقشة

الاستنتاجات الرئيسية

1. التحقق من الجدوى: إثبات أن الشهادة الرسمية لعدم قابلية حل التخطيط الزمني ممكنة
2. الضمانات النظرية: توفير ضمانات صحة قوية من خلال مثبت النظريات
3. التنفيذ الهندسي: بناء سلسلة أدوات شهادة كاملة بنجاح

القيود

1. قيود الإدخال: حالياً يقبل فقط مسائل تخطيط زمني مُنفذة كإدخال
2. مجموعة فرعية من الدلالات: الدلالات المدعومة هي مجموعة فرعية من فاحص التحقق من التخطيط المُحقق
3. القابلية للتنفيذ: آلية الشهادة لم تكن قابلة للتنفيذ بالكامل بعد

الاتجاهات المستقبلية

1. إثبات التكافؤ: التخطيط لإثبات رسمي لتكافؤ دلالات هذه الورقة مع دلالات فاحصات التحقق الموجودة
2. التنفيذ القابل للتنفيذ: تطوير فاحص شهادات قابل للتنفيذ
3. التحقق من الإنشاء: إضفاء الطابع الرسمي على خوارزميات الإنشاء، مثل حل Helmert للسجلات البيانية
4. تخفيف القيود: البحث في إمكانية تخفيف شرط عدم التداخل الذاتي

التقييم المتعمق

المميزات

1. الصرامة النظرية: أول إثبات رسمي معتمد على الآلة لشهادة عدم قابلية حل التخطيط الزمني
2. الاكتمال الهندسي: لا توفر إطار عمل نظري فقط، بل تنفيذ التكامل مع الأدوات الموجودة
3. ابتكار الطريقة:
   • تصميم ترميز يدعم التنفيذ المتزامن
   • حل أنيق لمعالجة الإجراءات الفورية
   • تصميم دلالات مبسطة وتكافؤة
4. ضمان الموثوقية: توفير أعلى مستويات ضمان الصحة من خلال مثبت النظريات

أوجه القصور

1. قيود الاستخدام العملي:
   • يتطلب إدخالاً مُنفذاً مسبقاً
   • لم يكن قابلاً للتنفيذ بالكامل بعد
   • نقص تقييم الأداء
2. نطاق التغطية: يدعم فقط مجموعة فرعية من التخطيط الزمني، لا يدعم ميزات PDDL الكاملة
3. قابلية التوسع: حجم العمل الرسمي البالغ 18,000 سطر كبير نسبياً، مما يزيد من تكاليف الصيانة

التأثير

1. المساهمة الأكاديمية:
   • ملء الفجوة في التحقق الرسمي للتخطيط الزمني
   • توفير أساس نظري جديد لشهادة عدم القابلية للحل
   • إظهار جدوى التحقق الرسمي للأنظمة المعقدة
2. القيمة العملية:
   • توفير شهادة نظام تخطيط موثوق للتطبيقات الحرجة
   • قابلية التوسع إلى أشكال تخطيط أخرى ومسائل رضا القيود
   • توفير مرجع لتطوير أدوات التحقق الآلي
3. قابلية التكرار: بناءً على Isabelle/HOL مفتوح المصدر، قابل للتكرار نظرياً بالكامل

السيناريوهات المطبقة

1. الأنظمة الحرجة: تطبيقات التخطيط التي تتطلب ضمانات موثوقية عالية (مثل الفضاء والأجهزة الطبية)
2. أدوات البحث: توفير البنية التحتية للتحقق الرسمي لبحث التخطيط الزمني
3. الاستخدام التعليمي: كحالة دراسية لتدريس الطرق الرسمية وخوارزميات التخطيط
4. تطوير الأدوات: توفير أساس نظري لتطوير أدوات تخطيط موثوقة

المراجع

تتضمن المراجع الرئيسية:

• Abdulaziz & Koller (2022): دلالات رسمية للتخطيط الزمني وفاحص
• Heinz et al. (2019): ترميز التخطيط الزمني إلى آلات زمنية
• Wimmer & von Mutius (2020): فاحص شهادات معتمد للآلات الزمنية
• Abdulaziz & Kurz (2023): نظام تخطيط معتمد قائم على SAT

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