المنطق الزمني والجهوي في الحوسبة

يوسع المنطق الزمني والجهوي المنطق الكلاسيكي بإضافة عوامل للزمن والإمكانية، مما يوفر لغات دقيقة لتحديد كيفية تصرف برنامج أو نظام تفاعلي على مدار تنفيذه بالكامل.

Definition

يعزز المنطق الزمني المنطق الافتراضي أو منطق الرتبة الأولى بعوامل تصف متى تتحقق الخصائص على طول عملية حسابية، مثل دائمًا، في النهاية، وحتى؛ ويعمم المنطق الجهوي هذا بعوامل للضرورة والإمكانية على هيكل من الحالات والانتقالات.

Scope

يغطي هذا الموضوع المنطق الزمني الخطي والمتفرع مثل LTL و CTL، والمنطق الجهوي بما في ذلك المنطق الديناميكي وحساب التفاضل والتكامل الجهوي (modal mu-calculus)، والتعبير عن خصائص السلامة والحيوية، والمشكلات الخوارزمية للتحقق من النموذج (model checking) والقابلية للتحقق (satisfiability) التي تجعل هذه المنطق محورية في التحقق الآلي.

Core questions

• كيف يمكن للمنطق أن يعبر عن أن شيئًا جيدًا سيحدث في النهاية أو أن شيئًا سيئًا لن يحدث أبدًا؟
• ما الفرق بين الاستدلال على تنفيذ واحد والاستدلال على جميع الاحتمالات المستقبلية الممكنة؟
• كيف يتم جعل التحقق مما إذا كان النظام يفي بخاصية زمنية خوارزميًا؟
• ما هي المنطق الزمني الذي يوازن بين القوة التعبيرية والتحقق الفعال؟

Key theories

المنطق الزمني لتحديد مواصفات البرامج

أظهر بنويلي أن المنطق الزمني يجسد صحة البرامج التفاعلية والمتزامنة من خلال التعبير عن الخصائص على مدى تنفيذها، مما يوفر لغة موحدة لمتطلبات السلامة والحيوية.

التحقق من نموذج المنطق الزمني المتفرع

قدم كلارك وإيمرسون منطق شجرة الحساب وخوارزمية للتحقق منه تلقائيًا مقابل نموذج ذي حالات محدودة، مؤسسين بذلك مجال التحقق من النماذج.

Clinical relevance

تُعد المنطق الزمني لغات المواصفات لأدوات التحقق من النماذج (model checkers) المستخدمة بشكل روتيني للتحقق من تصاميم الأجهزة، وبروتوكولات الاتصال، والبرمجيات المتزامنة، حيث تكشف عن حالات الجمود وانتهاكات السلامة والحيوية قبل النشر؛ وقد حصل مبتكرو هذه التقنية على جائزة تورينج وهي معيار في تصميم الرقائق.

History

اقترح بنويلي المنطق الزمني للاستدلال على البرامج في عام 1977، وطور كلارك وإيمرسون، بالتعاون مع كويل وسيفاكيس بشكل مستقل، التحقق من النماذج حوالي عام 1981. توسع النهج ليشمل الأنظمة الصناعية من خلال الأساليب الرمزية في أوائل التسعينيات، وحصل مبتكروه على جائزة تورينج لهذه التقنية.

Key figures

• Amir Pnueli
• Edmund Clarke
• E. Allen Emerson
• Joseph Sifakis

Seminal works

• clarkeEmerson1981
• huthRyan2004

Frequently asked questions

ما الفرق بين المنطق الزمني الخطي والمنطق الزمني المتفرع؟

تصف المنطق الزمني الخطي مثل LTL خصائص مسار تنفيذ واحد، قد يكون لا نهائيًا. بينما تحدد المنطق الزمني المتفرع مثل CTL كميًا شجرة جميع الاحتمالات المستقبلية الممكنة من كل حالة، مما يسمح بالقول بأن خاصية معينة تتحقق على طول مسار معين أو على طول جميع المسارات. لديهما قوى تعبيرية وخوارزميات تحقق مختلفة.

كيف يستخدم التحقق من النموذج هذه المنطق؟

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