טיוטה:תכונת זמן ליניארי

תכונת זמן ליניארי מוגדרת בבדיקות מודל, שיטה מרכזית באימות תוכנה - ענף של מדעי המחשב.והיא משמשת לתיאור הדרישות של מודל של מערכת מחשב. לדוגמה התכונה: "המכונה האוטומטית אינה נותנת משקה עד שהכניסו כסף" (תכונת בטיחות) או: "התכנית מסתיימת בסופו של דבר" (תכונת חייות ). ניתן להשתמש בתכונת הוגנות כדי לשלול נתיבים לא מציאותיים של מודל. לדוגמה, במודל של שני רמזורים, תכונת החייות "שני הרמזורים ירוקים אין סוף פעמים" עשויה להיות נכונה רק תחת מגבלת ההגינות הבלתי מותנית: "כל רמזור משנה את צבעו אינסוף פעמים" (כדי לא לכלול את המקרה שבו רמזור אחד הוא "מהיר באופן אינסופי" מהאחר). [1]

באופן פורמלי, תכונת זמן ליניארית היא שפת ω על קבוצת החזקה של "פסוקים אטומיים". כלומר, המאפיין מכיל רצפים של קבוצות של פסוקים, כל רצף ידוע בשם "מילה". כל מאפיין יכול להיכתב כ" P ו- Q שניהם מתרחשים" עבור מאפיין בטיחות כלשהו P ומאפיין חייות Q. אינוריאנט למערכת הוא משהו שהוא נכון או לא נכון עבור מצב מסוים. מאפיינים בלתי משתנים מתארים אינוריאנט שכל מצב שניתן להגיע אליו במודל חייב לעמוד בו, בעוד שמאפייני שמורה הם בנוסח "החל מרגע מסוים בריצה, לנצח מתקיים איזשהו אינוריאנט".

לוגיקת זמן כגון לוגיקה זמנית ליניארית מתארת סוגים של מאפייני זמן ליניאריים באמצעות נוסחאות.

מאמר זה עוסק במאפייני זמן ליניאריים פרופוזיציוניים ואינו יכול להתמודד עם פרדיקטים לגבי מצבי תוכנית, כך שהוא לא יכול להגדיר מאפיין כמו: הערך הנוכחי של y קובע את מספר הפעמים ש-x עובר בין 0 ל-1 לפני סיום. הפורמליזם הכללי יותר בשימוש במאפייני בטיחות וחיות יכול להתמודד עם זה.

הַגדָרָה

תהי AP קבוצה של פסוקים אטומיים. מילה מעל $2^{AP}$ ( קבוצת החזקה של AP ) היא רצף אינסופי של קבוצות של פסוקים, לדוגמה$w:=\{a\}\{a,b\}\emptyset \{a,b\}^{\omega }$ (עבור הפסוקים האטומיים $AP=\{a,b\}$ ). תכונת זמן ליניארי (LT) מעל AP הוא תת-קבוצה של $(2^{AP})^{\omega }$ כלומר קבוצה של מילים. [2] דוגמה למאפיין LT מעל הקבוצה $\{a,b\}$ הוא "קבוצת המילים המכילה את a אינסוף פעמים". המילה w נמצאת בקבוצה הזו, מכיוון ש-a כלול ב $\{a,b\}$, שמתרחשת אינסוף פעמים. מילה שלא בקבוצה היא $x:=\{a\}(\{b\}\emptyset )^{\omega }$, שכן a מופיעה רק פעם אחת (בקבוצה הראשונה).

מאפיין LT הוא שפת ω מעל האלפבית $\Sigma =2^{AP}$ (ולהפך).

נסמן ב- pref ( w ) את הרישות הסופיות של w (כלומר $\{\{a\},\{a\}\{a,b\},\{a\}\{a,b\}\emptyset ,...\}$ במקרה שלעיל). הסגור של מאפיין LT P היא:

${\mathit {closure}}(P):=\{\sigma \in (2^{AP})^{\omega }\mid {\mathit {pref}}(\sigma )\subseteq {\mathit {pref}}(P)\}$

יישומים

