Algorithms for Synthesis of GRNs for Stem Cells

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

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

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

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

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

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

קורסי קדם:

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

מקורות:

1. Carbognin et al Esrrb guides naive pluripotent cells through the formative transcriptional programme. Nature cell biology, 2023.
2. Manna, Zohar, and Amir Pnueli. "Temporal verification of reactive systems: safety." Springer (1995).
3. 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.
4. Boyan Yordanov, Sara-Jane Dunn, Colin Gravill, Hillel Kugler, Christoph M Wintersteiger
5. An SMT-Based Framework for Reasoning About Discrete Biological Models. ISBRA’22, LNCS Springer 2022.