المنطق الزمني الخطي

في المنطق ، يُعرف المنطق الزمني الخطي ( LTL ) بأنه منطق زمني ^مشروط^،^حيث تشير المشروطات إلى الزمن. في LTL، يمكن ترميز صيغ تتعلق بمستقبل المسارات ، على ^{سبيل المثال،}^{أن شرطًا ما سيصبح صحيحًا في النهاية،}^أو أن شرطًا ما سيظل صحيحًا حتى يصبح واقع آخر صحيحًا، وهكذا. وهو جزء من منطق CTL* الأكثر تعقيدًا ، والذي يسمح أيضًا بتفرع الزمن والمُكمِّمات . يُطلق على LTL أحيانًا اسم المنطق الزمني الافتراضي ( PTL ). ^[³^] من حيث القدرة التعبيرية ، يُعد LTL جزءًا من منطق الرتبة الأولى . ^[⁴^]^[⁵^]

تم اقتراح LTL لأول مرة للتحقق الرسمي من برامج الكمبيوتر بواسطة أمير بنويلي في عام 1977. ^{[ 6 ]}

بناء الجملة

تُبنى لغة LTL من مجموعة المتغيرات الافتراضية AP ، والمعاملات المنطقية ¬ و ∨، والمعاملات الزمنية X (تستخدم بعض المراجع O أو N ) و U. وبشكل رسمي، تُعرَّف مجموعة صيغ LTL على AP استقرائيًا كما يلي:

إذا كان $p \in AP$ فإن p عبارة عن صيغة LTL؛
إذا كانت $ψ$ و $φ$ عبارة عن صيغ LTL، فإن $\neg ψ و φ \lor ψ و X ψ$ و $φ U ψ$ هي صيغ LTL. ^{[ 7 ]}

يُقرأ الرمز X على أنه " التالي" ويُقرأ الرمز U على أنه " حتى". بالإضافة إلى هذه المعاملات الأساسية، توجد معاملات منطقية وزمنية إضافية مُعرَّفة بدلالة المعاملات الأساسية، وذلك لكتابة صيغ LTL بإيجاز. المعاملات المنطقية الإضافية هي: ∧، →، ↔، صحيح ، وخطأ . وفيما يلي المعاملات الزمنية الإضافية.

حرف G يرمز إلى "دائماً" ( وعلى نطاق عالمي)
F أخيرًا
R للإفراج
W لـ w ضعيف حتى
حرف M للإصدار القوي

القواعد النحوية الخالية من السياق لـ LTL هي كما يلي: $φ ::= ⊤ | ⊥ | ع | (\neg φ) | (φ \land φ) | (φ \lor φ) | (φ \to φ) | (س φ) | (ز φ) | (ف φ) | (φ يو φ) | (φ ث φ) | (φ ر φ) | (φ م φ)$

علم الدلالة

يمكن تحقيق صيغة LTL بواسطة سلسلة لانهائية من قيم الصواب لمتغيرات في AP . يمكن اعتبار هذه السلاسل كلمةً على مسار في بنية كريپكي ( كلمة ω على الأبجدية 2 ^AP ). لنفترض أن w = _a₀ , _a₁ , a₂ _, ... هي كلمة ω. ولنفترض أن _{w(i) = aᵢ. ولنفترض أن wᵢ = aᵢ, aᵢ₊₁} , ... ، وهي لاحقة لـ ^w. رسميًا ، تُعرَّف علاقة _{الإرضاء} ⊨ بين _كلمة وصيغة LTL كما يلي _:

w ⊨ p إذا كان p ∈ w (0)
w ⊨ ¬ ψ إذا w ⊭ ψ
ث ⊨ φ ∨ ψ إذا ث ⊨ φ أو ث ⊨ ψ
$w ⊨ X ψ$ إذا كان w ¹ ⊨ ψ (في الخطوة الزمنية t التالية ، يجب أن تكون ψ صحيحة)
$w ⊨ φ U ψ$ إذا كان هناك i ≥ 0 بحيث w ⁱ ⊨ ψ ولكل 0 ≤ k < i، w ^k ⊨ $φ$ ( $يجب أن تظل φ$ صحيحة حتى تصبح ψ صحيحة)

