المنطق الزمني الخطي لأتمتة بوشي

الموسوعة الحرة

في التحقق الرسمي (منهجية من علوم الحاسوب)، يتطلب فحص نموذج الحالة المحدودة إيجاد آلة بوشي (BA) مكافئة لصيغة منطقية زمنية خطية (LTL) معينة، أي بحيث تتعرف صيغة LTL وآلة بوشي على نفس لغة ω . توجد خوارزميات تُترجم صيغة LTL إلى آلة بوشي. [ 1 ] [ 2 ] [ 3 ] [ 4 ] عادةً ما تتم هذه العملية على مرحلتين. تُنتج المرحلة الأولى آلة بوشي معممة (GBA) من صيغة LTL. أما المرحلة الثانية، فتُترجم آلة بوشي المعممة إلى آلة بوشي، وهو ما يتضمن عملية بناء سهلة نسبيًا . ولأن LTL أقل تعبيرًا من آلة بوشي، فإن عملية البناء العكسي ليست ممكنة دائمًا.

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

التحويل من LTL إلى GBA

هنا، نُقدّم خوارزميتين للبناء. تُوفّر الأولى بناءً تصريحيًا وسهل الفهم، بينما تُوفّر الثانية بناءً خوارزميًا وفعّالًا. تفترض كلتا الخوارزميتين أن صيغة الإدخال f تُبنى باستخدام مجموعة المتغيرات المنطقية AP وأن f في صيغة النفي العادية . لكل صيغة LTL f' بدون الرمز ¬ كرمز علوي، نُعرّف neg (f') = ¬f' و neg (¬f') = f'. في حالة خاصة f' = true ، نُعرّف neg ( true ) = false .

البناء التصريحي

قبل وصف عملية البناء، نحتاج إلى تقديم بعض التعريفات المساعدة. بالنسبة لصيغة LTL f ، ليكن cl (f) أصغر مجموعة من الصيغ التي تحقق الشروط التالية:

  • صحيح ∈ cl ( f )
  • f ∈ cl ( f )
  • إذا كان f 1 ∈ cl ( f ) فإن neg (f 1 ) ∈ cl ( f )
  • إذا كان X f 1 ∈ cl ( f ) فإن f 1 ∈ cl ( f )
  • إذا كان f 1 ∧ f 2 ∈ cl ( f ) فإن f 1 ,f 2 ∈ cl ( f )
  • إذا كان f 1 ∨ f 2 ∈ cl ( f ) فإن f 1 ,f 2 ∈ cl ( f )
  • إذا كان f 1 U f 2 ∈ cl ( f ) فإن f 1 ,f 2 ∈ cl ( f )
  • إذا كان f 1 R f 2 ∈ cl ( f ) فإن f 1 ,f 2 ∈ cl ( f )

cl (f) هي مجموعة مغلقة للصيغ الفرعية من f تحت النفي . لاحظ أن cl (f) قد تحتوي على صيغ ليست في صيغة النفي العادية. ستُستخدم المجموعات الفرعية من cl (f) كحالات لـ GBA المكافئ. نهدف إلى بناء GBA بحيث إذا كانت حالة ما تُقابل مجموعة فرعية M ⊆ cl (f)، فإن GBA يحتوي على مسار قبول يبدأ من تلك الحالة لكلمة ما إذا وفقط إذا كانت هذه الكلمة تُحقق كل صيغة في M وتُخالف كل صيغة في cl (f) \ M. لهذا السبب، لن نأخذ في الاعتبار أي مجموعة صيغ M غير متسقة بشكل واضح أو مُضمنة في مجموعة شاملة صارمة M' بحيث تكون M وM' متكافئتين وقابلتين للتحقيق. تكون المجموعة M ⊆ cl (f) متسقة بشكل أقصى إذا حققت الشروط التالية:

  • صحيح ∈ م
  • f 1 ∈ M إذا وفقط إذا ¬f 1 ∉ M
  • f 1 ∧ f 2 ∈ M إذا وفقط إذا كان f 1 ∈ M و f 2 ∈ M
  • f 1 ∨ f 2 ∈ M إذا وفقط إذا كان f 1 ∈ M أو f 2 ∈ M

