| 研究課題/領域番号 |
21K11756
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60010:情報学基礎論関連
|
|---|
| 研究機関 | 長崎大学 |
|---|
研究代表者 |
伊藤 宗平 長崎大学, 情報データ科学部, 准教授 (50708005)
|
|---|
| 研究期間 (年度) |
2021-04-01 – 2025-03-31
|
| 研究課題ステータス |
交付 (2022年度)
|
| 配分額 *注記 |
4,160千円 (直接経費: 3,200千円、間接経費: 960千円)
2024年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2023年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
2022年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
2021年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円)
|
|---|
| キーワード | プロセスマイニング / 形式手法 / モデル検査 / 機械学習 |
|---|
| 研究開始時の研究の概要 |
企業におけるビジネスプロセスに誤りがないことを確認することはビジネスプロセスマネジメントにおける重要な関心事である。この問題に対する有望な解決策として形式手法による検証が注目を集めているが、その研究においては、主にビジネスプロセスをモデル化するための言語から形式手法で用いられる形式言語への変換法や、特定の性質の検証に特化した形式言語の考案に重点が置かれており、実際の企業内のビジネスプロセスの検証の方法論に関する研究はほぼない。そこで本研究では、既存のプロセスの実行履歴から検証可能な形式モデルを作成する手法を開発し、実際に運用されているプロセスの検証を可能とする技術を確立する。
|
| 研究実績の概要 |
本研究では、業務工程（ビジネスプロセス）の正しさを数理的に保証するための検証フレームワークの構築を目的としている。そのためには検証対象となる業務を数理的にモデル化したプロセスモデルが必要となる。実際の業務からプロセスモデルを発見・生成するための手法にプロセスマイニングというデータマイニング手法が考案されている。プロセスマイニングは業務の実行記録（イベントログ）を分析することでそのプロセスに関する知識を発見するもので、代表的な事例としてはプロセスモデルの発見、組織構造に関する発見、プロセスモデルと実際の実行記録が整合しているかの検査などがある。プロセスモデルの発見に関する従来の手法では個々の単位業務（アクティビティ）の順序関係のみを用いてモデルを発見するため、必然的にそのモデルはアクティビティの実行順番のみを表すものであった。本研究では、アクティビティの順序のみならず、そのアクティビティが実行されるための条件や、アクティビティが実行された結果企業の資源がどのように変化するかといった詳細な情報を含むモデルを発見することを目的としている。
今年度においては、昨年度の検討結果を踏まえ、時間オートマトンによるプロセスモデルの発見に取り組んだ。他のプロセスマイニング手法の開発にも着手し、時間オートマトンによるプロセスモデルに対する適合度検査アルゴリズムの開発と実装を行った。また、予測的プロセスモニタリング手法の一つとして、実行途中のイベント列から、次のプロセスの完了時間を予測するモデルを構築し評価実験を行った。最後に、他のプロセスモデル表現形式についても検討し、ハイブリッドオートマトンや論理によるモデルの表現・検証についても検討した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
本研究では時間オートマトンによるプロセスモデルにおいて、分岐の発生する地点を特定し、次に起こるイベントをそのイベントが持つ属性値を用いて分類する分類器を、イベントログより学習してモデルを構築する。今年度はサポートベクタマシンを用いた分類器を構築した。線形分類をまず試みたが、良いモデルは得られなかった。一方、非線形分類においては、適切なハイパーパラメータ設定の下では十分良い精度の分類器を得ることができた。また、当初は2値分類を試みたが、さらに多値分類も一体他方式と一対一方式の二通りで試みた。どちらもほぼ同程度の正解率のモデルが得られた。
時間オートマトンによるプロセスモデルの適合度検査手法においては、時間付きのイベント列と時間オートマトンモデルとの間の適合度を数学的に定式化した。具体的には、アラインメントによるイベント列の適合度と、時間制約の適合度の2種類に分け、それらを総合した評価値を適合度とした。適合度の計算アルゴリズムについては厳密解を求める方法と近似解を求める方法の2通りを実装し、それぞれの評価を行った。
予測的プロセスモニタリングにおいては、ある時点のイベントを入力として次のイベントの完了時刻の予測を行うモデルをロジスティック回帰とニューラルネットワークにより構築し、その評価を行った。
サイバーフィジカルシステムの制御プロセスについて、PIDによる車体の速度制御装置のモデル化をハイブリッドオートマトンにより行い、装置に要求される安全性の検証をモデル検査により行った。
一般的なプロセスモデルの形式であるペトリネットについて、その検証問題について調査を行った。また、帰納的に定義される述語を含む一階述語論理による検証の可能性について検討した。さらに、その検証問題の計算複雑性について明らかにした。
|
| 今後の研究の推進方策 |
時間オートマトンによるプロセスモデルの発見においては、これまで様々な学習アルゴリズムを用いた発見を試みてきたが、ニューラルネットワークによるモデル発見はまだ試みていなかったため、深層学習を用いたニューラルネットワークモデルの発見に取り組む。また、本年度のサポートベクタマシンのモデルおよびニューラルネットワークモデルはブラックボックスモデルであるため、そのモデルから人間にとって意味のあるモデルを抽出する必要がある。
時間オートマトンによるプロセスモデルの適合度検査においては、現在のところは単独の時間オートマトンを対象としているため、これを時間オートマトンのネットワークに拡張することが考えられる。
予測的プロセスモニタリングにおいては、現在のモデルでは予測時点で用いる情報は直前のイベントの情報のみであり精度はあまり良くなかった。これを、過去の情報も用いる学習モデルを用いて学習することが考えられる。
サイバーフィジカルシステムの制御プロセスモデル化と検証においては、外乱を考慮したモデルを作成し、より現実世界に近い環境での制御プロセスのモデル化と検証を行うことが考えられる。
論理によるプロセスモデルの検証においては、循環証明体系による定理証明による検証に取り組むことが考えられる。また、今年度の計算複雑性に関する結果から、より自動推論に適した部分論理の発見が望まれることも明らかになった。
|
