بنية كريپكي (التحقق من النموذج)

بنية كريپكي هي شكل من أشكال نظام الانتقال ، اقترحه في الأصل شاول كريپكي ^{[ 1 ]} ، ويُستخدم في التحقق من النماذج ^{[ 2 ]} لتمثيل سلوك النظام. تتكون هذه البنية من رسم بياني تمثل عقده الحالات التي يمكن الوصول إليها في النظام، وتمثل حوافه انتقالات الحالة، بالإضافة إلى دالة تصنيف تربط كل عقدة بمجموعة من الخصائص التي تنطبق على الحالة المقابلة. تُفسَّر المنطق الزمني تقليديًا باستخدام بنى كريپكي.

التعريف الرسمي

ليكن $AP$ مجموعة من القضايا الذرية ، أي التعبيرات ذات القيم المنطقية المكونة من متغيرات وثوابت ورموز مسندات. يُعرّف كلارك وآخرون ^{[ 3 ]} بنية كريپكي على $AP$ على أنها رباعية $M = (S, I, R, L)$ تتكون من

مجموعة محدودة من الحالات $S.$
مجموعة من الحالات الأولية $I \subseteq S$ .
علاقة انتقال $R \subseteq S \times S$ بحيث تكون $R$ كلية يسارية ، أي $\foralls \in S \existss' \in S$ بحيث $(s,s')$ ∈ $R.$
دالة التسمية (أو التفسير ) $L : S \to 2 AP$ .

بما أن $R$ هي مجموعة كاملة من اليسار ، فمن الممكن دائمًا إنشاء مسار لانهائي عبر بنية كريپكي. يمكن نمذجة حالة الجمود بحافة واحدة صادرة إلى نفسها. تحدد دالة التسمية $L$ لكل حالة $s \in S$ المجموعة $L (s)$ لجميع القضايا الذرية الصالحة في $s$ .

المسار في البنية $M هو$ سلسلة من الحالات $ρ$ $=$ $s1$ $,$ $s2$ $,$ $s3$ $,$ $...$ بحيث يكون لكل $i$ $>$ $0$ ، يتحقق $الشرط$ $R$ $($ $si$ $,$ $si$ $+1$ $)$ $.$ الكلمة على المسار $ρ$ هي سلسلة من مجموعات القضايا الذرية $w$ $=$ $L$ $($ $s1$ $)$ $,$ $L$ $($ $s2$ $)$ $,$ $L$ $($ $s3$ ) $, ...$ $،$ $وهي$ كلمة ω على الأبجدية $2AP$ $.$

وفقًا لهذا التعريف، يمكن تعريف بنية كريپكي (على سبيل المثال، التي لها حالة ابتدائية واحدة فقط $i \in I) بأنها$ آلة مور ذات أبجدية إدخال أحادية، وأن دالة الإخراج هي دالة التسمية الخاصة بها. ^{[ 4 ]}

مثال

لنفترض أن مجموعة القضايا الذرية $AP = {p, q}$ . يمكن لـ $p$ و $q$ أن تمثل خصائص منطقية عشوائية للنظام الذي يمثله هيكل كريپكي.

يوضح الشكل على اليمين بنية كريپكي $M = (S, I, R, L)$ ، حيث

$S = {s 1, s 2, s 3}$ .
$I = {s 1}$ .
$R = {(s 1, s 2), (s 2, s 1) (s 2, s 3), (s 3, s 3)}$ .
$L = {(s 1, {p, q}), (s 2, {q}), (s 3, {p})}$ .

$قد تُنتج M$ مسارًا $ρ = s1, s2, s1, s2, s3, s3, s3, ...$ و $w = {p, q}, {q}, {p, q}, {q}, {p}, {p}, {p}, ...$ هي كلمة التنفيذ على المسار $ρ$ . يمكن لـ $M$ إنتاج كلمات تنفيذ تنتمي إلى اللغة $({p, q}{q})*({p}) ω \cup ({p, q}{q}) ω$ .

العلاقة بالمفاهيم الأخرى