نقول إن كلمة ω- w تحقق صيغة LTL ψ عندما w ⊨ ψ . لغة ω- L ( ψ ) المعرفة بواسطة ψ هي { w | w ⊨ ψ }، وهي مجموعة كلمات ω- التي تحقق ψ . تكون الصيغة ψ قابلة للتحقيق إذا وُجدت كلمة ω- w بحيث w ⊨ ψ . تكون الصيغة ψ صحيحة إذا كان لكل كلمة ω- w على الأبجدية 2 ^AP ، لدينا w ⊨ ψ .

يتم تعريف عوامل التشغيل المنطقية الإضافية على النحو التالي:

φ ∧ ψ ≡ ¬(¬ φ ∨ ¬ ψ )
φ → ψ ≡ ¬ φ ∨ ψ
φ ↔ ψ ≡ ( φ → ψ ) ∧ ( ψ → φ )
صحيح ≡ p ∨ ¬ p ، حيث p ∈ AP
خطأ ≡ ¬ صحيح

يتم تعريف عوامل التشغيل الزمنية الإضافية R و F و G على النحو التالي:

ψ R φ ≡ ¬(¬ ψ U ¬ φ ) ( تبقى φ صحيحة حتى تصبح ψ صحيحة، بما في ذلك تلك اللحظة. إذا لم تصبح ψ صحيحة أبدًا، فيجب أن تبقى φ صحيحة إلى الأبد. ψ r تُحرر φ .)
$F ψ \equiv true U ψ$ (في النهاية تصبح ψ صحيحة)
G ψ ≡ false R ψ ≡ ¬ F ¬ ψ ( ψ تظل صحيحة دائمًا)

إطلاق ضعيف حتى إطلاق قوي

يُعرّف بعض المؤلفين أيضًا عاملًا ثنائيًا ضعيفًا يُسمى "حتى" ، ويرمز له بـ W ، وله دلالات مشابهة لدلالات عامل "حتى"، ولكن ليس من الضروري تحقق شرط التوقف (كما هو الحال في "الإفراج"). ^{[ 8 ]} وهو مفيد أحيانًا، إذ يمكن تعريف كل من U و R بدلالة "حتى" الضعيف.

$ψ W φ \equiv (ψ U φ) \lor G ψ \equiv ψ U (φ \lor G ψ) \equiv φ R (φ \lor ψ)$
$ψ U φ \equiv F φ \land (ψ W φ)$
$ψ R φ \equiv φ W (φ \land ψ)$

يُعدّ عامل التحرير الثنائي القوي ، الذي يُرمز له بـ M ، نظيرًا لعامل التحرير الضعيف "حتى". وهو مُعرّف بشكل مشابه لعامل "حتى"، بحيث يجب أن يتحقق شرط التحرير عند نقطة معينة. ولذلك، فهو أقوى من عامل التحرير.

$ψ M φ \equiv \neg(\neg ψ W \neg φ) \equiv (ψ R φ) \land F ψ \equiv ψ R (φ \land F ψ) \equiv φ U (ψ \land φ)$

يتم عرض دلالات عوامل التشغيل الزمنية بشكل تصويري كما يلي.

نصي	رمزي	توضيح
المعاملات الأحادية :
X φ	$\bigcirc \varphi$	ne X t: يجب أن يتحقق الشرط φ في الحالة التالية.
F φ	$\Diamond \varphi$	وأخيرًا : يتحقق الشرط φ عند حالة معينة على المسار.
G φ	$\Box \varphi$	عالميًا : يجب أن تبقى قيمة φ ثابتة على المسار بأكمله.
المعاملات الثنائية :
ψ U φ	$\psi \;{\mathcal {U}}\,\varphi$	حتى : يجب أن تبقى ψ صحيحة على الأقل حتى تصبح φ صحيحة، والتي يجب أن تبقى صحيحة في الوضع الحالي أو في وضع مستقبلي.
ψ R φ	$\psi \;{\mathcal {R}}\,\varphi$	R release: يجب أن تكون φ صحيحة حتى النقطة التي تصبح فيها ψ صحيحة لأول مرة، بما في ذلك تلك النقطة؛ إذا لم تصبح ψ صحيحة أبدًا، فيجب أن تظل φ صحيحة إلى الأبد.
ψ W φ	$\psi \;{\mathcal {W}}\,\varphi$	ضعيف حتى: يجب أن تظل ψ صحيحة على الأقل حتى φ ؛ إذا لم تصبح φ صحيحة أبدًا، فيجب أن تظل ψ صحيحة إلى الأبد.
ψ M φ	$\psi \;{\mathcal {M}}\,\varphi$	إطلاق قوي: يجب أن تكون φ صحيحة حتى النقطة التي تصبح فيها ψ صحيحة لأول مرة، والتي يجب أن تكون صحيحة في الوضع الحالي أو في وضع مستقبلي.

