概要

講演者：池田 光優（大阪大学）

題目：MTL formulaで定められた性質を連続時間確率過程が満たす確率について

概要：近年、ソフトウェアやハードウェアのデザインが複雑になるにつれ、それらのシステムの検証にコストが割かれるようになった。モデル検査とは、システムが取りうる状態やシステムの安全性を、グラフ理論やマルコフ過程、様相論理などを用いて記述し、検証する方法である。本研究では、連続時間確率過程によって記述されたシステムが、MTLと呼ばれる時相様相論理によって定義された性質を満たす確率について調べる。MTLは、確率過程の見本経路と時刻に関して自然に与えられる。しかし、様相論理によって定義された事象の可測性すら自明ではない。したがって、まず事象の可測性から議論を行い、次にブラウン運動のような標準的な確率過程が様相論理によって定められた性質を満たす確率を調べる。

なお、本研究は名古屋大学の木原貴行氏と産業技術総合研究所の山形頼之氏との共同研究である。