לוגיקת זמן

לוגיקת זמן, לוגיקה עתית או לוגיקה טמפורלית (באנגלית: Temporal Logic) היא הרחבה של הלוגיקה הקלאסית המאפשרת ביטויים הקשורים בזמן. לוגיקת זמן היא חלק מהלוגיקה המודלית.

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

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

אופרטורים של לוגיקת זמן

לוגיקת זמן מכילה שני סוגי אופרטורים: אופרטורים לוגיים ואופרטורים מודליים. האופרטורים הלוגיים הם פעולות בוליאניות רגילות ($\mathrm{\neg },\vee ,\wedge ,\to$). האופרטורים המודליים שמשתמשים בהם בלוגיקת זמן מוגדרים כך:

טקסטואלי	סימול	הגדרה	הסבר	תרשים
אופרטורים בינאריים
$\varphi$ U $\psi$	$\varphi 𝒰\psi$	$\begin{array}{c}(B𝒰C)(\varphi )=\\ (\mathrm{\exists }i:C({\varphi }_i)\wedge (\mathrm{\forall }j<i:B({\varphi }_j)))\end{array}$	$\varphi$ מתקיים עד ש- $\psi$ מתקיים: $\psi$ מתקיים בנקודת הזמן הנוכחית או בנקודת זמן עתידית, ועד נקודת זמן זו $\varphi$ חייב להתקיים. מנקודת הזמן בה $\psi$ מתקיים, $\varphi$ כבר לא חייב להתקיים.	<timeline> ImageSize = width:240 height:94 PlotArea = left:30 bottom:30 top:0 right:20 DateFormat = x.y Period = from:0 till:6 TimeAxis = orientation:horizontal AlignBars = justify ScaleMajor = gridcolor:black increment:1 start:0 ScaleMinor = gridcolor:black increment:1 start:0 PlotData= bar:p color:red width:10 align:left fontsize:S from:1 till:3 bar:q color:red width:10 align:left fontsize:S from:3 till:5 bar:pUq color:red width:10 align:left fontsize:S from:1 till:5 </timeline>
$\varphi$ R $\psi$	$\varphi ℛ\psi$	$\begin{array}{c}(BℛC)(\varphi )=\\ (\mathrm{\forall }i:C({\varphi }_i)\vee (\mathrm{\exists }j<i:B({\varphi }_j)))\end{array}$	$\varphi$ משחרר את $\psi$ : $\psi$ מתקיים עד נקודת הזמן הראשונה בה $\varphi$ מתקיים (ואחרי זה $\psi$ יכול להתקיים או לא להתקיים), או ש- $\psi$ מתקיים לנצח אם $\varphi$ לא מתקיים לעולם.	<timeline> ImageSize = width:240 height:100 PlotArea = left:30 bottom:30 top:0 right:20 DateFormat = x.y Period = from:0 till:6 TimeAxis = orientation:horizontal AlignBars = justify ScaleMajor = gridcolor:black increment:1 start:0 ScaleMinor = gridcolor:black increment:1 start:0 PlotData= bar:p color:red width:10 align:left fontsize:S from:2 till:4 bar:q color:red width:10 align:left fontsize:S from:1 till:3 from:5 till:6 bar:pRq color:red width:10 align:left fontsize:S from:1 till:3 from:5 till:6 </timeline>
אופרטורים אונריים
N $\varphi$	$\circ \varphi$	$𝒩B({\varphi }_i)=B({\varphi }_{i+1})$	$\varphi$ מתקיים בנקודת הזמן הבאה.	<timeline> ImageSize = width:240 height:60 PlotArea = left:30 bottom:30 top:0 right:20 DateFormat = x.y Period = from:0 till:6 TimeAxis = orientation:horizontal AlignBars = justify ScaleMajor = gridcolor:black increment:1 start:0 ScaleMinor = gridcolor:black increment:1 start:0 PlotData= bar:p color:red width:10 align:left fontsize:S from:2 till:3 from:5 till:6 bar:Np color:red width:10 align:left fontsize:S from:1 till:2 from:4 till:5 </timeline>
F $\varphi$	$◊\varphi$	$ℱB(\varphi )=(true𝒰B)(\varphi )$	לבסוף: לבסוף $\varphi$ מתקיים. כלומר בהכרח קיימת נקודה עתידית שבה $\varphi$ מתקיים.	<timeline> ImageSize = width:240 height:60 PlotArea = left:30 bottom:30 top:0 right:20 DateFormat = x.y Period = from:0 till:6 TimeAxis = orientation:horizontal AlignBars = justify ScaleMajor = gridcolor:black increment:1 start:0 ScaleMinor = gridcolor:black increment:1 start:0 PlotData= bar:p color:red width:10 align:left fontsize:S from:2 till:3 from:4 till:5 bar:Fp color:red width:10 align:left fontsize:S from:0 till:5 </timeline>
G $\varphi$	$◻\varphi$	$𝒢B(\varphi )=\mathrm{\neg }ℱ\mathrm{\neg }B(\varphi )$	תמיד: $\varphi$ תמיד מתקיים.	<timeline> ImageSize = width:240 height:60 PlotArea = left:30 bottom:30 top:0 right:20 DateFormat = x.y Period = from:0 till:6 TimeAxis = orientation:horizontal AlignBars = justify ScaleMajor = gridcolor:black increment:1 start:0 ScaleMinor = gridcolor:black increment:1 start:0 PlotData= bar:p color:red width:10 align:left fontsize:S from:1 till:3 from:4 till:6 bar:Gp color:red width:10 align:left fontsize:S from:4 till:6 </timeline>
A $\varphi$		$\begin{array}{c}(𝒜B)(\psi )=\\ (\mathrm{\forall }\varphi :{\varphi }_0=\psi \to B(\varphi ))\end{array}$	$\varphi$ מתקיים תמיד בכל נקודות הזמן בכל המסלולים שמתחילים בנקודת זמן זו.
E $\varphi$		$\begin{array}{c}(ℰB)(\psi )=\\ (\mathrm{\exists }\varphi :{\varphi }_0=\psi \wedge B(\varphi ))\end{array}$	קיים לפחות מסלול אחד מנקודת זמן זו שבו $\varphi$ מתקיים.

