1215 ورقة بحثية
تثبت هذه الورقة أن الأهداف الموضعية المستقلة عن البادئة في مع وجود حرف محايد تتميز بكونها أوتوماتات "co-Büchi" رتيبة وحتمية التاريخ فوق الأعداد الترتيبية المعدودة، وهي نتيجة تعمم معايير سابقة، وتقدم برهاناً جديداً على الانغلاق تحت عملية الاتحاد، وتثبت موضعية ألعاب متوسط الدفع عبر الرسوم البيانية التعسفية، وتُظهر خاصية الاكتمال للأهداف الموضعية فوق الرسوم البيانية المحدودة.
تتقصى هذه الورقة البحثية المحولات -الآفينية (affine -transducers) كنموذج للدوال من شجرة إلى شجرة، حيث تُثبت أن متغيراتها الآفينية تكافئ محولات المشي على الأشجار (tree-walking transducers)، وأن امتداداً غير خطي طفيفاً منها يطابق القدرة التعبيرية لمحولات الأشجار ذات الحصى غير المرئية (invisible pebble tree transducers)، مع استناد البراهين إلى آلة التفاعل المجردة (Interaction Abstract Machine) لحل فرضية عدم القدرة على التعبير.
تتقصى هذه الورقة بنية دوائر بتري (Petri's cycloids) من خلال تعريف نظم اختزال لتوصيف الأشكال غير القابلة للاختزال، واستخلاص طريقة لتوليف المعلمات من بنيات الشبكة، مما يؤدي إلى إرساء إجراء قرار فعال لتماثل الدوائر.
تقدم هذه الورقة لغة كوريوجرافية احتمالية لنمذجة الأنظمة المتزامنة من منظور عالمي، والتي تم ترميزها رسميًا في أداة التحقق من النماذج PRISM لتمكين التحقق الصارم من خصائص النظام وموثوقيته.
تقدم هذه الورقة نظرة شاملة على {log}، وهي لغة برمجة المنطق المقيد التي تطورت إلى بيئة تحقق رسمي متكاملة قادرة على التعامل مع آلات الحالة باعتبارها برامج قابلة للتنفيذ ومواصفات في آن واحد من خلال ميزات مثل إثبات النظريات الآلي، وتوليد شروط التحقق، وتوليد حالات الاختبار.
تقدم هذه الورقة الأشكال الطبيعية العادية الاحتمالية (PDNFs) كإطار عمل جديد يخصص أوزانًا ذات قيم حقيقية للمتغيرات لترميز عدم اليقين، مؤسسةً بنية فضاء باناخ التي تجسر الفجوة بين المنطق، والتحليل الدالي، ودمج الأدلة البايزية للاستدلال حول المنطق الزمني والتوزيعات الاحتمالية.
تقدم هذه الورقة إطاراً نظرياً شبكياً (lattice-theoretical) باستخدام الروابط الغالواية (Galois connections) لبناء شهود (witnesses) تستنتج استراتيجيات فوز في ألعاب النقطة الثابتة الأولية والمزدوجة، مما يتيح التحقق من النقاط الثابتة الصغرى وتطبيقها على مشكلات مثل تمييز الصيغ في الأنظمة الاحتمالية وإثبات احتمالات التوقف في سلاسل ماركوف.
تتقصى هذه الورقة أي من نظريات القابلية للتعريف والتحفظ الجهوية الكلاسيكية تظل صالحة عند تقييدها بالبنى المتناهية، مبرهنةً على أنه في حين تفشل بعض نتائج التحفظ من الدرجة الأولى، فإن التوصيفات الدلالية الرئيسية ونظرية سلامة التماثل (Bisimulation Safety Theorem) تنتقل بنجاح إلى المجال المتناهي.
تقدم هذه الورقة إطاراً جبرياً قائماً على مجموعات التبديل وأنظمة إعادة كتابة السلاسل لتوصيف وبناء شواهد السياقية المستقلة عن الحالة، مما يوفر نهجاً موحداً لتحليل اللاكلاسيكية الكمومية وتطبيقاتها في التفوق الكمومي.
تُبين هذه الورقة أن نظرية النوع المتجانس (homotopy type-theory) الممتدة باستخدام جهات تعديل (modalities) محددة من نوع "lex" و"accessible"، يمكنها إعادة بناء مخططات الـ -logoses، مما يتيح الاستدلال حول عدة -logoses في آن واحد ويقدم تعميماً عالي الأبعاد لنموذج ستيرلينغ للحوسبة التايتية الاصطناعية (Sterling's synthetic Tait computability).