Axiomatisation for an asynchronous epistemic logic with sending and receiving messages

إليك ملخص تقني مفصل لورقة "Axiomatisation for an asynchronous epistemic logic with sending and receiving messages" من إعداد بالبياني، وفان ديمتارش، وليروفيلوايس.

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

تعالج الورقة تحدي نمذجة الاتصال غير المتزامن في الأنظمة متعددة الوكلاء باستخدام المنطق الإبستمي الديناميكي (DEL).

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

العمل السابق (تحديدًا المرجع [4]) قدم صياغة ($AA$) للصلاحيات من نوع $\epsilon$ باستخدام نظام اختزال (اختزال الصيغ الديناميكية إلى صيغ إبستيمية ثابتة). ومع ذلك، فإن نهج الاختزال هذا يفشل بالنسبة للصلاحيات من نوع $\ast$ لأن خصائص النظام تتغير جذرياً بمجرد وجود تاريخ (على سبيل المثال، قد يكون لدى الوكلاء أعداد مختلفة من الرسائل المستلمة).

2. المنهجية

2.1 اللغة والتركيب (Syntax)

يعرف المؤلفون لغة $\mathcal{L}$ توسع المنطق الموديلي متعدد الوكلاء عبر نوعين من الصيغ الديناميكية:

• البث (Broadcasting): $\langle \varphi \rangle \psi$ (يتم الإعلان عن/بث الصيغة $\varphi$؛ ومن ثم تتحقق $\psi$).
• الاستلام (Receiving): $\langle a \rangle \psi$ (يستلم الوكيل $a$ الرسالة التالية في طابوره؛ ومن ثم تتحقق $\psi$).
• كلمات التاريخ (History Words): تمثل تسلسلات الوكلاء والصيغ (مثل $p.a.q$) تسلسل الأحداث. التاريخ هو كلمة حيث لا يتجاوز عدد الرسائل المستلمة لكل وكيل عدد الرسائل المرسلة (قيد FIFO - الوارد أولاً يُصرف أولاً).

2.2 الدلالات (Semantics)

تُعرف الدلالات على أزواج $(s, \alpha)$، حيث $s$ هي حالة في نموذج كريبكي و $\alpha$ هي كلمة تاريخ.

• قابلية التنفيذ ($\triangleright\triangleleft$): علاقة تحدد ما إذا كان يمكن تنفيذ التاريخ $\alpha$ في الحالة $s$. وهذا يضمن أن:
  1. التاريخ هو تسلسل صالح (FIFO).
  2. جميع الصيغ المعلن عنها كانت صحيحة في لحظة بثها.
  3. الوكلاء لا يعتبرون إلا التواريخ القابلة للتنفيذ في الحالات التي يعتبرونها ممكنة.
• علاقة الرؤية ($\triangleright_a$): تحدد ما يعتبره الوكيل $a$ ممكناً. يعتبر الوكيل $a$ التاريخ $\beta$ ممكناً بالنسبة للتاريخ الفعلي $\alpha$ إذا تطابق تسلسل الرسائل التي استلمها $a$ في $\beta$ تماماً مع ما استلمه في $\alpha$. ومن الأهمية بمكان أن الوكلاء لا يتخيلون تواريخ تحتوي على رسائل لم يستلموها بعد.
• الطابع ثلاثي القيم: تتصرف الدلالات بشكل يشبه المنطق ثلاثي القيم. إذا لم يكن التاريخ قابلاً للتنفيذ في حالة ما ($s \not\triangleright\triangleleft \alpha$)، فإن الصيغ تكون لا صحيحة ولا خاطئة في ذلك الزوج، رغم أن المنطق يحتفظ بالصلاحيات القياسية.

2.3 الصيغة "الفارغة" (The "Empty" Formula)

الابتكار التقني المركزي هو تعريف الصيغة empty:
$$\text{empty} := \bigwedge_{a \in A} [a]\bot \land \bigwedge_{a,b \in A} K_a [b]\bot$$
تحدد هذه الصيغة الحالة التي يكون فيها التاريخ فارغاً ($\alpha = \epsilon$). وهي تؤكد أنه لم يتم استلام أي رسائل من قبل أي شخص، وأن الجميع يعرفون ذلك. وهذا لا يكون ممكناً إلا في بيئة متعددة الوكلاء ($|A| \ge 2$).

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

3.1 الصياغة $AA^*$

المساهمة الأساسية هي اقتراح $AA^*$، وهي صياغة لـ الصلاحيات من نوع $\ast$ (الصلاحيات الدائمة).

• الطبيعة اللانهائية: على عكس النظام السابق القائم على الاختزال $AA$، فإن $AA^*$ هو نظام لانهائي. لا يمكنه اختزال الصيغ الديناميكية إلى صيغ ثابتة لأن حقيقة الصيغ تعتمد على تاريخ محدد.
• القاعدة $(R^*)$: يتضمن النظام قاعدة لانهائية:
  • المقدمة: لكل الكلمات $\alpha$، يكون $\text{empty} \to [\alpha]\varphi$ قابلاً للاشتقاق.
  • النتيجة: $\varphi$ قابلة للاشتقاق.
    تعمل هذه القاعدة فعلياً على تقليص الصلاحية من نوع $\ast$ إلى الصلاحية من نوع $\epsilon$ عبر "إعادة ضبط" التاريخ إلى الحالة الفارغة عبر صيغة empty.
