mnagakuさん「FDRによるRPGシナリオの検証」を解説

長久 勝 @mnagaku

「FDRによるRPGシナリオの検証」ですが、レポートが自宅鯖にしか置いてなかった＆今それ止まってるなので、"The verification of RPG scenario by FDR"でググってクイックビューして下さい

長久 勝 @mnagaku

今、ググってすぐ見つかる、各種発表で使ったスライド資料だと詳細は載せてないので、スライドの後に、このレポートを読んでもらえればと思います。このアプローチの要点は、RPGシナリオをプロセス代数で書くこと、それをモデル検査器で検証すること、の2点です

長久 勝 @mnagaku

FDR2は違いますが、現世代のモデル検査器は、検証内容をSATに変換してSATソルバにかけます。ここ数年、制約問題を解くのにSATソルバのアプローチが有用とされ、活発に研究開発が進んでいるため、タダメシが食えるからです

長久 勝 @mnagaku

SATソルバ良くなる->応用ツールがタダメシ食いに来る->SATソルバの注目度上がって更に研究開発が進む、みたいな感じです

長久 勝 @mnagaku

プロセス代数CSPをベースとするモデル検査器でバックエンドがSATソルバのものとしてはPAT3があります http://t.co/RdUCoO9K 初期のPATでは文法が不十分だった部分があり、移植するのがしんどそうだったのですが、今はもう大丈夫なので、いい加減やらんとなあ

長久 勝 @mnagaku

PAT3には、FDR2になかった、LTLで検証式書ける、4種のプロセス公平性を扱える、といった機能があり、より普通のモデル検査器といった趣があります。つまり、扱いやすい

長久 勝 @mnagaku

PAT3は商業利用可能なライセンスが整備される予定ですが、シンガポールで開発されていることもあり、中国も含め、アジアで使える価格体系になるという話です。これまで3桁万円切るツールは聞いたことないですが、私が聞いてる話だと、10万切ってくる可能性もあります

長久 勝 @mnagaku

あと、複数プロセスの平行合成を考慮しないADVのエンジン程度なら、それを検証するモデル検査器を自作するのは可能です。変数を同値分割でフラグ化するとか、ある程度の効率化は文献読んで実装する必要があるかもだけど

長久 勝 @mnagaku

ゲーム進行に関する部分を変えないで使い続けてるエンジン（てゆーか文法）があるなら、そのDSLをモデル表現として対応するツールを作るコストをかけても、進行バグを早期に見つけるので幸せになれるかも

長久 勝 @mnagaku

で、抽象的なモデルも、DSLも、粒度が違うだけでモデルやんとか言うと、実装に対してかけるモデル検査の話になります。最近だと、CBMCとか。Cのコードを検査します

長久 勝 @mnagaku

とゆーわけで、どこかが開発費を出してくれるなら、何がしかは作れる状況になってる感じです。実問題に合わせた調整とか、費用対効果の評価とかは、それとは別ですが

長久 勝 @mnagaku

ほんとは、社会インフラで使って、安くしてもらって、ゲームの世界にも落ちてくるというのが、良いシナリオなんですがねえ（終）