ماذا يعني CTL في الخوارزميات وهياكل البيانات؟ شرح مبسّط مع أمثلة

اختصار CTL يعني Computation Tree Logic، أي «منطق الحوسبة الشجرية»، وهو نوع من المنطق الزمني (Temporal Logic) يُستخدم في علوم الحاسوب لوصف سلوك الأنظمة عبر الزمن والتحقق آليًا من صحتها. الأهم أن تعرف هذا من البداية: CTL ليس هيكل بيانات ولا خوارزمية ترتيب أو بحث، بل لغة صياغة منطقية نكتب بها «شروطًا» عن النظام، ثم نتحقق هل يحققها أم لا. لهذا يظهر اسمه غالبًا في مواد «التحقق الرسمي» و«فحص النماذج»، لا في درس المصفوفات أو الأشجار الثنائية.

لماذا يرتبط CTL بالخوارزميات وهياكل البيانات؟

الرابط ليس في تخزين البيانات، بل في التحليل. تخيّل نظامًا له حالات كثيرة تتغيّر بمرور الوقت: إشارة مرور، بروتوكول شبكة، أو نظام تحكم صناعي. نمثّل هذا النظام برسم بياني موجّه من الحالات والانتقالات يُسمى بنية كريبكه (Kripke Structure). عندما «نفكّ» هذا الرسم بدءًا من الحالة الابتدائية نحصل على شجرة حسابية لا نهائية تمثّل كل المسارات الممكنة للتنفيذ. من هنا جاء الاسم: CTL يصف خصائص على هذه الشجرة.

ولأن التحقق يتم على رسم بياني ضخم، فهو في صميمه مسألة خوارزميات وهياكل بيانات: خوارزمية فحص CTL تعمل بزمن خطي تقريبًا بالنسبة لحجم النظام وطول الشرط، أي بحدود O(|S| × |φ|) حيث |S| عدد الحالات و|φ| طول المعادلة. هذه الكفاءة أحد أسباب شهرة CTL عمليًا.

كيف تُقرأ صيغ CTL؟

تتكوّن كل صيغة في CTL من جزأين متتاليين:

• مكمّم مسار يحدد «أي المسارات» نقصد: A تعني «على كل المسارات» (All)، وE تعني «يوجد مسار واحد على الأقل» (Exists).
• عامل زمني يحدد «متى» تتحقق الحالة: X (التالي/neXt)، F (في النهاية/Finally)، G (دائمًا/Globally)، U (حتى/Until).

نجمع بينهما فنقرأ الصيغة بسهولة:

1. AG p — «في كل مسار وكل الأوقات تبقى الخاصية p صحيحة» (خاصية أمان، مثل: النظام لا يدخل حالة خطأ أبدًا).
2. EF p — «يوجد مسار يصل في النهاية إلى p» (قابلية الوصول، مثل: من الممكن الوصول إلى حالة إعادة التشغيل).
3. AF p — «على كل المسارات سنصل حتمًا إلى p» (خاصية حيوية، مثل: كل طلب يُخدَم في النهاية).
4. AG(request → AF grant) — «كلما وُجد طلب، فسيُلبّى حتمًا لاحقًا».

CTL أم LTL؟ الفرق جوهري

كثيرون يخلطون بين CTL وLTL (المنطق الزمني الخطي). الفرق أن LTL يفكّر في مسار تنفيذ واحد كخط مستقيم، بينما CTL يفكّر في شجرة متفرّعة من المستقبلات الممكنة، ولهذا يملك مكمّمات المسارات A وE.

الجانب	CTL	LTL
نموذج الزمن	متفرّع (شجرة مستقبلات)	خطي (مسار واحد)
مكمّمات المسار	نعم (A وE)	لا
التعبير عن «يوجد مسار ما»	ممكن مباشرة (EF)	غير ممكن
تعقيد الفحص	خطي في حجم النظام	أسّي في طول الصيغة
أدوات شائعة	NuSMV، SMV	SPIN

لا يحتوي أحدهما الآخر بالكامل؛ وهناك منطق أشمل يجمعهما اسمه ‏*CTL يتيح خلط المكمّمات والعوامل بحرّية أكبر.

انتبه: CTL ليست STL

هذا أكثر خلط شائع لمن يدرس الخوارزميات وهياكل البيانات. إن كنت تقصد المكتبة التي تعطيك جاهزًا vector وmap وset وخوارزميات الفرز والبحث في ++C، فتلك اسمها STL أي Standard Template Library، وهي شيء مختلف تمامًا عن CTL. تشابه الحروف يوقع كثيرين، فتأكد أيّهما تريد قبل البحث. وإن كنت تدرس التحقق من صحة البرمجيات والأنظمة المتزامنة، فالمقصود فعلًا هو CTL.

خطوات استخدام CTL عمليًا

1. حدّد المواصفة بلغة طبيعية، مثل: «يجب ألا يفتح المصعد بابه أثناء الحركة».
2. انمذج النظام كبنية حالات وانتقالات (Kripke Structure) داخل أداة فحص نماذج.
3. صُغ الشرط بـ CTL، مثل AG(moving → ¬doorOpen).
4. شغّل أداة الفحص (مثل NuSMV) لتفحص كل الحالات الممكنة تلقائيًا.
5. حلّل النتيجة: إن فشل الشرط تعطيك الأداة مسارًا مضادًا (Counterexample) يوضّح تسلسل الخطوات المؤدي للخطأ، فتصلح النموذج وتعيد الفحص.

نصيحة عملية من التطبيق الفعلي: ابدأ بخصائص أمان بسيطة من نوع AG قبل الانتقال إلى الخصائص الحيوية المعقّدة، لأن أخطاء الأمان أسهل في التشخيص، كما أن الخطأ الأشيع للمبتدئين هو الخلط بين AF (سيحدث حتمًا) وEF (قد يحدث)؛ اختيار المكمّم الخاطئ يجعل الشرط يمرّ رغم أن النظام معطوب.

الأسئلة الشائعة

هل CTL خوارزمية؟ لا، CTL لغة منطقية لوصف الخصائص. الخوارزمية هي «مُدقّق النموذج» الذي يفحص هل النظام يحقق صيغة CTL.

هل أحتاج CTL في مشاريعي اليومية؟ غالبًا لا في تطبيقات الويب العادية، لكنها أساسية في الأنظمة الحرجة: العتاد، بروتوكولات الاتصال، وأنظمة التحكم التي لا يُحتمل فيها الخطأ.

من ابتكر CTL؟ طُوّر مطلع الثمانينيات ضمن أبحاث فحص النماذج التي نال روّادها (كلارك وإيمرسون وسيفاكيس) جائزة تورينغ عام 2007.

ما الفرق بين CTL وCTL؟* ‏*CTL منطق أعمّ يسمح بدمج مكمّمات المسار والعوامل الزمنية بمرونة أكبر، ويحتوي CTL وLTL معًا كحالتين خاصتين منه.