סימולים אלטרנטיביים:

• אופרטור R מוחלף לעיתים על ידי הסימון V.
• אופרטור W משמעו U חלש ושקול ל- $fUg\vee Gf$. כלומר $\varphi 𝒲\psi$ משמעו $\varphi$ מתקיים עד ש- $\psi$ מתקיים, או ש- $\varphi$ ממשיך להתקיים לעולם.

אופרטורים אונריים מוגדרים היטב כאשר (B($\varphi$ מוגדר היטב. אופרטורים בינאריים מוגדרים היטב כאשר (B($\varphi$ ו- (C($\varphi$ מוגדרים היטב.

שקילויות

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

• $◻◻\varphi =◻\varphi$
• $◊◊\varphi =◊\varphi$
• $\varphi \to ◊\varphi$
• $◊◻◊\varphi =◻◊\varphi$
• $◻◊◻\varphi =◊◻\varphi$
• $\mathrm{\neg }◻\varphi \to ◊\mathrm{\neg }\varphi$
• $\mathrm{\neg }◊\varphi \to ◻\mathrm{\neg }\varphi$
• $\circ \varphi \to ◊\varphi$
• $◊\psi \to ◊(\varphi 𝒰\psi )$
• $◻\varphi \vee ◻\psi \to ◻(\varphi \vee \psi )$
• $◻\varphi \wedge ◻\psi =◻(\varphi \wedge \psi )$

ראו גם

• לוגיקה
• לוגיקה מודלית
• אימות תוכנה