抄録

樋口昌宏・◎稲森啓太（近畿大）

混合型時間アンビアント計算とは、動的な階層構造を持つシステムを形式的に記述することができるアンビアント計算を時間拡張した言語であり、物流システムの持つ階層構造を簡潔に表現することができる。この混合型時間アンビアント計算によって記述された物流記述式が所期の目的を満たしているかを確認するためには、その物流記述式に対してCTLモデル検査を行う必要がある。しかし、CTLモデル検査で用いられる通常の様相論理だけでは、動的な階層構造の変化や時間的制約などの混合型時間アンビアント計算特有の性質を表現することができない。本発表では、これらの性質を表現するために新たに提案した混合型時間アンビアント計算論理、及び本研究で開発した、任意の物流記述式に対してCTLモデル検査を行うプログラムについて述べる。