特許ウォッチ

公開番号2025100131
公報種別公開特許公報(A)
公開日2025-07-03
出願番号2023217272
出願日2023-12-22
発明の名称モデル検査装置、モデル検査方法及びプログラム
出願人大学共同利用機関法人情報・システム研究機構,国立大学法人東北大学
代理人個人,個人
主分類G06F 11/36 20060101AFI20250626BHJP(計算;計数)
要約【課題】内部構成が未知のコンポーネントを含むモデルに対するモデル検査を実行する。
【解決手段】モデル検査装置が、複数のコンポーネントの間を状態遷移する状態遷移モデルを取得するモデル取得部と、コンポーネントについて予め定めた部分特徴量を取得する部分特徴量取得部と、コンポーネントごとの部分特徴量に基づいて状態遷移モデルの全体特徴量を計算する全体特徴量計算部と、全体特徴量に基づいて状態遷移モデルを検査する検査実行部と、を備える。
【選択図】図9
特許請求の範囲【請求項１】
複数のコンポーネントの間を状態遷移する状態遷移モデルを取得するように構成されているモデル取得部と、
前記コンポーネントについて予め定めた部分特徴量を取得するように構成されている部分特徴量取得部と、
前記コンポーネントごとの前記部分特徴量に基づいて前記状態遷移モデルの全体特徴量を計算するように構成されている全体特徴量計算部と、
前記全体特徴量に基づいて前記状態遷移モデルを検査するように構成されている検査実行部と、
を備えるモデル検査装置。
続きを表示（約 1,000 文字）【請求項２】
請求項１に記載のモデル検査装置であって、
前記部分特徴量取得部は、内部構成が未知の前記コンポーネントについて前記部分特徴量を取得するように構成されている、
モデル検査装置。
【請求項３】
請求項２に記載のモデル検査装置であって、
内部構成が既知の前記コンポーネントについて前記部分特徴量を計算するように構成されている部分特徴量計算部をさらに含む、
モデル検査装置。
【請求項４】
請求項１から３のいずれかに記載のモデル検査装置であって、
前記状態遷移モデルは、定量的指標を計算する定量的状態遷移モデルである、
モデル検査装置。
【請求項５】
請求項４に記載のモデル検査装置であって、
前記定量的指標は、遷移確率又は利得を含む、
モデル検査装置。
【請求項６】
請求項４に記載のモデル検査装置であって、
前記定量的状態遷移モデルは、マルコフ決定過程又はミーンペイオフゲームである、
モデル検査装置。
【請求項７】
請求項４に記載のモデル検査装置であって、
前記部分特徴量は、前記コンポーネントの入力から出力への到達確率及び利得の期待値を含む、
モデル検査装置。
【請求項８】
請求項７に記載のモデル検査装置であって、
前記全体特徴量は、前記状態遷移モデルの利得の期待値を含む、
モデル検査装置。
【請求項９】
コンピュータが、
複数のコンポーネントの間を状態遷移する状態遷移モデルを取得する手順と、
前記コンポーネントについて予め定めた部分特徴量を取得する手順と、
前記コンポーネントごとの前記部分特徴量に基づいて前記状態遷移モデルの全体特徴量を計算する手順と、
前記全体特徴量に基づいて前記状態遷移モデルを検査する手順と、
を実行するモデル検査方法。
【請求項１０】
コンピュータに、
複数のコンポーネントの間を状態遷移する状態遷移モデルを取得する手順と、
前記コンポーネントについて予め定めた部分特徴量を取得する手順と、
前記コンポーネントごとの前記部分特徴量に基づいて前記状態遷移モデルの全体特徴量を計算する手順と、
前記全体特徴量に基づいて前記状態遷移モデルを検査する手順と、
を実行させるためのプログラム。

発明の詳細な説明【技術分野】
【０００１】
本発明は、モデル検査装置、モデル検査方法及びプログラムに関する。
続きを表示（約 1,400 文字）【背景技術】
【０００２】
形式検証の一種であるモデル検査は、ハードウェア又はソフトウェアの設計から導出されたモデルが形式仕様を満足するかどうかを網羅的な全数探索により検証する手法である。モデル検査は、自動検証技術として注目されており、様々なモデル検査手法が提案されている。
【０００３】
例えば、非特許文献１には、確率的モデル検査の状態空間爆発問題を解決するために、コンポーネントを階層化した構造をもつマルコフ決定過程を分割統治方式で処理する要素還元的分割統治アルゴリズムが開示されている。
【先行技術文献】
【非特許文献】
【０００４】
Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, and Ichiro Hasuo, "Compositional Probabilistic Model Checking with String Diagrams of MDPs", CAV 2023, pp 40-61, 2023.
【発明の概要】
【発明が解決しようとする課題】
【０００５】
しかしながら、従来技術では、検査対象とするモデルに内部構成が未知のコンポーネントが含まれることを想定していない。
【０００６】
本発明の一態様は、上記のような技術的課題に鑑みて、内部構成が未知のコンポーネントを含むモデルに対するモデル検査を実行することを目的とする。
【課題を解決するための手段】
【０００７】
上記の課題を解決するために、本発明の一態様によるモデル検査装置は、複数のコンポーネントの間を状態遷移する状態遷移モデルを取得するモデル取得部と、コンポーネントについて予め定めた部分特徴量を取得する部分特徴量取得部と、コンポーネントごとの部分特徴量に基づいて状態遷移モデルの全体特徴量を計算する全体特徴量計算部と、全体特徴量に基づいて状態遷移モデルを検査する検査実行部と、を備える。
【発明の効果】
【０００８】
本発明の一態様によれば、内部構成が未知のコンポーネントを含むモデルに対するモデル検査を実行することができる。
【図面の簡単な説明】
【０００９】
合成マルコフ決定過程の一例を示す図である。
合成マルコフ決定過程の一例を示す図である。
ホワイトボックスモデルの一例を示す図である。
ブラックボックスモデルの一例を示す図である。
数学的特徴量が既知のブラックボックスモデルの一例を示す図である。
構成性原理を説明するための図である。
モデル検査システムの全体構成の一例を示すブロック図である。
コンピュータのハードウェア構成の一例を示すブロック図である。
モデル検査システムの機能構成の一例を示すブロック図である。
モデル検査方法の一例を示すフローチャートである。
【発明を実施するための形態】
【００１０】
以下、本発明の各実施形態について添付の図面を参照しながら説明する。なお、本明細書及び図面において、実質的に同一の機能構成を有する構成要素については、同一の符号を付することにより重複した説明を省略する。
（【００１１】以降は省略されています）

関連特許