Title

不動点を用いたモデル検査とProduct Constructionの不可能性定理
(Model checking via fixed points and no-go theorem for product construction)

Date

2025年4月30日（水）　16:45〜17:45
（16:15より数理研 2 階コモンルームでtea)　

Place

京都大学数理解析研究所 (RIMS) 110号室
(Rm110, Research Institute for Mathematical Sciences, Kyoto University)

Speaker

郡 茉友子 (Mayuko Kori)氏 （京大・数理研）

Abstract

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