Principles of Model Checking: Lemma 3.27

Reference: Baier, Christel, and Joost-Pieter Katoen. Principles of Model Checking, MIT Press, 2008.

Lemma 3.27の証明は, もう少し見通しよくできると思う。

Def. $\text{Start}(\hat{\sigma}) := \{\sigma \in (2 ^ {AP}) ^ {\omega};\,\hat{\sigma} \in \text{pref}(\sigma)\}$ . 直感的には $\text{Start}(\sigma)$ は $\hat{\sigma}$ を prefix にもつword $\sigma$ 全体の集合である. この記法から, LT property $P$ が safety property であるという定義は,

$(\forall \sigma \in (2 ^ {AP}) ^ {\omega} \backslash P)(\exists \hat{\sigma} \in \text{pref}(\sigma))(P \cap \text{Start}(\hat{\sigma}) = \emptyset)$

とかける. また, 定義より

$\sigma \in \text{Start}(\hat{\sigma}) \iff \hat{\sigma} \in \text{pref}(\sigma)$ .

Lemma. $P \cap \text{Start}(\hat{\sigma}) \neq \emptyset \iff (\exists \sigma \in P)(\hat{\sigma} \in \text{pref}(\sigma) )$ .

証明（左辺） $\iff$ $(\exists \sigma)(\sigma \in P \cap \text{Start}(\hat{\sigma}))$ $\iff$ $(\exists \sigma)(\sigma \in P \land \sigma \in \text{Start}(\hat{\sigma}))$ $\iff$ $(\exists \sigma)(\sigma \in P \land \hat{\sigma} \in \text{pref}(\sigma))$ $\iff$ （右辺）. 終

$\text{closure}(P) = \{\sigma \in (2 ^ {AP}) ^ \omega;\,\text{pref}(\sigma) \subseteq \text{pref}(P)\}$ を $\text{cl}(P)$ と略記する. なお, ここに $\text{pref}(P) = \bigcup _ {\sigma \in P} \text{pref}(\sigma)$ .

Lemma 3.27. $P$ is a safety property $\iff \text{cl}(P)=P$ .

証明 $P \subseteq \text{cl}(P)$ は成立つから, 右辺は $\text{cl}(P) \subseteq P$ と同値である. いま, $(2 ^ {AP}) ^ \omega \backslash A$ を $A ^ {c}$ とかくことにすれば,

$P$ is safety

$\iff$ $(\forall \sigma \in P ^ {c})(\exists \hat{\sigma} \in \text{pref}(\sigma) )(P \cap \text{Start}(\hat{\sigma}) = \emptyset)$

$\iff$ $(\forall \sigma \in P ^ {c})(\exists \hat{\sigma} \in \text{pref}(\sigma) )(\forall \tilde{\sigma} \in P)(\hat{\sigma} \notin \text{pref}(\tilde{\sigma}) )$

$\iff$ $(\forall \sigma \in P ^ {c})(\exists \hat{\sigma} \in \text{pref}(\sigma) )\left( \hat{\sigma} \notin \bigcup _ {\tilde{\sigma} \in P} {\text{pref}(\tilde{\sigma})} \right)$