6.4.4.3. אלגוריתם לחישוב קבוצת המצבים המספקים ![plot:${E_F}G{\varphi _1}$](/documentResources/326/plot_1396.png)
רכיב קשיר היטב הוגן – רכיב קשיר היטב
הינו הוגן אם לכל
![plot:$C \cap {h_i} \ne
\emptyset $](/documentResources/326/plot_1399.png)
נבנה
באופן הבא (נשים לב כי
מוגדרים כמו קודם):
![plot:\[\begin{gathered}
M' = \left( {S',R',L',H'} \right) \hfill \\
S' = \left\{ {\left. S \right|M,S{ \vDash _F}{\varphi _1}} \right\}
\hfill \\
R' = \left( {S' \times S'} \right) \cap R \hfill \\
L'\left( s \right) = L\left( s \right),s \in S' \hfill \\
H' = \left\{ {\underbrace {{h_i} \cap S'}_{{{h'}_i}}\left| {{h_i} \in H}
\right.} \right\} \hfill \\
\end{gathered} \]](/documentResources/326/plot_209.png)
הערה: אם
נסיק כי M מסלול הוגן המספק את
(אין מסלולים הוגנים).
למה:
אמ"ם מתקיימים 2
התנאים:
![plot:$s \in S'$](/documentResources/326/plot_1405.png)
- יש מסלול ב-
מ-
למצב
ברכיב קשיר היטב מקסימאלי, לא טריוויאלי והוגן.
טיפול ב-![plot:${E_F}G{\varphi
_1}$](/documentResources/326/plot_1409.png)
האלגוריתם:
- בנו
![plot:$\left| H \right| + \left| R \right| + \left| S \right|$](/documentResources/326/plot_1411.png)
- מצאו את הרכיבים הקשירים היטב המקסימאליים, כולל הטריוויאלים
![plot:$\left| S \right| + \left| R \right|$](/documentResources/326/plot_1412.png)
- מצאו את הרכיבים הקשירים היטב המקסימאליים, הלא טריוויאליים
וההוגנים.
![plot:$\left| S \right| \cdot \left| H \right|$](/documentResources/326/plot_1413.png)
- סמנו את כל המצבים מ-3 ב-
וכן בסריקה אחורנית סמנו את כל המצבים שמהם ישיגים מצבים שמסומנים ב-
. ![plot:$\left| S \right| + \left| R
\right|$](/documentResources/326/plot_1416.png)
סיבוכיות כוללת: ![plot:$0\left( {\left| S \right| \cdot \left| H \right| + \left| R \right|}
\right)$](/documentResources/326/plot_1417.png)