UPPAAL Tiga הוא הרחבה של [BDL04] UPPAAL והוא מיישם את האלגוריתם יעיל הראשון ב- the-fly לפתרון משחקים מבוססים על אוטומטים משחק מתוזמן ביחס לנכסי reachability ובטיחות.
למרות שמשחקי מתוזמן לכבר מזמן ידועים כלהכריע בי עד עכשיו יש כבר חוסר אלגוריתמים יעילים ובאמת על-the-fly לניתוח שלהם.
UPPAAL Tiga מספק ממשק ידידותי למשתמש גרפי עם השרת המקביל שלה, ואימות שורת הפקודה.
האלגוריתם אנו מציעים [CDFLL05] הוא הרחבה סמלית של האלגוריתם על-the-fly שהוצע על ידי יו & Smolka [LS98] ליניארי-זמן-מודל בדיקה של מערכות-סופי מדינה. להיות על-the-fly, האלגוריתם הסמלי רשאי לסיים הרבה לפני שחקר את חלל המדינה כולה.
גם הצעדים הבודדים של האלגוריתם מתבצעים ביעילות על ידי שימוש באזורים שנקרא כמבנה נתונים הבסיסי. הכלי שלנו מיישם אופטימיזציות שונות של האלגוריתם הסמלי הבסיסי, כמו גם שיטות להשגת אסטרטגיות זכיית זמן אופטימלי (למשחקי reachability).
מה חדש במהדורה זו:
תגובות לא נמצא