يُعد التحقق المحدود من النموذج (Bounded Model Checking) تقنية فعالة للتحقق الرمزي، تتيح التحقق من الخصائص المرغوبة لنظام برمجي عبر تشغيلات محدودة لنموذج مجرد للنظام. وتُصاغ هذه الخصائص غالبًا باستخدام منطق زمني معين، بينما يُمثل النظام كنظام انتقال حالة. في هذه الورقة، نقترح منطقًا جديدًا للعد، يُرمز إليه بـ $\mathcal{L}{C}$LC، لوصف الخصائص الزمنية لأنظمة العميل-الخادم التي تضم عددًا غير محدود من العملاء. كما نقترح استراتيجية جديدة تُسمى التحقق المحدود من النموذج ثنائي الأبعاد ($2D$2D-BMC)، والتي تستخدم معلمتين متمايزتين: إحداهما تمثل عدد خطوات التنفيذ، والأخرى تمثل عدد الرموز (tokens) في الشبكة التي تمثل نظام العميل-الخادم، حيث تتطور هاتان المعلمتان بشكل منفصل، وهو ما يختلف عن التقنيات القياسية للتحقق المحدود من النموذج في صيغة الشبكات البترية (Petri Nets). تم تنفيذ هذه الاستراتيجية $2D$2D-BMC في أداة تُسمى DCModelChecker، التي تستفيد من تقنية $2D$2D-BMC مع مُحلِّل قابلية التحقق المُحدَّدة بالنظرية (SMT) من الجيل الحديث Z3. يتم إدخال النظام كشبكة بترية، وتُحوَّل الخصائص المحددة باستخدام منطق $\mathcal{L}{C}$LC إلى صيغ رياضية تُختبر بواسطة المُحلِّل. كما يمكن لأداتنا العمل على معايير صناعية من مسابقة التحقق من النماذج (Model Checking Contest - MCC). ونُقدِّم نتائج هذه التجارب لتوضيح مدى ملاءمة واستخدامية استراتيجية $2D$2D-BMC.