形式手法特論：Hyperproperty とモデル検査 #kernelvm / Kernel VM Study Tokyo 19th

Kernel/VM 探検隊@東京 No.19 で使用したスライドです。

Transcript

1. #kernelvm チェシャ猫 (@y_taka_23) Kernel/VM 探検隊@東京 No.19 (22nd Aug. 2026) 形式手法特論 Hyperproperty と モデル検査
2. 夏休みといえば冪集合
3. 例：押しボタン式信号機
4. 押しボタン式信号機の状態空間 • 色は赤 R と青 G、押しボタン P を持つ • 系の状態としては 2 × 2 で 4 通り ◦ (R, -)：信号は赤、ボタンは押されていない ◦ (R, P)：信号は赤、ボタンは押されている ◦ (G, -)：信号は青、ボタンは押されていない ◦ (G, P)：信号は青、ボタンは押されている
5. (R, -) (G, -) (R, P) (G, P)
6. 単に状態を 無作為に並べた列 … (R, -) (R, P) (R, -) (R, -) (G, -) … (R, -) (G, -) (G, P) (R, P) (G, -) … (R, -) (R, P) (R, P) (R, P) (G, -) … (R, -) (R, -) (R, P) (G, -) (G, -)
7. 単に状態を 無作為に並べた列 状態遷移図で 発生し得る列 … (R, -) (R, P) (R, -) (R, -) (G, -) … (R, -) (G, -) (G, P) (R, P) (G, -) … (R, -) (R, P) (R, P) (R, P) (G, -) … (R, -) (R, -) (R, P) (G, -) (G, -)
8. 仕様：青の間はボタンが反応しない
9. システムの安全性 • Safety（安全性） ◦ 違反する場合、ある有限 Prefix まで見れば違反が確定 • 例：「青の間はボタンが反応しない」は Safety ◦ どこかで (G, P) が現れた時点で違反が確定 • 例「赤の後いつか青になる」は Safety ではない ◦ 赤が 100 回続いても、101 回目が青の可能性が残る
10. 単に状態を 無作為に並べた列 状態遷移図で 発生し得る列 … (R, -) (R, P) (R, -) (R, -) (G, -) … (R, -) (G, -) (G, P) (R, P) (G, -) … (R, -) (R, P) (R, P) (R, P) (G, -) … (R, -) (R, -) (R, P) (G, -) (G, -)
11. 単に状態を 無作為に並べた列 状態遷移図で 発生し得る列 … (R, -) (R, P) (R, -) (R, -) (G, -) … (R, -) (G, -) (G, P) (R, P) (G, -) 仕様を満たす列 … (R, -) (R, P) (R, P) (R, P) (G, -) … (R, -) (R, -) (R, P) (G, -) (G, -)
12. 単に状態を 無作為に並べた列 状態遷移図で 発生し得る列 仕様違反確定 … (R, -) (R, P) (R, -) (R, -) (G, -) … (R, -) (G, -) (G, P) (R, P) (G, -) 仕様を満たす列 … (R, -) (R, P) (R, P) (R, P) (G, -) … (R, -) (R, -) (R, P) (G, -) (G, -)
13. Trace と Property • Trace：状態の（無限）列 • Property：Trace の集合 ◦ t ∈ P は「t に対して P が成り立つ」を意味する • Plotkin 位相 ◦ 共通 Prefix が長い Trace 同士は「近い」とみなす ◦ Safety は Plotkin 位相における閉集合に相当
14. 仕様：ボタンを早く押せば 青になるのも早い
15. 複数の Trace の比較が必要
16. Hyperproperties M.R. Clarkson, F.B. Schneider (JCS 2010) https://doi.org/10.3233/JCS-2009-0393
17. Hyperproperty • 通常の Property ◦ Trace の集合 ◦ 一本の Traceに対して性質を記述（t ∈ P かどうか） • Hyperproperty ◦ Trace の集合の集合 ◦ Trace の集合（複数本の関係）に対して性質を記述
18. Hyperproperty の世界における Safety の対応物は何であるべきか？
19. Vietoris 位相 • 位相空間 X に対し、その冪集合 P(X) に位相を入れたい • X の開集合 U に対し、自然な P(X) の準開基の構成ふたつ • Lower Vietoris 位相 ◦ {A ⊆ X : A ∩ U ≠ ∅}（U と交わる集合の全体） • Upper Vietoris 位相 ◦ {A ⊆ X : A ⊆ U}（U に含まれる集合の全体）
20. それぞれの位相における閉集合 • Plotkin 位相の閉集合（元々の Safety） ◦ ある有限 Prefix が生じ得ると分かれば違反 • Lower Vietoris 位相の閉集合 ◦ ある有限本の有限 Prefix が生じ得ると分かれば違反 • Upper Vietoris 位相の閉集合 ◦ 特定の有限 Prefix 以外が生じ得ないと分かれば違反
21. Lower Vietoris 位相の方が 元の Safety を上手く拡張している
22. ふたつの Trace を比較したいなら 信号機を 2 個組にすれば良いのでは？
23. k-Safety • 高々 k 本の有限 Prefix が生じれば違反が確定 • 例：「ボタンを早く押せば、青になるのも早い」 は以下の 2 本の Prefix で違反確定なので 2-Safety … (R, -) (R, P) (R, P) (R, P) (G, -) … (R, -) (R, -) (R, P) (G, -) (G, -)
24. k-Safety のモデル検査 定理（Clarkson-Schneider, 2010, Theorem 2） k-Safety のモデル検査は、元の状態遷移系を k 個複製して 同期積を取った状態遷移系に対する、 Hyper でない従来の Safety のモデル検査に帰着できる
25. 本日のまとめ • Property：Trace がなす集合 • Safety：Plotkin 位相における閉集合 ◦ 有限 Prefix を見れば違反が確定 • Hyperproperty：Trace がなす集合の集合 • Hypersafety：Lower Vietoris 位相における閉集合 ◦ 有限本の有限 Prefix を見れば違反が確定
26. Check Hypersafeties for Hyper-safe systems! Presented By チェシャ猫 (@y_taka_23)