على الرغم من شيوع هذا المصطلح في مجتمع التحقق من النماذج، فإن بعض الكتب الدراسية في هذا المجال لا تُعرّف "بنية كريپكي" بهذه الطريقة الموسعة (أو لا تُعرّفها على الإطلاق في الواقع)، بل تستخدم ببساطة مفهوم نظام انتقال (مُصنّف) ، والذي يحتوي بالإضافة إلى ذلك على مجموعة من الأفعال $(Act$ )، وتُعرّف علاقة الانتقال على أنها مجموعة فرعية من $S \times Act \times S$ ، والتي تُوسّعها هذه الكتب لتشمل مجموعة من القضايا الذرية ودالة تصنيف للحالات أيضًا ( $L$ كما هو مُعرّف أعلاه). في هذا النهج، تُسمى العلاقة الثنائية التي يتم الحصول عليها من خلال تجريد تصنيفات الأفعال بمخطط الحالة . ^{[ 5 ]}

أعاد كلارك وآخرون تعريف بنية كريپكي على أنها مجموعة من الانتقالات (بدلاً من انتقال واحد فقط)، وهو ما يعادل الانتقالات المصنفة أعلاه، عندما قاموا بتعريف دلالات حساب μ الموجه . ^{[ 6 ]}

انظر أيضاً

مراجع

↑ كريپكي، شاول، 1963، "اعتبارات دلالية حول المنطق الموجه"، أكتا فيلوسوفيكا فينيكا، 16: 83-94
↑ كلارك، إدموند م. (2008): نشأة التحقق من النماذج. في: غرومبيرغ، أورنا وفيث، هيلموت (محرران): 25 عامًا من التحقق من النماذج، المجلد 5000: سلسلة محاضرات في علوم الحاسوب. سبرينغر برلين هايدلبرغ، ص 1-26.
↑ كلارك، إدموند إم. الابن؛ غرومبيرغ، أورنا ؛ بيليد، دورون (ديسمبر 1999). التحقق من النماذج . سلسلة الأنظمة الفيزيائية السيبرانية. مطبعة معهد ماساتشوستس للتكنولوجيا. ص 14. ISBN 978-0-262-03270-4.
↑ كلاوس شنايدر (2004). التحقق من الأنظمة التفاعلية: الأساليب الرسمية والخوارزميات . سبرينغر. ص 45. ISBN 978-3-540-00296-3.
^ كريستيل باير . جوست بيتر كاتوين (2008). مبادئ فحص النماذج . مطبعة معهد ماساتشوستس للتكنولوجيا. ص 20 – 21 و 94 – 95. رقم ISBN 978-0-262-02649-9.
↑ كلارك وآخرون، ص 98

[1] كريپكي، شاول، 1963، "اعتبارات دلالية حول المنطق الموجه"، أكتا فيلوسوفيكا فينيكا، 16: 83-94

[2] كلارك، إدموند م. (2008): نشأة التحقق من النماذج. في: غرومبيرغ، أورنا وفيث، هيلموت (محرران): 25 عامًا من التحقق من النماذج، المجلد 5000: سلسلة محاضرات في علوم الحاسوب. سبرينغر برلين هايدلبرغ، ص 1-26.

[Clarke1999-3] كلارك، إدموند إم. الابن؛ غرومبيرغ، أورنا ؛ بيليد، دورون (ديسمبر 1999). التحقق من النماذج . سلسلة الأنظمة الفيزيائية السيبرانية. مطبعة معهد ماساتشوستس للتكنولوجيا. ص 14. ISBN 978-0-262-03270-4.

[Schneider2004-4] كلاوس شنايدر (2004). التحقق من الأنظمة التفاعلية: الأساليب الرسمية والخوارزميات . سبرينغر. ص 45. ISBN 978-3-540-00296-3.

[BaierKatoen2008-5] كريستيل باير . جوست بيتر كاتوين (2008). مبادئ فحص النماذج . مطبعة معهد ماساتشوستس للتكنولوجيا. ص 20 – 21 و 94 – 95. رقم ISBN 978-0-262-02649-9.

[6] كلارك وآخرون، ص 98

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]