Module checking of pushdown multi-agent systems
تثبت هذه الورقة أن التحقق من الوحدات لأنظمة الوكلاء المتعددين ذات المكدس هو مسألة كاملة من فئة 2EXPTIME بالنسبة لمواصفات ATL، ولكنه مسألة كاملة من فئة 4EXPTIME بالنسبة لمواصفات *ATL، مما يمثل حالة نادرة لمسألة قرار أولية تتجاوز تعقيدها الزمن الأسي الثلاثي.