التوصيفات النظرية الآلية للمنطق الزمني المتفرع

تخدم نظريات التوصيف كأدوات مهمة في نظرية النماذج ويمكن استخدامها لتقييم ومقارنة القوة التعبيرية للغات الزمنية المستخدمة في تحديد والتحقق من الخصائص في الأساليب الرسمية. بينما تم تأسيس روابط كاملة لحالة الزمن الخطي بين المنطق الزمني واللوجيكات المرتبطة والنماذج الجبرية والآلات، لا تزال الحالة في حالة الوقت المتفرع أكثر تفككاً بشكل ملحوظ. في هذا العمل، نقدم توصيفاً نظرياً آلياً لبعض المنطق الزمني المتفرع المهم، وهي CTL* و ECTL* المفسرة على أشجار ذات تفرعات عشوائية، من خلال تحديد نوعين من آلات الأشجار المترددة التي تم إثبات تكافؤها مع تلك المنطقيات. تنطبق هذه التوصيفات أيضاً على منطق المسار الأحادي وشظية المحاكاة المراعية في منطق السلاسل الأحادية، مرة أخرى المفسرة على الأشجار. هذه النتائج توسع مساحة التوصيف لحالة الوقت المتفرع وتحل سؤالاً مفتوحاً عمره أربعون عاماً.