Formal Verification Methods for solving spatial games

הרקע לפרויקט:

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

מטרת הפרויקט:

מטרת הפרויקט לפתח אלגוריתמים לפתרון משחקים מרחביים תוך שילוב של שימוש באימות פורמלי
ולמידת מכונה. אימות פורמלי מאפשר שימוש באלגוריתמים ושיטות מתמטיות להוכחת נכונות של מערכות תוכנה וחומרה מורכבות. בפרויקט נלמד איך שיטות אלה יכולות להיות מיושמות ומורחבות למשחקים מרחביים, כולל משחק Sokoban שהוא משחק מאתגר לפתרון ממוחשב.

תכולת הפרויקט:

במהלך הפרויקט הסטודנטים ירכשו ידע בשיטות אימות פורמלי וסינתזה (Formal Verification and Synthesis) וייפתחו ויבדקו אלגוריתמים לפתרון יעיל ככל הניתן למשחקים מרחביים כולל Sokoban . אלגוריתמים של למידת מכונה ישולבו עם שיטות אימות כדי לשפר ביצועים ולאפשר פתרון של קונפיגורציות מורכבות.

קורסי קדם:

Formal Verification and Synthesis (במקביל לפרויקט)

מקורות:

1. Manna, Zohar, and Amir Pnueli. "Temporal verification of reactive systems: safety." Springer (1995).
2. Yaron Shoham, Gal Elidan. Demonstrating scalable Verification on large benchmarks. (2121).
3. https://www.mathsisfun.com/games/sokoban.html