Kripke Structureとfixedpoint

研究 基礎理論

最近Kripke Structureにはまっている。

原子命題AP上のKripke Structure Mとは４タプルである。
$M=(S,S_0,R,L)$

  • $S$は有限の状態の集合
  • $S_0 \subseteq S$は初期状態の集合
  • $R \subseteq S \times S$は全象の遷移関係
  • $L:S \rightarrow 2^{AP}$は個々の状態で成立する命題の集合への写像関数

これは、Reactive Systemの基本モデル言語ともされるし、特に時相論理の基盤となっている。
ところが、$P(S)$をSの部分集合の集合とすると、$P(S)$は束(Lattice)を構成する
ということなのだ。束ということで順序関係があるわけですが、ここでは集合の包含関係が順序になる。

さらに、\tau : P(S)\rightarrow P(S)という述語変換を考えると、集合演算にて
monotonicな性質や、連続の性質が定義される。

  • "$P \subseteq Q$なら$\tau(P) \subseteq \tau(Q)$"ならばmonotonic
  • "$P_1 \subseteq P_2 \subseteq ...$なら$\tau(\cup_i P_i) = \cup_i \tau(P_i)$"ならば$\cup$連続
  • "$P_1 \supseteq P_2 \supseteq ...$なら$\tau(\cap_i P_i) = \cap_i \tau(P_i)$"ならば$\cap$連続

とな。さらにmonotonicならばleast fixedpointとgreatest fixed pointが存在し

  • least fixedpoint: $\mu Z.\tau(Z)=\cap\{Z|\tau(Z) \subseteq Z\}$
  • greatest fixedponit:$\nu Z.\tau(Z)=\cup\{Z|\tau(Z) \supseteq Z\}$

さらに連続ならば

  • \mu.\tau(Z)=\cup_i\tau^i(False)
  • \nu.\tau(Z)=\cap_i\tau^i(True)

とつづくわけなんですが。どうもこれが位相構造でいうと何になる？だろうか？
上界？下界

上界の集合の最小元（最小の上限）を上限(least upper bound)$sup(A)$とよぶし、下界の集合の最大元を下限$inf(A)$と呼ぶのと呼応するんだろうなあ？と森先生の位相のこころ (ちくま学芸文庫)をちょうど通勤読してるので、気になったのさ。

いや違うぞ、Falseから\tauを連続適用した集合の上限がleast fixedpointで、逆、つまり
Trueから\tauを連続適用した集合の下限がgreatest fixedpointになるということだ。あぶないあぶない。

上限なのにleast,下限なのにgreatestというのが今一歩理解を阻む。