1215 ورقة بحثية
تثبت هذه الورقة أن تحديد ما إذا كان نظام اتصالات صندوق بريد ذو حالة محدودة قابلاً للمزامنة في ظل دلالات قائمة على الجولات دون قيود على الحجم هو مسألة معقدة من فئة PSPACE-complete، وذلك من خلال نهج جديد قائم على الأتمتة يعمل أيضاً على تنقيح تعقيد الأسئلة ذات الصلة.
تثبت هذه الورقة أن التحقق من توازنات اللعبة الفرعية الكاملة في أنظمة الألعاب المتزامنة الاحتمالية ذات الأفق المحدود يقع ضمن فئة PSPACE، بينما التحقق من توازنات ناش هو مسألة EXPTIME-complete، وهي نتيجة غير متوقعة تُظهر أن مفهوم التوازن الأكثر دقة هو الأسهل حوسبياً من حيث التحقق مقارنة بالمفهوم القياسي.
يتتبع هذا الاستطلاع تطور أداة فحص النماذج ESBMC من أصولها في عام 2009 إلى وضعها في عامي 2025-2026 كمنصة تحقق متعددة الاستخدامات، وحائزة على جوائز، ومستقلة ذاتياً بشكل أصيل، ومتكاملة مع الوكلاء الذكيين وأطر العمل الصناعية، مع تحليل تأثيرها الاقتصادي وتحديد التحديات المستقبلية في التحقق الرسمي من البرمجيات.
تُثبت الورقة البحثية أن الحساب الحقيقي غير الخطي (NRA)، كما هو مُعرَّف في معيار SMTLIB، هو مسألة غير قابلة للتقرير لأن معاملته للقسمة على صفر كدالة غير مفسرة تُمكِّن من ترميز مسائل الحساب الصحيح غير القابلة للتقرير.
تؤسس هذه الورقة إطاراً نظرياً برهانياً للتفسير المجرد من خلال البناء المنهجي لأنظمة منطقية تتوافق بنياتها الجبرية مع شبكات مجردة معطاة، مما يوحد تحليل البرامج مع نظرية البرهان والمنطق الجبري عبر نتائج السلامة والاكتمال.
تقدم هذه الورقة عائلة من علاقات المحاكاة "شبه العادلة" للأنظمة الانتقالية ذات شروط عدالة بوشي (Büchi) التي تبسط عملية الاستنتاج من خلال قواعد استنتاجية حدسية، مما يوفر بديلاً أكثر سهولة لعلاقات المحاكاة العادلة القياسية المعقدة لإثبات الاحتواء العادل للمسارات في التحقق التفاعلي.
تقدم هذه الورقة منطق فعل الوجوب (DAML)، وهو إطار نمطي ديناميكي مستحدث يوسع منطق نموذج الفعل لاستخلاص الالتزامات الحساسة للسياق في الأنظمة متعددة الوكلاء من خلال تقييم الأفعال بناءً على قيمتها الوجوبية المتوقعة، وتؤسس لسلامته واكتماله وقدرته التعبيرية من خلال الصياغة البديهية ودراسات حالة مثل لغز المنقبين.
تقدم هذه الورقة mstlo، وهي مكتبة لغة Rust عالية الأداء مع روابط لغة بايثون تتيح المراقبة الفورية والفعالة للمنطق الزمني الإشاري من خلال واجهة موحدة، وخوارزمية برمجة ديناميكية تراكمية مع التخزين المؤقت، ولغة مجال محدد مدمجة، مما يظهر تحسينات كبيرة في القابلية للتوسع مقارنة بالأدوات الحالية.
تقدم هذه الورقة منطق سيمبليشيال ديونطي (DSL) وامتداده الديناميكي (DDSL)، وهما إطاران جديدان يستخدِمان المعقدات السيمبليشيالية لنمذجة الالتزامات الفردية، والواجبات الجماعية، وآثار الأفعال المشتركة صوريًا، مع إثبات سلامتهما واكتمالهما.
تقترح هذه الورقة بنية تحقق هجينة عصبية-رمزية تجمع بين الاستدلال المنطقي الصوري والتحليل الدلالي العصبي للكشف بفعالية عن الهلوسة وضمان الموثوقية في المحتوى الذي تولده النماذج اللغوية الكبيرة للمجالات عالية المخاطر والحساسة للبيانات، كما تم التحقق من ذلك من خلال انخفاض بنسبة 30% في وقت إنشاء التقارير ومعدلات كشف عالية في نظام تقييم أجهزة طبية في العالم الحقيقي.