研究課題
線形時相論理（LTL）で表現可能な代表的な性質のクラス（lead-to性、eventual性、条件付安定性、until性、until安定性）に対し、各初期状態から構築される無限木を複数の層に分割し、複数の部分空間ごとに独立にモデル検査することでもとの状態空間に対するモデル検査と同等のモデル検査結果を得ることのできる技術を考案すると共に正当性を証明した。部分空間ごとに独立に行えるモデル検査を同時に行うことで並列モデル検査を可能とする。モデル検査におけるもっともやっかいな状態空間爆発を緩和可能であると共にモデル検査にとって重要な実行速度の改善に貢献することができる。until性とuntil安定性を除き、逐次版と並列版の支援ツールを作成した。支援ツールの作成にはMaudeを用いた。支援ツールの実装において、部分空間のモデル検査においてすべての反例をひとつずつ探すことが実行面におけるボトルネックになっていたため、Tarjanの提案した、強連結要素を探すアルゴリズム用いて一度にすべての反例を探すことの出来るモデル検査器を、MaudeのLTLモデル検査器で使われているソフトウェアコンポネントを再利用するとで作成し、支援ツールで利用することにした。これによりそのボトルネックを解消することができた。提案方法では、上述した無限木をどのような層に分割するのか（レイヤーコンフィグレーション）がモデル検査の性能に大きく影響する。そこで、より良いレイヤーコンフィグレーションを探すことを支援するツールを作成した。事例実験により効果を確認することができた。提案方法は、LTLモデル検査の並列化のみならず、セキュリティプロトコル専用の解析ツールであるMaude-NPAやJavaのモデル検査器であるJava Pathfinder（JPF）の並列化にも有効であることを示した。
令和4年度が最終年度であるため、記入しない。
すべて 2022
すべて 雑誌論文 (4件) (うち査読あり 4件、 オープンアクセス 3件) 学会発表 (2件) (うち国際学会 2件)
IEEE Access
巻: 10 ページ: 133749～133765
10.1109/ACCESS.2022.3230844
巻: 10 ページ: 24955～24975
10.1109/ACCESS.2022.3155629
14th International Workshop on Rewriting Logic and Its Applications
巻: LNCS 13252 ページ: 253～273
10.1007/978-3-031-12441-9_13
34th International Conference on Software Engineering and Knowledge Engineering
巻: NA ページ: 388～393
10.18293/SEKE2022-058
