1 \documentclass{article
}
7 \usepackage[all
]{xypic
}
9 \newcommand{\ra}{\rightarrow}
10 \newcommand{\un}{\text{ \textsf{U
} }}
11 \newcommand{\ev}{\lozenge}
12 \newcommand{\al}{\square}
13 \newcommand{\nx}{\bigcirc}
15 \everymath{\displaystyle}
19 \title{Model Checking Excercises
2}
26 $TS
\nvDash\varphi_1$ & $s_1
\ra \overline{s_3
\ra s_4
}$\\
27 $TS
\vDash\varphi_2$ & Yes, all loops go via $s_2,s_3$ or $s_5$
29 $TS
\vDash\varphi_3$ & Yes, $
\nx\neg c$ is only true when the next
31 & From $s_4$ you can only go to a state where $c$ holds.\\
32 $TS
\nvDash\varphi_4$ & $s_2
\ra\ldots$\\
33 $TS
\vDash\varphi_5$ & Yes, starting in $s_1$ $b
\vee c$ holds after
34 the first transition\\
35 & Starting in $s_2$ $b
\vee c$ holds immediatly.\\
36 $TS
\vDash\varphi_6$ & $s_1
\ra\overline{s_4
\ra s_2
}$
42 *+
[F
]{s_0
}\ar@/^/
[r
]^
{\neg a
}\ar@(d,l)^
{a
} &
43 *+
[F
]{s_1
}\ar@/^/
[l
]^
{\neg b
}\ar[r
]^
{b
} &
44 *+
[Fo
]{s_2
}\ar@(d,r)_
{true
}
51 *+
[Fo
]{s_0
}\ar@(d,l)^
{true
}\ar[r
]^
{a
} &
52 *+
[F
]{s_1
}\ar@(d,l)^
{true
}\\
53 \ar[r
] & *+
[F
]{s_2
}\ar@(d,l)^
{\emptyset}\ar[r
]^
{a
\vee b
} &
54 *+
[Fo
]{s_3
}\ar@(d,l)^
{true
}
61 *+
[Fo
]{s_0
}\ar[r
]^
{\neg a
}\ar[d
]_
{a
} &
62 *+
[F
]{s_1
}\ar@(d,r)_
{true
}\\
63 & *+
[Fo
]{s_2
}\ar@(d,l)^
{true
}
67 $
\ev\al(a
\wedge\ev b)$