المكافئات

لنفترض أن φ و ψ و ρ هي صيغ LTL. تُدرج الجداول التالية بعض المكافئات المفيدة التي تُوسّع المكافئات القياسية بين عوامل التشغيل المنطقية المعتادة.

التوزيعية
X (φ ∨ ψ) ≡ ( X φ) ∨ ( X ψ)	X (φ ∧ ψ) ≡ ( X φ) ∧ ( X ψ)	X (φ U ψ)≡ ( X φ) U ( X ψ)
و (φ ∨ ψ) ≡ ( F φ) ∨ ( F ψ)	جي (φ ∧ ψ) ≡ ( جي φ) ∧ ( جي ψ)
ρ U (φ ∨ ψ) ≡ (ρ U φ) ∨ (ρ U ψ)	(φ ∧ ψ) U ρ ≡ (φ U ρ) ∧ (ψ U ρ)

انتشار النفي
X هو ذاتي الازدواجية	F و G ثنائيان	U و R متناظران	W و M متناظران
¬ X φ ≡ X ¬φ	¬ F φ ≡ G ¬φ	¬ (φ U ψ) ≡ (¬φ R ¬ψ)	¬ (φ ث ψ) ≡ (¬φ م ¬ψ)
	¬ G φ ≡ F ¬φ	¬ (φ R ψ) ≡ (¬φ U ¬ψ)	¬ (φ م ψ) ≡ (¬φ ث ¬ψ)

خصائص زمنية خاصة
F φ ≡ F F φ	G φ ≡ G G φ	φ U ψ ≡ φ U (φ U ψ)
φ U ψ ≡ ψ ∨ ( φ ∧ X (φ U ψ))	φ W ψ ≡ ψ ∨ ( φ ∧ X (φ W ψ)) )	φ R ψ ≡ ψ ∧ (φ ∨ X (φ R ψ)) )
G φ ≡ φ ∧ X ( G φ)	F φ ≡ φ ∨ X ( F φ)

الصيغة الطبيعية للنفي

يمكن تحويل جميع صيغ LTL إلى صيغة النفي العادية ، حيث

تظهر جميع أدوات النفي فقط أمام القضايا الأساسية،
لا يمكن أن تظهر إلا عوامل التشغيل المنطقية: صحيح ، خطأ ، ∧، و∨، و
لا يمكن أن تظهر إلا العوامل الزمنية X و U و R.

باستخدام المكافئات المذكورة أعلاه لنشر النفي، يمكن اشتقاق الصيغة المعيارية. تسمح هذه الصيغة المعيارية بظهور R و true و false و∧ في الصيغة، وهي ليست عوامل أساسية في لغة LTL. تجدر الإشارة إلى أن التحويل إلى الصيغة المعيارية للنفي لا يزيد من طول الصيغة. تُعد هذه الصيغة المعيارية مفيدة في الترجمة من صيغة LTL إلى أوتوماتون بوشي .

العلاقات مع المنطق الأخرى

يمكن إثبات أن LTL مكافئ لمنطق الرتبة الأولى الأحادي للترتيب ، FO[<] - وهي نتيجة تُعرف باسم نظرية كامب - ^{[ 9 ]} أو مكافئ للغات الخالية من النجوم . ^{[ 10 ]}

يُعد كل من منطق شجرة الحساب (CTL) والمنطق الزمني الخطي (LTL) مجموعة فرعية من CTL* ، لكنهما غير قابلين للمقارنة. على سبيل المثال،

لا يمكن لأي صيغة في لغة CTL أن تحدد اللغة التي تحددها صيغة LTL F ( G p ).
لا يمكن لأي صيغة في لغة LTL أن تحدد اللغة التي تحددها صيغ CTL AG ( p → ( EX q ∧ EX ¬q) ) أو AG ( EF (p)).

المشاكل الحسابية

