6.4.3. סיבוכיות בדיקת מודל
לוגיקה |
CTL |
LTL |
סיבוכיות |
![plot:$O\left( {\left|
M \right| \cdot \left| f \right|} \right)$](/documentResources/326/plot_1335.png) |
![plot:$O\left( {\left|
M \right| \cdot {2^{\left| f \right|}}} \right)$](/documentResources/326/plot_1336.png) |
הוא מספר המצבים במבנה
ו-
הוא אורך הנוסחה
.
חלק מהדרך להצגת הסיבוכיות של CTL
הוצגה: האלגוריתם לסימון, כאשר אנחנו מתחילים לסמן את הנוסחאות האטומיות ועולים
כלפי מעלה, ובכל שלב אנחנו מניחים שנוסחאות מהשלב הקודם ניתן לקבל את ערכן ב-
(מתקיים כי ערכן כבר חושב).
בדיקת מודל ב-LTL היא מעבר להיקפו של מסמך זה,
והסיבוכיות מוצגת לידיעת הקורא בלבד.
לכאורה LTL בסיבוכיות יותר גבוהה מ-CTL אבל
זה נובע רק מצורת הכתיבה. ניתן לרשום למשל:
עבור CTL:
כאשר
הוא מספר הביטים הדרושים
לייצוג המבנה
,
עבור LTL: ![plot:$O\left( {{2^{\left| {R\left( M \right)} \right|}} \cdot {2^{\left| f \right|}}}
\right)$](/documentResources/326/plot_1345.png)