لنفترض أن cs (f) هي مجموعة المجموعات الجزئية المتسقة بشكل أقصى من cl (f). سنستخدم cs (f) فقط كحالات لـ GBA.

شركة جي بي إيه للإنشاءات

يُعرَّف GBA المكافئ للدالة f على النحو التالي: A = ({init}∪ cs ( f ), 2 AP , Δ,{init}, F ), حيث

  • Δ = Δ 1 ∪ Δ 2
    • (M, a, M') ∈ Δ 1 إذا وفقط إذا ( M' ∩ AP ) ⊆ a ⊆ {p ∈ AP | ¬p ∉ M' } و:
      • X f 1 ∈ M إذا وفقط إذا f 1 ∈ M';
      • f 1 U f 2 ∈ M iff f 2 ∈ M or ( f 1 ∈ M and f 1 U f 2 ∈ M' );
      • f 1 R f 2 ∈ M إذا وفقط إذا كان f 1 ∧ f 2 ∈ M أو ( f 2 ∈ M و f 1 R f 2 ∈ M' )
    • Δ 2 = { (init, a, M') | ( M' ∩ AP ) ⊆ a ⊆ {p ∈ AP | ¬p ∉ M' } و f ∈ M' }
  • لكل f 1 U f 2 ∈ cl ( f )، {M ∈ cs ( f ) | f 2 ∈ M أو ¬(f 1 U f 2 ) ∈ M } ∈ F

تضمن الشروط الثلاثة في تعريف Δ1 أن أي سلسلة من A لا تنتهك دلالات المؤثرات الزمنية. لاحظ أن F هي مجموعة من مجموعات الحالات. تُعرَّف المجموعات في F لالتقاط خاصية للمؤثر U لا يمكن التحقق منها بمقارنة حالتين متتاليتين في سلسلة، أي إذا كانت f1 ∪ f2 صحيحة في حالة ما، فإن f2 ستكون صحيحة في حالة لاحقة.

إثبات صحة البناء المذكور أعلاه

ليكن w = a₁ , a₂ , ... كلمة ω على الأبجدية 2 AP . ليكن wᵢ = aᵢ , aᵢ₊₁ , ... . ليكن M w = { f' ∈ cl (f) | w⊨{\displaystyle \vDash } {f'}، والتي نسميها المجموعة المُرضية . نظرًا لتعريف cs (f)، فإن Mw ∈ cs  ( f ). يمكننا تعريف متتالية ρw = init, Mw1 , Mw2 , ... . نظرًا لتعريف A ، إذا كان w ⊨{\displaystyle \vDash }إذا كان f، فإن ρ w يجب أن يكون تشغيلًا مقبولًا لـ A على w .

على العكس من ذلك، لنفترض أن A تقبل w . ولتكن ρ = init, M 1 , M 2 ,... سلسلة من A على w . تُكمل النظرية التالية بقية برهان الصحة.

النظرية 1: لكل i > 0، M w i = M i .

البرهان: يتم البرهان بالاستقراء على بنية f' ∈ cl (f).

  • الحالات الأساسية:
    • f' = صحيح . بحسب التعريفات، f' ∈ M w i و f' ∈ M i .
    • f' = p. بحسب تعريف A ، فإن p ∈ M i إذا وفقط إذا كان p ∈ a i إذا وفقط إذا كان p ∈ M w i .
  • خطوات الاستهلال:
    • f' = f 1 ∧ f 2. بناءً على تعريف المجموعات المتسقة، فإن f 1 ∧ f 2 ∈ M i إذا وفقط إذا كان f 1 ∈ M i و f 2 ∈ M i . بناءً على فرضية الاستقراء، فإن f 1 ∈ M w i و f 2 ∈ M w i . بناءً على تعريف المجموعة المُرضية، فإن f 1 ∧ f 2 ∈ M w i .
    • f' = ¬f 1 , f' = f 1 ∨ f 2 , f' = X f 1 أو f' = f 1 R f 2 . البراهين مشابهة جدًا للبرهان الأخير.
    • f' = f 1 U f 2 . ينقسم برهان المساواة إلى برهانين استلزاميين.
      • إذا كان f 1 U f 2 ∈ M i ، فإن f 1 U f 2 ∈ M w i . وبحسب تعريف انتقالات A ، يمكننا الحصول على الحالتين التاليتين.
        • f 2 ∈ M i . بحسب فرضية الاستقراء، f 2 ∈ M w i . إذن، f 1 U f 2 ∈ M w i .
        • f₁ ∈ Mᵢ و f₁ ∪ f₂ ∈ Mᵢ₊₁ . وبسبب شرط القبول لـ A ، يوجد على الأقل دليل واحد j ≥ i بحيث f₂ ∈ Mⱼ . ليكن j' أصغر هذه الأدلة. نبرهن النتيجة بالاستقراء على k = {j', j' -1, ..., i₊₁, i}. إذا كان k = j'، فإن f₂ ∈ Mⱼ ، ونطبق نفس الحجة كما في حالة f₂ ∈ Mᵢ . إذا كان i ≤ k < j'، فإن f₂ ∉ Mⱼ ، وبالتالي f₁ ∈ Mⱼ و f₁ ∪ f₂ ∈ Mⱼ₊₁ . وبسبب فرضية الاستقراء على f' ، لدينا f₁ ∈ Mⱼ₋ₖ . بسبب فرضية الاستقراء على المؤشرات، لدينا أيضًا f 1 U f 2 ∈ M w k+1 . وبسبب تعريف دلالات LTL، فإن f 1 U f 2 ∈ M w k .
      • إذا كان f 1 U f 2 ∈ M w i ، فإن f 1 U f 2 ∈ M i . وبسبب دلالات LTL، يمكننا الحصول على الحالتين التاليتين.
        • f 2 ∈ M w i . بحسب فرضية الاستقراء، f 2 ∈ Mi . إذن، f 1 U f 2 ∈ Mi .
        • f 1 ∈ M w i و f 1 U f 2 ∈ M w i+1 . بسبب دلالات LTL، يوجد على الأقل فهرس واحد j ≥ i بحيث f 2 ∈ M j . ليكن j' أصغر هذه الفهارس. تابع الآن كما في برهان الاستلزام العكسي.

بناءً على النظرية المذكورة أعلاه، فإن M w 1 = M 1. وبناءً على تعريف انتقالات A ، فإن f ∈ M 1. وبالتالي، فإن f ∈ M w 1 و w⊨{\displaystyle \vDash }و.

خوارزمية جيرث وآخرون

يعود الخوارزمية التالية إلى جيرث، وبيليد، وفاردي ، وولبر . [ 3 ] كما تتوفر آلية بناء موثقة لهذه الخوارزمية من قِبل شيمبف، وميرز، وسماوس. [ 5 ] تُنشئ الخوارزمية السابقة عددًا هائلاً من الحالات مُسبقًا، وقد يكون الوصول إلى العديد من هذه الحالات مستحيلاً. تتجنب الخوارزمية التالية هذا الإنشاء المُسبق، وتتألف من خطوتين. في الخطوة الأولى، تُنشئ الخوارزمية تدريجيًا رسمًا بيانيًا مُوجهًا . في الخطوة الثانية، تُنشئ الخوارزمية آلة بوشي مُعممة مُصنفة (LGBA) من خلال تعريف عُقد الرسم البياني كحالات، والحواف المُوجهة كانتقالات. تأخذ هذه الخوارزمية إمكانية الوصول في الحسبان، وقد تُنتج آلة أصغر حجمًا، لكن تعقيد الحالة الأسوأ يبقى كما هو.

تُسمى عُقد الرسم البياني بمجموعات من الصيغ، ويتم الحصول عليها بتحليل الصيغ وفقًا لبنيتها المنطقية، وتوسيع عوامل الزمن لفصل ما يجب أن يكون صحيحًا فورًا عما يجب أن يكون صحيحًا بدءًا من الحالة التالية. على سبيل المثال، لنفترض أن صيغة LTL f₁ ∪ f₂ تظهر في تسمية إحدى العُقد. f₁ ∪ f₂ تُكافئ f₂ ∨ (f₁ ∧ X ( f₁ ∪ f₂ ) ). يشير التوسيع المكافئ إلى أن f₁ ∪ f₂ صحيحة في إحدى الحالتين التاليتين .

  1. يتحقق الشرط f 1 في الوقت الحالي، ويتحقق الشرط (f 1 U f 2 ) في الخطوة الزمنية التالية، أو
  2. f 2 ثابتة عند الخطوة الزمنية الحالية

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

نحتاج أيضًا إلى مراعاة المؤثر الزمني R الذي قد يتسبب في هذا الانقسام. f 1 R f 2 مكافئ لـ ( f 1 ∧ f 2 ) ∨ ( f 2 ∧ X (f 1 R f 2 ) )، ويشير هذا التوسع المكافئ إلى أن f 1 R f 2 صحيح في إحدى الحالتين التاليتين.

  1. يتحقق الشرط f 2 في الوقت الحالي، ويتحقق الشرط (f 1 R f 2 ) في الخطوة الزمنية التالية، أو
  2. يتحقق الشرط ( f 1 ∧ f 2 ) عند الخطوة الزمنية الحالية.

لتجنب العديد من الحالات في الخوارزمية التالية، دعونا نحدد الدوال curr1 و next1 و curr2 التي تشفر المكافئات المذكورة أعلاه في الجدول التالي.

وcurr1(f)next1(f)curr2(f)
f 1 U f 2{f 1 }{ f 1 U f 2 }{f 2 }
f 1 R f 2{f 2 }{ f 1 R f 2 }{f 1 ,f 2 }
f 1 ∨ f 2{f 2 }∅{f 1 }

لقد أضفنا أيضًا حالة الفصل في الجدول أعلاه لأنها تتسبب أيضًا في انقسام الحالة في الآلة.

فيما يلي خطوتا الخوارزمية.

الخطوة 1. إنشاء_الرسم_البياني

في المربع التالي، نعرض الجزء الأول من الخوارزمية التي تُنشئ رسمًا بيانيًا موجهًا. الدالة `create_graph` هي دالة الإدخال، وتتوقع صيغة الإدخال `f` في صيغة النفي العادية . تستدعي هذه الدالة الدالة التكرارية `expand` التي تُنشئ الرسم البياني عن طريق ملء المتغيرات العامة `Nodes` و` Incoming` و` Now` و` Next` . تخزن المجموعة `Nodes` مجموعة العقد في الرسم البياني. تربط الدالة `Incoming` كل عقدة من `Nodes` بمجموعة فرعية من `Nodes` ∪ {init}، والتي تُحدد مجموعة الحواف الواردة. قد تحتوي `Incoming` الخاصة بعقدة ما أيضًا على رمز خاص `init` يُستخدم في بناء الأوتوماتون النهائي لتحديد مجموعة الحالات الأولية. تربط الدالتان `Now` و` Next` كل عقدة من `Nodes` بمجموعة من صيغ LTL. بالنسبة للعقدة `q`، تُشير ` Now (q)` إلى مجموعة الصيغ التي يجب أن تُحققها بقية كلمة الإدخال إذا كان الأوتوماتون حاليًا عند العقدة (الحالة) `q`. يشير Next (q) إلى مجموعة الصيغ التي يجب أن تفي بها بقية كلمة الإدخال إذا كان الجهاز الآلي موجودًا حاليًا في العقدة (الحالة) التالية بعد q.

typedefs LTL : صيغ LTL LTLSet : مجموعات من صيغ LTL NodeSet : مجموعات من عقد الرسم البياني ∪ {init} المتغير العام Nodes : مجموعة عقد الرسم البياني := ∅ الوارد : Nodes → NodeSet := ∅ الحالي : Nodes → LTLSet := ∅ التالي : Nodes → LTLSet := ∅ دالة إنشاء_الرسم_البياني ( LTL f) { expand({f}, ∅, ∅, {init}) return ( Nodes , Now , Incoming ) }
دالة توسيع ( LTLSet curr، LTLSet old، LTLSet next، NodeSet incoming){ 1: إذا كان curr = ∅، فإن 2: إذا كان ∃q ∈ Nodes : Next (q)=next ∧ Now (q)=old، فإن 3: Incoming (q) := Incoming (q) ∪ incoming 4: وإلا 5: q := new_node () 6: العقد := العقد ∪ {q} 7: الوارد (q) := الوارد 8: الآن (q) := قديم 9: التالي (q) := التالي 10: توسيع( التالي (q)، ∅، ∅، {q}) 11: وإلا 12: f ∈ curr 13: curr := curr\{f} 14: قديم := قديم ∪ {f} 15: طابق f مع 16: | صحيح ، خطأ ، p، أو ¬p، حيث p ∈ AP → 17: إذا كانت f = خطأ ∨ neg (f) ∈ old، فإن 18: تخطى 19: وإلا 20: توسيع(الحالي، القديم، التالي، الوارد) 21: | f 1 ∧ f 2 → 22: توسيع(الحالي ∪ ({f 1 ,f 2 }\old), القديم، التالي، الوارد) 23: | X g → 24: توسيع(الحالي، القديم، التالي ∪ {g}، الوارد) 25: | f 1 ∨ f 2 ، f 1 U f 2 ، أو f 1 R f 2 → 26: توسيع(الحالي ∪ ( الحالي1 (f)\old), القديم، التالي ∪ التالي1 (f), الوارد) 27: توسيع(الحالي ∪ ( الحالي2 (f)\old), القديم، التالي، الوارد) 28: إرجاع }

يُرقّم كود دالة التوسيع بأرقام الأسطر لتسهيل الرجوع إليه. يهدف كل استدعاء لهذه الدالة إلى إضافة عقدة وعقدها اللاحقة إلى الرسم البياني. وتصف معلمات الاستدعاء عقدة جديدة محتملة.

  • يحتوي المعامل الأول curr على مجموعة الصيغ التي لم يتم توسيعها بعد.
  • يحتوي المعامل الثاني القديم على مجموعة الصيغ التي تم توسيعها بالفعل.
  • المعامل الثالث التالي هو مجموعة الصيغة التي سيتم من خلالها إنشاء العقدة اللاحقة.
  • يُحدد المعامل الرابع الوارد مجموعة الحواف الواردة عند إضافة العقدة إلى الرسم البياني.

في السطر 1، يتحقق شرط if مما إذا كانت curr تحتوي على أي صيغة قابلة للتوسيع. إذا كانت curr فارغة، يتحقق شرط if في السطر 2 مما إذا كانت هناك حالة q' موجودة بالفعل بنفس مجموعة الصيغ الموسعة. إذا كان الأمر كذلك، فلا نضيف عقدة زائدة، ولكن نضيف المعامل incoming في Incoming (q') في السطر 3. وإلا، نضيف عقدة جديدة q باستخدام المعاملات في الأسطر من 5 إلى 9، ونبدأ بتوسيع عقدة لاحقة لـ q باستخدام next (q) كمجموعة صيغها غير الموسعة في السطر 10.

في حال لم يكن المتغير curr فارغًا، فسنحصل على المزيد من الصيغ لتوسيعها والتحكم في الانتقالات من السطر 1 إلى السطر 12. في الأسطر من 12 إلى 14، يتم اختيار الصيغة f من المتغير curr ونقلها إلى المتغير old . وبناءً على بنية الصيغة f، يتم تنفيذ باقي الدالة.

  • إذا كانت f قيمة حرفية، فإن التوسيع يستمر في السطر 20، ولكن إذا كان old يحتوي بالفعل على neg (f) أو f= false ، فإن old يحتوي على صيغة غير متسقة ونتجاهل هذه العقدة بعدم إجراء أي تكرار في السطر 18.
  • إذا كان f = f 1 ∧ f 2 ، فسيتم إضافة f 1 و f 2 إلى curr وسيتم إجراء استدعاء متكرر لمزيد من التوسع في السطر 22.
  • إذا كان f = X f 1 ، فسيتم إضافة f 1 إلى التالي لخليفة العقدة الحالية قيد النظر في السطر 24.
  • إذا كان f = f 1 ∨ f 2 ، أو f = f 1 U f 2 ، أو f = f 1 R f 2 ، فسيتم تقسيم العقدة الحالية إلى عقدتين، وسيتم إجراء استدعاء متكرر لكل عقدة.

بالنسبة للاستدعاءات المتكررة، يتم تعديل curr و next باستخدام الدوال curr1 و next1 و curr2 التي تم تعريفها في الجدول أعلاه.

الخطوة الثانية: بناء LGBA

ليكن ( العقد ، الآن ، الوارد ) = إنشاء_رسم_بياني(f). الرسم البياني المكافئ لـ f هو A = ( العقد ، 2 AP ، L ، Δ، Q 0 ، F )، حيث

  • L = { (q,a) | q ∈ Nodes and ( Now (q) ∩ AP ) ⊆ a ⊆ {p ∈ AP | ¬p ∉ Now (q) } }
  • Δ = {(q,q')| q,q' ∈ Nodes and q ∈ Incoming(q') }
  • Q 0 = { q ∈ Nodes | init ∈ Incoming (q) }
  • لكل صيغة فرعية g = g 1 U g 2 ، ليكن F g = { q ∈ Nodes | g 2 ∈ Now (q) or g ∉ Now (q) }، عندئذٍ F = { F g | g ∈ cl ( f ) }

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

أدوات

  • مترجم LTL2TGBA الخاص بـ Spot - مترجم LTL2TGBA مُضمّن في مكتبة C++ SPOT. مترجم متاح عبر الإنترنت.
  • LTL2BA - مترجم سريع من LTL إلى BA عبر الأتمتة المتناوبة. مترجم متاح عبر الإنترنت.
  • LTL3BA - تحسين محدّث لـ LTL2BA.
  • مترجم LTL2NBA من Owl - مترجم LTL2NBA مُضمّن في مكتبة جافا Owl. يتوفر مترجم عبر الإنترنت.

مراجع

  1. ↑ MY Vardi و P. Wolper، التفكير في الحسابات اللانهائية، المعلومات والحوسبة ، 115 (1994)، 1-37.
  2. ^ Y. Kesten، Z. Manna، H. McGuire، A. Pnueli ، خوارزمية قرار للمنطق الزمني المقترح الكامل، CAV'93، Elounda، اليونان، LNCS 697، Springer – Verlag، 97-109.
  3. 1 2 R. Gerth, D. Peled, MY Vardi and P. Wolper, “Simple On-The-Fly Automatic Verification of Linear Temporal Logic,” Proc. IFIP/WG6.1 Symp. Protocol Specification, Testing, and Verification (PSTV95), pp. 3-18, Warsaw, Poland, Chapman & Hall, June 1995.
  4. ↑ P. Gastin and D. Oddoux, Fast LTL to Büchi automata translation, Thirteenth Conference on Computer Aided Verification (CAV ′01), number 2102 in LNCS, Springer-Verlag (2001), pp. 53–65.
  5. ↑ أ. شيمبف، س. ميرز، و ج.-ج. سماوس، "بناء أوتوماتا بوشي للتحقق من نموذج LTL تم التحقق منه في Isabelle/HOL"، وقائع المؤتمر الدولي حول إثبات النظريات في منطق الرتبة العليا (TPHOLs 2009)، ص 424-439، ميونيخ، ألمانيا، سبرينغر، أغسطس 2009.