מבוא לאימות תוכנה

ספר אלקטרוני מאת: ניר אדר

6.4.3. סיבוכיות בדיקת מודל

לוגיקה	CTL	LTL
סיבוכיות	$plot:$O\left( {\left\| M \right\| \cdot \left\| f \right\|} \right)$$	$plot:$O\left( {\left\| M \right\| \cdot {2^{\left\| f \right\|}}} \right)$$

$plot:$\left| M \right|$$ הוא מספר המצבים במבנה plot:$M$ ו- $plot:$\left| f \right|$$ הוא אורך הנוסחה plot:$f$ .

חלק מהדרך להצגת הסיבוכיות של CTL הוצגה: האלגוריתם לסימון, כאשר אנחנו מתחילים לסמן את הנוסחאות האטומיות ועולים כלפי מעלה, ובכל שלב אנחנו מניחים שנוסחאות מהשלב הקודם ניתן לקבל את ערכן ב- $plot:$O\left( 1 \right)$$ (מתקיים כי ערכן כבר חושב).

בדיקת מודל ב-LTL היא מעבר להיקפו של מסמך זה, והסיבוכיות מוצגת לידיעת הקורא בלבד.

לכאורה LTL בסיבוכיות יותר גבוהה מ-CTL אבל זה נובע רק מצורת הכתיבה. ניתן לרשום למשל:

עבור CTL: $plot:$O\left( {{2^{\left| {R\left( M \right)} \right|}} \cdot \left| f \right|} \right)$$ כאשר $plot:$\left| {R\left( M \right)} \right|$$ הוא מספר הביטים הדרושים לייצוג המבנה plot:$M$ ,