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