モデル検証

輪講でした。突っ込みどこ多すぎ。
というか、先生に議題を投げて、先生が講義って形に近かった。
うーむ。しかし、さすが教授というだけあって、一人で悩んでて、全然わかんなかったのが結構なペースで理解できました。
が、ゼミとしてはすごく遅いペースに。
早い人は３０分くらいで終わってしまうのに、１時間近くやったのにまだ半分。残り半分は来週に持ち越しになってしまいました。
改良しないとなぁ。

jusはSAT solverのお話。
で、自分はLTL（線形時間時相論理Linear-time temporal logic）のお話。
LTLには¬、∧、∨、→、以外に
X、F、G、U、R、Wというものを使います。
Xφは次の状態のときφがある。
Fφは将来φがある可能性がある。
Gφは将来常にφがある場合。
φUψはψまではφが成り立ち、ψはかならず起きること。
φWψはψまではφが成り立ち、ψはかならず起きるとは限らない。
で、問題はR。一応¬（¬φU¬ψ）とかけます。
頑張って解読してくださいな。

なんか、全体的に分かってないことが分かった今日この頃でした。
気合が足りないのかしら・・・。