Synthesis Algorithms for Gene Networks

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

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

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

מטרת הפרויקט לפתח אלגוריתמים לסינתזה של רשתות גנטיות תוך שימוש באימות פורמלי (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. A. Pnueli and R. Rosner "On the synthesis of a reactive module". POPL '89 Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, Pages 179-190, 1989.
3. Boyan Yordanov, Sara-Jane Dunn, Colin Gravill, Hillel Kugler, Christoph M Wintersteiger
4. An SMT-Based Framework for Reasoning About Discrete Biological Models. ISBRA’22, LNCS Springer 2022.