Solving spatial planning problems using Formal Verification

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

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

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

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

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

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

קורסי קדם:

83691 Formal Verification and Synthesis

מקורות:

1. Manna, Zohar, and Amir Pnueli. "Temporal verification of reactive systems: safety." Springer (1995).
2. MATT LUCKCUCK, MARIE FARRELL, LOUISE A. DENNIS, CLARE DIXON, and MICHAEL FISHER, Formal Specification and Verification of Autonomous Robotic Systems: A Survey. ACM Computing Surveys Volume 52 Issue 5, 2019.