يُعدّ التحقق من النموذج وإمكانية إرضائه وفقًا لصيغة LTL من المسائل الكاملة في فئة PSPACE . أما توليف LTL ومسألة التحقق من الألعاب في ظل شرط فوز LTL فهي مسائل كاملة في فئة 2EXPTIME . ^{[ 11 ]}

التطبيقات

التحقق من صحة نموذج المنطق الزمني الخطي القائم على نظرية الأوتوماتا: تُستخدم صيغ LTL عادةً للتعبير عن القيود أو المواصفات أو العمليات التي يجب أن يتبعها النظام. يهدف مجال التحقق من النماذج إلى التحقق رسميًا مما إذا كان النظام يفي بمواصفات معينة. في حالة التحقق من النماذج باستخدام نظرية الأوتوماتا، يُعبَّر عن كل من النظام محل الاهتمام والمواصفات كآلات حالة محدودة منفصلة ، أو أوتوماتا، ثم تتم مقارنتهما لتقييم ما إذا كان النظام يضمن امتلاك الخاصية المحددة. في علوم الحاسوب، يُستخدم هذا النوع من التحقق من النماذج غالبًا للتحقق من صحة بنية الخوارزمية.

للتحقق من مواصفات منطق الزمن الخطي (LTL) في عمليات تشغيل النظام اللانهائية، تتمثل إحدى التقنيات الشائعة في الحصول على آلة بوشي مكافئة للنموذج (تقبل كلمة ω تحديدًا إذا كانت هي النموذج) وأخرى مكافئة لنفي الخاصية (تقبل كلمة ω تحديدًا إذا كانت تحقق الخاصية المنفية) (انظر: منطق الزمن الخطي إلى آلة بوشي ). في هذه الحالة، إذا كان هناك تداخل في مجموعة كلمات ω التي تقبلها الآلتان، فهذا يعني أن النموذج يقبل بعض السلوكيات التي تنتهك الخاصية المطلوبة. أما إذا لم يكن هناك تداخل، فلا توجد سلوكيات منتهكة للخاصية يقبلها النموذج. رسميًا، يكون تقاطع آلتَي بوشي غير الحتميتين فارغًا إذا وفقط إذا كان النموذج يحقق الخاصية المحددة. ^{[ 12 ]}

التعبير عن الخصائص المهمة في التحقق الرسمي: هناك نوعان رئيسيان من الخصائص التي يمكن التعبير عنها باستخدام المنطق الزمني الخطي: خصائص الأمان ، التي تنص عادةً على أن شيئًا سيئًا لا يحدث أبدًا ( G ∈ ϕ )، وخصائص الحيوية ، التي تنص على أن شيئًا جيدًا يستمر في الحدوث ( GF ψ أو G ( ϕ → F ψ )). ^{[ 13 ]} على سبيل المثال، قد تتطلب خاصية الأمان ألا يقود الروبوت الجوال المستقل أبدًا من فوق جرف، أو ألا يسمح برنامج ما بتسجيل دخول ناجح بكلمة مرور خاطئة. وقد تتطلب خاصية الحيوية أن يستمر الروبوت الجوال دائمًا في جمع عينات البيانات، أو أن يرسل برنامج ما بيانات القياس عن بُعد بشكل متكرر.

بشكل عام، خصائص الأمان هي تلك التي يكون لكل مثال مضاد لها بادئة محدودة، بحيث يظل مثالًا مضادًا مهما امتد إلى مسار لانهائي. أما بالنسبة لخصائص الحيوية، فيمكن تمديد كل مسار محدود إلى مسار لانهائي يحقق الصيغة.

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

الإضافات

يوسع المنطق الزمني الخطي البارامتري منطق LTL بالمتغيرات على نمط حتى. ^{[ 14 ]}

انظر أيضاً

مراجع

