تحقق من بروتوكولات السكان مع بيانات غير مرتبة

بروتوكولات السكان هي نموذج مدروس جيدًا للحوسبة الموزعة حيث يتواصل مجموعة من الوكلاء غير المعروفين ذوي الحالة المحدودة من خلال تفاعلات ثنائية. معًا يقررون ما إذا كانت تكوينهم الابتدائي، أي التوزيع الابتدائي للوكلاء في الحالات، يلبي خاصية معينة. كإضافة من أجل التعبير عن خصائص المجموعات المتعددة في نطاق بيانات لانهائي، قدم بلوندان و لادوكر (ICALP'23) بروتوكولات السكان مع بيانات غير مرتبة (PPUD). في PPUD، يحمل كل وكيل قيمة بيانات ثابتة، وتعتمد التفاعلات بين الوكلاء على ما إذا كانت بياناتهم متساوية أم لا. كما حدد بلوندان و لادوكر الفئة المثيرة للاهتمام من بروتوكولات PPUD للملاحظة الفورية (IOPPUD)، حيث يبقى أحد الوكيلين في كل انتقال غير نشط ولا يتحرك، وقد وصفوا قوتها التعبيرية. ندرس قابلية التحليل والتعقيد للتحقق رسميًا من هذه البروتوكولات. المشكلة الرئيسية للتحقق من بروتوكولات السكان هي التحديد الجيد، أي التحقق مما إذا كان الـ PPUD المعطى يحسب وظيفة معينة. نظهر أن التحديد الجيد غير قابل للحل بوجه عام. بالمقابل، بالنسبة لـ IOPPUD، نعرض فئة كبيرة لكنها طبيعية من المشاكل، والتي تشمل التحديد الجيد من بين مشاكل كلاسيكية أخرى، ونثبت أن هذه المشاكل تقع في EXPSPACE. كما نقدم حد أدنى من التعقيد، وهو صعوبة coNEXPTIME.