普通の Web エンジニアのための様相論理入門 #yapcjapan / YAPC Hakodate 2024

YAPC::Hakodate 2024 で使用したスライドです。

本セッションでは、分散システムのような複雑な仕様や動作を持つプログラムに対して、様相論理を用いてその仕様を記述し検査する技術について解説します。

我々はシステムの仕様を保証する際、テスト設計や自動化ツールのような、仕様を「テストする」ための方法論を考えがちです。しかし、その前に仕様が「記述できる」ことが前提であり、これは決して自明ではありません。例えば、分散システムに対して「一部のサーバが落ちてもいつか回復する」といった性質なんて一体どうしたら表現できるのでしょうか？

複雑なシステムの仕様を考える上で、自然言語による曖昧性を排した「共通言語」を定義したいという動機は、古くから現在に至るまで、研究と実用が交わる大きなテーマの一つであり続けています。本セッションではこのような「共通言語」としての様相論理について、自分では手を出しづらいあなたのために、しかしできるだけ誤魔化さず解説します。

Transcript

1. 普通のWebエンジニアのための 様相論理入門 #yapcjapan チェシャ猫 (@y_taka_23) YAPC::Hakodate 2024 (5th Oct. 2024)
2. • テーマは様相論理 ◦ 特に時相論理の一種 CTL について解説 ◦ 非同期システムの「テスト」に使用可能 • 普通の Web エンジニア向け ◦ 今回の内容を押さえておけば教養としては OK ◦ 興味が有り余った人のために最後に読書案内あり 本日お話しすること
3. 非同期システムの設計 • 応援数をカウントするシステム ◦ 現在の応援数を読み込む ◦ クライアント側で +1 する ◦ 新しい値を書き込む クライアント A サーバ S null 0 0 1 1 GET PUT ++ ♪ ♥99 ♥ ♥
4. 非同期起因の不具合 • クライアントが複数いる場合、特定のタイミングで 割り込まれると両方から +1 しても結果が +2 にならない クライアント A クライアント B サーバ S null 0 null 0 0 1 1 1 1 GET PUT GET PUT ++ ++
5. 非同期システムの挙動 • 非同期性は非決定性をもたらす • 入出力の値の対応だけではなく 動作の軌跡（パス）全体がなす グラフを網羅的に考慮して 設計する必要がある A=null S=0 B=null A=0 S=0 B=null A=null S=0 B=0 A=1 S=0 B=null A=0 S=0 B=0 A=null S=0 B=1 … … …
6. ここまでのまとめ • 非同期システムは非決定性を持ちテストが難しい • 非決定的な挙動はグラフ構造として表される
7. 様相論理 Modal Logic グラフ構造上で意味論が展開される論理体系
8. 代表的な様相論理 • K 論理：最も基本となる様相論理の体系 • グラフ構造に追加条件を課す方向の拡張 ◦ Geach 論理：合流性に関する仮定を追加 • 演算子を追加して論理式の表現力を上げる方向の拡張 ◦ 時相論理：「ずっと」「いつか」など時間経過を追加 ◦ 様相 μ 計算：不動点演算子を追加 • 今回は時相論理の一種、計算木論理（CTL）を解説
9. Kripke 構造 • グラフのノード上で真偽値の概念を考える • 以下の組 K = (S, ⇝, AP, f) を Kripke 構造と呼ぶ ◦ 状態の集合：S ◦ S 上の遷移関係：⇝ ⊆ S × S ◦ 原子命題の集合：AP ◦ 付値関数：f: S × AP → {true, false}
10. • S = {s1, s2, s3} • ⇝ = {(s1, s1), (s1, s2), (s2, s1), (s2, s3), (s3, s2) (s3, s1)} • AP = {p, q} • f(s1, p) = false, f(s1, q) = false f(s2, p) = true, f(s2, q) = false f(s3, p) = true, f(s3, q) = true Kripke 構造の例 表現したいグラフ構造 ¬p ¬q ¬p q p q s1 s2 s3
11. CTL の論理式 • 原子命題 p ∈ AP は論理式 • φ と ψ が論理式なら、通常の（命題）論理演算子で 作られる ¬φ、φ ∧ ψ、φ ∨ ψ、φ → ψ も論理式 • φ が論理式なら、AX φ、AG φ、AF φ、EX φ、EG φ、 EF φ も論理式 • φ と ψ が論理式なら、A (φ U ψ)、E (φ U ψ) も論理式
12. X、G、F、U の直観的な説明 • 「状態の条件」を「パス（状態の列）の条件」に変換 ◦ X φ：パスの 2 コマ目の状態で φ が真（neXt） ◦ G φ：パスを辿るとずっと φ が真（Globally） ◦ F φ：パスを辿るといつか一度は φ が真（Future） ◦ φ U ψ：パスを辿るといつか一度は ψ が真になり、 かつそれまではずっと φ が真（Until）
13. A、E の直観的な説明 • 「パス（状態の列）の条件」を「状態の条件」に変換 ◦ A α：その状態から出発する任意のパスで 条件 α が真となる（All） ◦ E α：その状態から出発するパスのうち最低一つで 条件 α が真となる（Exists）
14. 演算子の組み合わせ • CTL では必ず「A、E」+「X、G、F、U」の組で使用 ◦ つまり CTL 論理式は常に「状態の条件」 • 実は E + X、E + G、E + U があれば残りは代用可能 ◦ 例えば AF φ の代わりに ¬EG (¬φ) で表現可能 ◦ De Morgan の法則に類似 φ φ s において AF φ は真、EG φ は偽 φ φ s
15. CTL の意味論 K, s ⊨ φ（Kripke 構造 K の s ∈ S で φ が真）を定義 • K, s0 ⊨ EX φ ⇔ あるパス s0 ⇝ s1 ⇝ … が存在し K, s1 ⊨ φ • K, s0 ⊨ EG φ ⇔ あるパス s0 ⇝ s1 ⇝ … が存在し、 任意の i に対して K, si ⊨ φ • K, s0 ⊨ E (φ U ψ) ⇔ あるパス s0 ⇝ s1 ⇝ … が存在し、 ある i に対し K, si ⊨ φ、かつ任意の j < i に対し K, sj ⊨ ψ
16. CTL による厳密な仕様の表現 • 仕様書「故障した場合であっても復旧できる」 ◦ 自然言語による表現には曖昧性がある • AG (crash → EF recover) ◦ 故障後、なんとかして結果的に復旧するルートが存在 • AG (crash → AF recover) ◦ 故障後、どのルートで遷移しても結果的に必ず復旧
17. CTL 以外の時相論理 • LTL（線形時相論理） ◦ G（◻ で表す）と F（◇ で表す）のみ使用できる ◦ CTL では不可能な ◻ (◇ φ) のような式が表現可能 • CTL* ◦ 演算子を自由な順序で組み合わせられる ◦ CTL や LTL の上位互換
18. ここまでのまとめ • 非同期システムは非決定性を持ちテストが難しい • 非決定的な挙動はグラフ構造として表される • 様相論理ではグラフ（Kripke 構造）上での真偽を定義 • CTL では、時間経過に関する仕様が記述できる
19. モデル検査 • システムを Kripke 構造 K、仕様を CTL 論理式 φ で表現 • モデル検査器に入力して K, 初期状態 ⊨ φ かどうかを検査 • いわば CTL を「テストフレームワーク」として使用 モデル検査のワークフロー モデル検査器 「K, init ⊨ φ か？」 システム設計 要求仕様 真：OK K, init φ 偽：再設計 表現 入力 出力
20. EX φ、E (φ U ψ) の検査アルゴリズム • EX φ は単純に s の次の状態で φ が真かどうか確認 • E (φ U ψ) は ψ が真になる状態から遷移を後ろ向きに φ が真になる範囲で辿って、出発点 s まで戻れるか確認 φ φ M, s ⊨ EX φ の検査 φ φ M, s ⊨ E (φ U ψ) の検査 φ ψ φ s s
21. EG φ の検査アルゴリズム（1/3） • EG φ は「無限に真が続くパス」という条件なので、 愚直に計算しようとしてもアルゴリズムが停止しない • まず φ が真になる強連結成分を Kosaraju-Sharir や Tarjan の アルゴリズムで計算しておく （どの二つの状態も双方向に到達可能） φ が真になる強連結成分 φ φ φ φ φ φ φ φ s
22. EG φ の検査アルゴリズム（2/3） • 後は E (φ U ψ) の場合と同じように、強連結成分から φ が成り立つ範囲で後ろ向きに辿って確認 • 結果、まず φ が真の状態のみを 辿って強連結成分まで到着後、 強連結成分内でループすることで ずっと φ が真となる無限パスを得る φ φ M, s ⊨ EG φ の検査 φ φ φ φ φ φ s
23. EG φ の検査アルゴリズム（3/3） • このパターン以外にも条件を満たすパスがあるのでは？ • Kripke 構造の状態 S が有限集合なら他には無い • ノードが有限個しか無いので「無限パス」と言っても 実際にはどこかで既出の 状態が現れてループに入る φ φ φ 「ずっと φ が真」を満たすパス φ … … φ φ = s
24. 計算可能性と有限モデル性 • CTL 以外でも、様相論理式の真偽を判定するためには、 Kripke 構造 K の状態数が有限であることが効いてくる • 様相論理の中でも有限モデル性を持つ体系は扱いやすい ◦ 論理式 φ がある Kripke 構造 K で K, s ⊨ φ ならば、 特に状態数が有限な Kripke 構造 K’ が存在し K’, s’ ⊨ φ • 有限モデルを得る方法として濾過法が知られている
25. 濾過法のアイデア • 論理式 φ の部分式全体からなる集合を Sub(φ) と表す • 状態集合 S 上の同値関係 ∼ を以下で定義する ◦ s1 ∼ s2 ⇔ 任意の ψ ∈ Sub(φ) に対して K, s1 ⊨ ψ の真偽と K, s2 ⊨ ψ の真偽が一致 • 商集合 S/∼ を新しい状態集合とする • ψ たちの真偽によって区別可能な同値類は有限個しかない
26. 本日のまとめ • 非同期システムは非決定性を持ちテストが難しい • 非決定的な挙動はグラフ構造として表される • 様相論理ではグラフ（Kripke 構造）上での真偽を定義 • CTL では、時間経過に関する仕様が記述できる • CTL では、無限のパスに関する条件であっても、 グラフアルゴリズムを用いて有限時間で検査が可能
27. 読書案内 • 鹿島亮『コンピュータサイエンスにおける様相論理』 • 菊池誠（編）『数学における証明と真理』 • チェシャ猫『モデル検査器をつくる』（技術書典）
28. Test Distributed Systems by Modal Logics! Presented By チェシャ猫 (@y_taka_23)