形式検証とは、システムの正しさを数理的に保証するための手法である。
本講演では、形式検証の中でも特にモデル検査に焦点を当て、圏論的・束論的な
不動点理論に基づく枠組みを紹介する。自己関手の余代数を用いることで、
遷移システムやマルコフ決定過程など多様なシステムを表すことができ、
不動点で意味を表すことができる。この不動点の性質を用いた様々な検証手法が
存在する。特に、システムと仕様の積をとって検証問題を効率的に解く
Product Constructionという手法に注目し、確率的システムとオートマトンの
合成による、仕様を満たす確率の計算問題を取り上げる。そのうえで、
マルコフ連鎖と非決定性有限オートマトンの合成が実現不可能であることを
自然変換の特徴づけを用いて示す。

16:15- tea