PowerPoint Presentation様相論理と時相論理 Kripke構造 • K = 〈S, R, L〉 S: 状態の集合（無限かもしれない） R: 状態間の遷移関係 R ⊆ S×S L: 状態から命題記号の集合への写像 L(s) は、状態 s∈S において成り立つ 命題記号の集合を与える。 Kripke構造 • K = 〈S, R, L〉 • G = 〈S, R〉 有向グラフ Kripke構造 • K = 〈S, R, L〉 • L : S→2Atom Atom : 命題記号の 全体 P Q Q Q P, Q P Atom = {P, Q} 様々なKripke構造 • 木 • 森 • 無限木 P Q Q Q P, Q Q P Q P,Q 様相論理式 ϕ, ψ ::= P 命題記号 | ¬ϕ 否定 | ϕ∧ψ 連言 | ϕ∨ψ 選言 | □ϕ 必然 | ◇ϕ 可能 意味論 s |= P iff P ∈ L(s) s |= ¬
