שם הפריט: אימות נוסחאות LTL ובניית מודל אוטומט LGBA
שם המחבר: עודד פרץ
| שם הפריט: | אימות נוסחאות LTL ובניית מודל אוטומט LGBA עפ |
| מחברים: | עודד פרץ |
| מקום הפיתוח: | המחלקה להוראת המדעים, מכון ויצמן למדע |
| תחום דעת: | מתמטיקה, הוראת המתמטיקה |
| סוג הפריט: | עבודת גמר |
| שנת פרסום: | 2012 |
| מילות מפתח: | לוגיקה קלאסית, לוגיקת הזמנים הלינארית (LTL), אוטומט בושי, אימות תוכנה, Linear Temporal Logic- LTL LGBA: Labeled Generalized Buchi Automaton Model checking |
| גודל הקובץ: | 868Kb |
| הפנייה לפריט: | http://stwww.weizmann.ac.il/teachersacademy/maagar/uploads/22052013_1071071288.docx |
| מקור: | תוכנית רוטשילד-ויצמן למצוינות בהוראת המדעים |
| תקציר: | העבודה עוסקת במערכות אוטומטיות המשתמשות בשיטת ה- model checking, כלומר ע"י אלגוריתמים וגרפים המשתמשים בלוגיקה טמפורלית (עיתית – תלוית זמן), על מנת לבצע בדיקת תקינות המערכת. במסגרת זאת העבודה תציג את הנושאים הבאים: הגדרת הלוגיקה הטמפורלית והדגמה של מספר נוסחאות בשפה; הגדרת האוטומט LGBA ומספר דוגמאות של אוטומטים אלו; מאפייני ה-Model Checking; האלגוריתם של ורדי-פלד-גרט-וולפר לאימות בזמן אמת של נוסחה ב-LTL ומציאת אוטומט (LGBA) מתאים לנוסחה; מספר דוגמאות לבדיקת נוסחאות ב-LTL ויצירת אוטומט עבורן; מספר שיפורים שהוצעו ע"י מפתחי האלגוריתם והצעת המחבר לשיפורים חדשים. |
| מקוריות: | מקורי |
| קהל יעד: | מורים ותלמידים למתמטיקה בחטיבה העליונה |
| הערות: | מנחה: פרופ' מוטי בן ארי |
| קישורים: |
23
נוב
2016
נוב
2016
0