כל מה שרצית לדעת על לוגיקת זמן:
לוגיקת זמן, או לוגיקה טמפורלית (באנגלית: Temporal Logic) היא הרחבה של הלוגיקה הקלאסית המאפשרת ביטויים הקשורים בזמן.
לוגיקת זמן היא חלק מהלוגיקה המודלית.
לוגיקת זמן מאפשרת לנו לעסוק בקו זמן, ועל כן מאפשרת לנו לנסח מתמטית משפטים כמו "אני תמיד רעב", "לבסוף אהיה רעב", או "אהיה רעב עד שאוכל משהו".
קו הזמן מתחלק לשני סוגים אפשריים: קו זמן לינארי, שמוגבל לקו זמן אפשרי אחד (כמו בדוגמאות לעיל), וקו זמן מסתעף (Branching logic) שמאפשר לעבוד במספר קוי זמן חלופיים במקביל.
בצורה כזו אנו מניחים מראש סביבה לא צפויה שמספר דברים שונים יכולים להתרחש בה.
בסביבה כזו נוכל לנסח את המשפטים: "יש אפשרות שאשאר רעב לנצח" או "יש אפשרות שלבסוף לא אהיה רעב".
במידה ואנו לא יודעים אם אי פעם אוכל – שני המשפטים הם בחזקת נכונים.
אמיר פנואלי זכה בשנת 1996 בפרס טיורינג על הכנסת לוגיקת הזמן אל מדעי המחשב.
כיום נעשה שימוש נרחב בלוגיקת זמן באימות תוכנה כדי להוכיח מתמטית נכונות של מערכת מחשב, זאת להבדיל מתהליך בדיקת תוכנה על ידי בודקי תוכנה אנושיים.

נלקח מויקיפדיה

הגדרות נוספות הקשורות ללוגיקת זמן:
•לוגיקה