• البديهيات (Axioms): يتضمن النظام بديهيات لـ:
  • توزيع المعرفة والعمليات الديناميكية.
  • شروط قابلية التنفيذ (مثلاً، لا يمكن استلام رسالة إلا إذا تم إرسالها).
  • الثبات الذري (قيم الحقيقة للذرات لا تتغير).
  • بديهية محددة للمعرفة في البيئات غير المتزامنة: $\text{empty} \to (K_a \varphi \leftrightarrow ([\alpha]\bot \lor \bigvee_{\alpha \triangleright_a \beta} K_a [\beta]\varphi))$.

3.2 الاكتمال والصلاحية (Completeness and Soundness)

• الصلاحية (Soundness): يثبت المؤلفون أن كل نظرية في $AA^*$ هي $\ast$-صحيحة.
• الاكتمال (Completeness): يثبتون أن كل صيغة $\ast$-صحيحة هي نظرية في $AA^*$. تستخدم عملية الإثبات بناء النموذج القانوني (canonical model construction) بناءً على النظريات المتسقة القصوى. كانت هناك عقبة تقنية كبيرة في تعريف علاقات الوصول في النموذج القانوني لضمان أنها تشكل علاقات تكافؤ فقط عند تقييدها بالنظريات التي تحتوي على empty.

3.3 محدودية الوكيل الواحد

توضح الورقة بصرامة أن الطريقة المقترحة تفشل في حالة الوكيل الواحد.

• في نظام الوكيل الواحد، يعرف الوكيل دائماً أنه استلم جميع الرسائل التي رآها. لا توجد صيغة مكافئة لـ empty يمكنها التمييز بين تاريخ فارغ وتاريخ غير فارغ استلم فيه الوكيل كل شيء.
• وبناءً عليه، فإن الاختزال من الصلاحية $\ast$ إلى الصلاحية $\epsilon$ عبر empty مستحيل في حالة الوكيل الواحد. وقد ترك المؤلفون صياغة حالة الوكيل الواحد كمسألة مفتوحة.

4. النتائج

1. النظام الرسمي: صياغة لانهائية كاملة وصحيحة ($AA^*$) للمنطق الإبستمي غير المتزامن مع فصول متميزة للإرسال والاستلام.
2. آلية الاختزال: طريقة مبتكرة للتعامل مع "الصلاحية الدائمة" باستخدام صيغة empty لربط المنطق بالوضع الابتدائي، مما يتجاوز الحاجة إلى نظام اختزال منتهي.
3. المقارنة مع S5: لا يحقق المنطق بديهية الحقيقة القياسية لـ S5 ($K_a \varphi \to \varphi$) بشكل عالمي. المعرفة تكون واقعية فقط إذا عرف الوكيل أن التاريخ فارغ. خلاف ذلك، تعمل الـ Modality كـ "اعتقاد متسق".
4. المقارنة مع الحوسبة الموزعة: تتوافق الدلالات مع مفهوم القطع المتسق (consistent cuts) في الأنظمة الموزعة ولكنها تهذبها عبر دمج شروط الحقيقة (قابلية التنفيذ) مباشرة في المنطق، مما يمنع الحالات غير المتسقة (مثل استلام رسالة قبل إرسالها، أو استلام إعلان خاطئ).

5. الأهمية

• التقدم النظري: يجسد هذا العمل الفجوة بين المنطق الإبستمي الديناميكي القياسي (الذي يفترض التزامن) وواقع الحوسبة الموزعة (عدم التزامن). إنه يوفر أول إطار منطقي صارم يعامل الإرسال والاستلام كأحداث منفصلة وغير متزامنة ذات صيغ متميزة.
• نمذجة عدم اليقين الزمني: ينجح في نمذجة النوع المحدد من عدم اليقين حيث لا يعرف الوكلاء طول تاريخ الاتصال بالنسبة للآخرين، وهو سيناريو شائع في بروتوكولات النشر (gossip protocols) والاتفاق الموزع.
• الابتكار المنهجي: يوفر استخدام القاعدة اللانهائية ($R^*$) مع صيغة "إعادة الضبط" (empty) نموذجاً جديداً لصياغة المنطقيات التي لا يمكن اختزال خصائصها الديناميكية إلى خصائص ثابتة عبر إعادة كتابة منتهية.
• الاتجاهات المستقبلية: تحدد الورقة مسارات واضحة للبحث المستقبلي، بما في ذلك التوسع في المعرفة الجماعية (المعرفة الموزعة)، والاتصال غير العام، وحل مشكلة صياغة الوكيل الواحد.

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