"Analyzing the One Dimensional Ising Model by Probabilistic Model Checking" （関澤俊弦氏）
物理ではシミュレーションはもはや不可欠な道具だが、シミュレーションに関して
- 定量的な議論はできるが、定性的な議論はできない
- モデルの妥当性を問うことが難しい（シミュレーションが変な数字を出してきて初めて前提のおかしさに気づく）
という問題がある。というわけで、モデル検査法によって物理のシミュレーション用モデルを分析し、補完として役立てようというお話。今回は磁性体に関するモデルを例に、確率遷移系を、確率モデル検査によって分析した。非常に面白い。
問題点は、モデル検査の際に計算量が跳ね上がり、現在は非常に小さなモデルしか検査できないこと。うまく抽象化してケースの数を減らす必要があるが、下手な抽象化はモデルの性質を破壊する恐れがあり、悩ましい問題のようだ。
