6.5.2. יצוג מבנה קריפקה על ידי פונקציה בוליאנית - דוגמא
קידוד של מצבים
נשתמש במשתנים
כדי לייצג קידוד של מצבים. לדוגמא:
![](/documentResources/326/image086.png)
![plot:${f_{\left\{
{{S_1}} \right\}}}\left( {{v_1},{v_2}} \right) = \neg {v_1} \wedge \neg {v_2}$](/documentResources/326/plot_1470.png)
נוסחה
מייצגת קבוצה A
אמ"מ ההשמות המספקות ל-
מתאימות בדיוק לקידוד של איברי A.
![plot:\[{f_{\left\{
{{S_3}} \right\}}}\left( {{v_1},{v_2}} \right) = \neg {v_1} \wedge {v_2}\]](/documentResources/326/plot_214.png)
![plot:\[{f_{\left\{
{{S_1},{S_3}} \right\}}}\left( {{v_1},{v_2}} \right) = \left( {\neg {v_1}
\wedge {v_2}} \right) \vee \left( {\neg {v_1} \wedge \neg {v_2}} \right) = \neg
{v_1}\]](/documentResources/326/plot_215.png)
![plot:${f_{\left\{
{{S_2}} \right\}}}\left( {{v_1},{v_2}} \right) = {v_1} \wedge {v_2}$](/documentResources/326/plot_1473.png)
ייצוג רלציית המעברים
אם נתונים המשתנים
לתיאור מצב אזי נוסיף משתנים
לתיאור "המצב הבא"
(המצב הסופי ברשת). בדוגמא:
![plot:${f_{\left\{
{{S_1} \to {S_2}} \right\}}}\left\{ {{v_1},{v_2},{v_1}^\prime ,{v_2}^\prime }
\right\} = \underbrace {\neg {v_1} \wedge \neg {v_2}}_{{S_1}} \wedge
\underbrace {{v_1}^\prime \wedge
{v_2}^\prime }_{{S_2}}$](/documentResources/326/plot_1476.png)
ונוכל אף לייצג את כל הרלציה:
![plot:\[{f_R}\left(
{{v_1},{v_2},{v_1}^\prime ,{v_2}^\prime } \right) = \left( {\neg {v_1} \wedge
\neg {v_2} \wedge {v_1}^\prime \wedge
{v_2}^\prime } \right) \vee \left( {\neg {v_1} \wedge \neg {v_2} \wedge \neg
{v_1}^\prime \wedge {v_2}^\prime }
\right) \vee \]](/documentResources/326/plot_216.png)
![plot:$\left(
{{v_1} \wedge {v_2} \wedge \neg {v_1}^\prime
\wedge {v_2}^\prime } \right) \vee \left( {\neg {v_1} \wedge {v_2}
\wedge \neg {v_1}^\prime \wedge \neg
{v_2}^\prime } \right)$](/documentResources/326/plot_1477.png)
הערה: כל השמה שמספקת את
מספקת בדיוק אחת מהפסוקיות שבה.