↑ المنطق في علوم الحاسوب: نمذجة الأنظمة والاستدلال حولها : صفحة 175
↑ "المنطق الزمني الخطي" . مؤرشف من الأصل بتاريخ 30-04-2017 . تم الاطلاع عليه بتاريخ 19-03-2012 .
↑ دوف م. غاباي ؛ أ. كوروتش؛ ف. وولتر؛ م. زاخارياشيف (2003). منطق الوسائط متعدد الأبعاد: النظرية والتطبيقات . إلسيفير. ص 46. ISBN 978-0-444-50826-3.
↑ ديكرت، فولكر. "لغات قابلة للتعريف من الدرجة الأولى" (ملف PDF) . جامعة شتوتغارت.
↑ كامب، هانز (1968). منطق الزمن ونظرية الترتيب الخطي (دكتوراه). جامعة كاليفورنيا، لوس أنجلوس.
↑ أمير بنويلي ، المنطق الزمني للبرامج. وقائع الندوة السنوية الثامنة عشرة حول أسس علوم الحاسوب (FOCS) ، 1977، 46-57. doi : 10.1109/SFCS.1977.32
↑ القسم 5.1 من كتاب كريستيل باير وجوست بيتر كاتوين ، مبادئ التحقق من النماذج ، منشورات معهد ماساتشوستس للتكنولوجيا . مؤرشف من الأصل بتاريخ 4 ديسمبر 2010. تم الاطلاع عليه بتاريخ 17 مايو 2011 .
↑ القسم 5.1.5 "الضعف حتى، والتحرير، والشكل الطبيعي الإيجابي" من مبادئ التحقق من النموذج.
↑ أبرامسكي، سامسون ؛ جافويل، سيريل؛ كيرشنر، كلود؛ سبيراكيس، بول (30 يونيو 2010). الأوتوماتا واللغات والبرمجة: الندوة الدولية السابعة والثلاثون، ICALP ... - كتب جوجل . سبرينغر. ISBN 9783642141614تم الاطلاع عليه بتاريخ 30 يوليو 2014 .
↑ موشيه ي. فاردي (2008). "من الكنيسة وما قبلها إلى PSL ". في أورنا غرومبرغ ؛ هيلموت فيث (محرران). 25 عامًا من التحقق من النماذج: التاريخ والإنجازات والآفاق . سبرينغر. ISBN 978-3-540-69849-4.نسخة أولية
↑ أ. بنويلي و ر. روزنر. "حول توليف وحدة تفاعلية". في وقائع الندوة السادسة عشرة لجمعية آلات الحوسبة SIGPLAN-SIGACT حول مبادئ لغات البرمجة (POPL '89). جمعية آلات الحوسبة، نيويورك، نيويورك، الولايات المتحدة الأمريكية، 179-190. https://doi.org/10.1145/75277.75293
↑ موشيه ي. فاردي. مدخلٌ قائم على نظرية الأوتوماتا إلى المنطق الزمني الخطي. وقائع ورشة عمل بانف الثامنة للرتب العليا (بانف 94). سلسلة محاضرات في علوم الحاسوب ، المجلد 1043، الصفحات 238-266، سبرينغر-فيرلاغ، 1996. ISBN 3-540-60915-6.
↑ بوين ألبيرن، فريد ب. شنايدر ، تعريف الحيوية ، رسائل معالجة المعلومات ، المجلد 21، العدد 4، 1985، الصفحات 181-185، الرقم الدولي الموحد للدوريات 0020-0190، https://doi.org/10.1016/0020-0190(85)90056-0
↑ تشاكرابورتي، سويموديب؛ كاتوين، جوست-بيتر (2014). "البرمجة الخطية البارامترية على سلاسل ماركوف". في: دياز، جوزيب؛ لانسي، إيفان؛ سانجيورجي، دافيد (محررون). علوم الحاسوب النظرية . سلسلة محاضرات في علوم الحاسوب. المجلد 7908. سبرينغر برلين هايدلبرغ. الصفحات 207-221 . arXiv : 1406.6683 . Bibcode : 2014arXiv1406.6683C . doi : 10.1007/978-3-662-44602-7_17 . ISBN 978-3-662-44602-7. S2CID 12538495 .

روابط خارجية

عرض تقديمي عن LTL
المنطق الزمني الخطي وأتمتة بوشي
شرائح تعليمية من إعداد البروفيسور أليساندرو أرتالي في جامعة بولزانو الحرة
خوارزميات ترجمة LTL إلى Buchi: سلسلة نسب، من موقع Spot الإلكتروني ، وهي مكتبة للتحقق من النماذج.
Tempus fugit ، لعبة متصفح تدور حول عوامل LTL (بما في ذلك أنماط الماضي).

[1] المنطق في علوم الحاسوب: نمذجة الأنظمة والاستدلال حولها : صفحة 175

[2] "المنطق الزمني الخطي" . مؤرشف من الأصل بتاريخ 30-04-2017 . تم الاطلاع عليه بتاريخ 19-03-2012 .

[Gabbay2003-3] دوف م. غاباي ؛ أ. كوروتش؛ ف. وولتر؛ م. زاخارياشيف (2003). منطق الوسائط متعدد الأبعاد: النظرية والتطبيقات . إلسيفير. ص 46. ISBN 978-0-444-50826-3.

[4] ديكرت، فولكر. "لغات قابلة للتعريف من الدرجة الأولى" (ملف PDF) . جامعة شتوتغارت.

[5] كامب، هانز (1968). منطق الزمن ونظرية الترتيب الخطي (دكتوراه). جامعة كاليفورنيا، لوس أنجلوس.

[6] أمير بنويلي ، المنطق الزمني للبرامج. وقائع الندوة السنوية الثامنة عشرة حول أسس علوم الحاسوب (FOCS) ، 1977، 46-57. doi : 10.1109/SFCS.1977.32

[7] القسم 5.1 من كتاب كريستيل باير وجوست بيتر كاتوين ، مبادئ التحقق من النماذج ، منشورات معهد ماساتشوستس للتكنولوجيا . مؤرشف من الأصل بتاريخ 4 ديسمبر 2010. تم الاطلاع عليه بتاريخ 17 مايو 2011 .

[8] القسم 5.1.5 "الضعف حتى، والتحرير، والشكل الطبيعي الإيجابي" من مبادئ التحقق من النموذج.

[9] أبرامسكي، سامسون ؛ جافويل، سيريل؛ كيرشنر، كلود؛ سبيراكيس، بول (30 يونيو 2010). الأوتوماتا واللغات والبرمجة: الندوة الدولية السابعة والثلاثون، ICALP ... - كتب جوجل . سبرينغر. ISBN 9783642141614تم الاطلاع عليه بتاريخ 30 يوليو 2014 .

[10] موشيه ي. فاردي (2008). "من الكنيسة وما قبلها إلى PSL ". في أورنا غرومبرغ ؛ هيلموت فيث (محرران). 25 عامًا من التحقق من النماذج: التاريخ والإنجازات والآفاق . سبرينغر. ISBN 978-3-540-69849-4.نسخة أولية

[11] أ. بنويلي و ر. روزنر. "حول توليف وحدة تفاعلية". في وقائع الندوة السادسة عشرة لجمعية آلات الحوسبة SIGPLAN-SIGACT حول مبادئ لغات البرمجة (POPL '89). جمعية آلات الحوسبة، نيويورك، نيويورك، الولايات المتحدة الأمريكية، 179-190. https://doi.org/10.1145/75277.75293

[12] موشيه ي. فاردي. مدخلٌ قائم على نظرية الأوتوماتا إلى المنطق الزمني الخطي. وقائع ورشة عمل بانف الثامنة للرتب العليا (بانف 94). سلسلة محاضرات في علوم الحاسوب ، المجلد 1043، الصفحات 238-266، سبرينغر-فيرلاغ، 1996. ISBN 3-540-60915-6.

[13] بوين ألبيرن، فريد ب. شنايدر ، تعريف الحيوية ، رسائل معالجة المعلومات ، المجلد 21، العدد 4، 1985، الصفحات 181-185، الرقم الدولي الموحد للدوريات 0020-0190، https://doi.org/10.1016/0020-0190(85)90056-0

[14] تشاكرابورتي، سويموديب؛ كاتوين، جوست-بيتر (2014). "البرمجة الخطية البارامترية على سلاسل ماركوف". في: دياز، جوزيب؛ لانسي، إيفان؛ سانجيورجي، دافيد (محررون). علوم الحاسوب النظرية . سلسلة محاضرات في علوم الحاسوب. المجلد 7908. سبرينغر برلين هايدلبرغ. الصفحات 207-221 . arXiv : 1406.6683 . Bibcode : 2014arXiv1406.6683C . doi : 10.1007/978-3-662-44602-7_17 . ISBN 978-3-662-44602-7. S2CID 12538495 .

مشروط

حيث

[

[

[

[ 6 ]

[ 7 ]

[ 8 ]

[ 9 ]

[ 10 ]

[ 11 ]

[ 12 ]

[ 13 ]

[ 14 ]