מבנה קריפקה נגמר $\{p,q\}$ . הוא אינו עונה על התכונה LT "אינסוף פעמים q ", בגלל הנתיב $s_{1}s_{2}s_{3}^{\omega }$ . זה כן מספק את התכונה "לאינסוף פעמים p ", כי כל המסלולים האפשריים נכנסים ל- $s_{1}$ אוֹ $s_{3}$ אינסוף פעמים.

באמצעות התיאוריה של אוטומט סופי, ניתן לתכנן תוכנית או מערכת מחשב על ידי מבנה Kripke . תכונות זמן ליניארי מתארים אז הגבלות על עקבות (פלטים) של מבנה Kripke. לדוגמה, אם שני רמזורים בצומת מיוצגים על ידי מבנה קריפקה אזי הפסוקים האטומיים עשויות להיות הצבעים האפשריים של כל אור וייתכן שרצוי שהעקבות יעמדו בתכונה "הרמזור לא יכול להיות שניהם ירוקים ב- באותו זמן" (כדי למנוע התנגשויות מכוניות). [3]

אם כל עקבה במבנה קריפקה TS הוא גם עקבה ב- 'TS אז כל תכונה LT ש- TS' מקיימת, תקויים גם על-ידי TS . משפט זה שימושי בבדיקת מודלים כדי לאפשר הפשטה: אם מודל מפושט של המערכת עונה על תכונת LT אז המודל האמיתי של המערכת יספק אותו גם כן. [4]

סיווג תכונות זמן ליניארי

תכונת בטיחות משמעה בצורה לא פורמלית "דבר רע לא קורה". [5] לדוגמה, אם מערכת מסמלצת מכשיר כספומט, אז מאפיין כזה הוא "אין להוציא כסף אלא אם כן הוזן PIN". [6] מבחינה פורמלית, תכונת בטיחות הוא מאפיין LT כך שלכל מילה המפרה את התכונה יש "רישא רעה", ששום מילה עם אותה רישא לא מקיימת את התכונה. כלומר, [7]

$\forall \sigma \in (2^{AP})^{\omega }\setminus P\ \exists {\text{ a finite prefix}}\ {\hat {\sigma }}:P\cap \{\sigma '\mid {\hat {\sigma }}\ {\text{is a prefix of}}\ \sigma '\}=\emptyset$

בדוגמה של הכספומט, רישא רעה מינימלית היא קבוצה סופית של שלבים שבוצעו בהם כסף מופק בשלב האחרון ולא הוזן PIN בשום שלב. כדי לאמת תכונה בטיחותית, די בדוק רק את העקבות הסופיות של מבנה קריפקה ולבדוק אם עקבות אלו הן רישות רעות. [8]

תכונה LT P היא תכונה בטיחותית אם ורק אם ${\mathit {closure}}(P)=P$ . [9]

תכונת שמורה

תכונת שמורה היא סוג של תכונה בטיחותית שבה המצב מתייחס רק למצב הנוכחי. [10] לדוגמה, בדוגמת הכספומט אינה משתנה מכיוון שאיננו יכולים לדעת אם הנכס מופר על ידי ראייה שהמצב הנוכחי הוא "לחלק כסף", רק על ידי ראייה שהמצב הנוכחי הוא "לחלק כסף" ושום מצב קודם לא "נקרא" פִּין". דוגמה לתכונת שמורה היא מצב הרמזור "הרמזור לא יכול להיות שניהם ירוקים בו זמנית" לעיל. דוגמה נוספת היא "המשתנה x לעולם אינו שלילי", במודל של תוכנית מחשב.

פורמלית, תכונת שמורה הוא מהצורה:

$P=\{A_{0}A_{1}....\in (2^{AP})^{\omega }\mid \forall j\in \mathbb {N} :A_{j}\ {\text{satisfies}}\ \Phi \}$

עבור פסוק לוגי כלשהו $\Phi$ . [10]

מבנה קריפקה עונה על תכונת שמורה אם ורק אם כל מצב שניתן להגיע אליו עונה על תכונת השמורה, ניתן לבדוק זאת על ידי אלגוריתם חיפוש לרוחב או אלגוריתם חיפוש לעומק. [11] ניתן לאמת את תכונות הבטיחות באופן אינדוקטיבי באמצעות אינווריאנטים. [12]