| Project/Area Number |
21K11756
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60010:Theory of informatics-related
|
|---|
| Research Institution | Nagasaki University |
|---|
Principal Investigator |
伊藤 宗平 長崎大学, 情報データ科学部, 准教授 (50708005)
|
|---|
| Project Period (FY) |
2021-04-01 – 2025-03-31
|
| Project Status |
Granted (Fiscal Year 2023)
|
| Budget Amount *help |
¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000)
Fiscal Year 2024: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2023: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2022: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2021: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
|
|---|
| Keywords | プロセスマイニング / 形式手法 / 時間オートマトン / 適合性検査 / ハイブリッドシステム / 数理論理学 / モデル検査 / 機械学習 |
|---|
| Outline of Research at the Start |
企業におけるビジネスプロセスに誤りがないことを確認することはビジネスプロセスマネジメントにおける重要な関心事である。この問題に対する有望な解決策として形式手法による検証が注目を集めているが、その研究においては、主にビジネスプロセスをモデル化するための言語から形式手法で用いられる形式言語への変換法や、特定の性質の検証に特化した形式言語の考案に重点が置かれており、実際の企業内のビジネスプロセスの検証の方法論に関する研究はほぼない。そこで本研究では、既存のプロセスの実行履歴から検証可能な形式モデルを作成する手法を開発し、実際に運用されているプロセスの検証を可能とする技術を確立する。
|
| Outline of Annual Research Achievements |
本研究では、業務工程（ビジネスプロセス）の正しさを数理的に保証するための検証フレームワークの構築を目的としている。そのためには検証対象となる業務を数理的にモデル化したプロセスモデルが必要となる。実際の業務からプロセスモデルを発見・生成するための手法にプロセスマイニングというデータマイニング手法が考案されている。プロセスマイニングは業務の実行記録（イベントログ）を分析することでそのプロセスに関する知識を発見するもので、代表的な事例としてはプロセスモデルの発見、組織構造に関する発見、プロセスモデルと実際の実行記録が整合しているかの検査などがある。プロセスモデルの発見に関する従来の手法では個々の単位業務（アクティビティ）の順序関係のみを用いてモデルを発見するため、必然的にそのモデルはアクティビティの実行順番のみを表すものであった。本研究では、アクティビティの順序のみならず、そのアクティビティが実行されるための条件や、アクティビティが実行された結果企業の資源がどのように変化するかといった詳細な情報を含むモデルを発見することを目的としている。
今年度においては、昨年度の研究を発展させ、業務工程の時間オートマトンによるモデルに対し、実際のイベントの実行記録（イベントログ）との差異を評価する、適合性検査手法を効率化に取り組み、ツールとして実装した。また、現実的な規模のモデルとログに対する評価実験を行った。さらに、サイバーフィジカルシステムの制御プロセスの形式的検証にも取り組み、ケーススタディとしてモータ駆動のロボットカーのモデル化と検証を行った。また、プロセス検証の基礎理論として検証に適した論理の表現力と決定可能性について明らかにした。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究では時間オートマトンによるプロセスモデルにおいて、昨年度開発した時間付きのイベント列と時間オートマトンモデルとの間の適合度の評価手法の改良に取り組んだ。具体的には、イベント列が、モデルが実行すべきアクティビティをスキップしている場合に、モデル上ではスキップされたアクティビティが分岐の内部に含まれており、どちらの実行をスキップしたと判断すべきかにおいて、イベントに記録されているタイムスタンプを用い、そのタイムスタンプがモデルが規定する制約をよりよく満たしている方を選択するという手法を実装した。これにより、より良い適合度を得ることができるようになったのみでなく、適合度の計算コストも削減することに成功した。
サイバーフィジカルシステムの制御プロセスについて、PIDによるロボットカーの速度制御装置のモデル化をハイブリッドシステムにより行った。さらに、このシステムに対する外乱として路面の勾配を確率的パラメータとして与え、確率的なハイブリッドシステムとしてモデル化し、安全性がどの程度の確率で満たされるかを検証した。さらに、安全性に違反する確率を最小化するための適切なゲインを確率的手法により推定し、実機で用いられているゲインとの比較のために計算機実験を行い、パフォーマンス指標の差も含めて評価した。
プロセス検証のための論理として、メモリの性質について記述できる分離論理の表現力について研究を行い、直観的な points-to 演算のみの分離論理フラグメントにプレスバーガー算術（加法のみの算術）を追加した場合に、論理式の妥当性を判定する問題が決定不能になることを明らかにした。また、一階述語論理にプレスバーガー算術とリストのシグネチャを追加した論理において、その標準的な意味論における論理式の真偽判定問題が決定可能であることを明らかにした。
|
| Strategy for Future Research Activity |
時間オートマトンによるプロセスモデルの適合性検査においては、昨年度ではモデルとイベント列の間の適合度のみ考慮していたが、今年度はモデルとログ全体（複数のイベント列から成る）に対する適合度を定義し、その評価方法を実装した。これを用いてモデルとログとの間の適合度の検査をいくつかの例を用いて実験し、有用性を確認した。また、現実規模のモデルとログに対しても実験を行ったが、計算論的困難性のため現実的な時間での評価が困難であることが判明した。今後はこの改善手法について検討を行う。
サイバーフィジカルシステムの制御プロセスモデル化と検証においては、外乱として考えているのは路面の勾配のみであったが、他の外乱、例えば車輪の空転についてモデル化し、安全性の検証を行う。
プロセス検証のための論理に関しては、プレスバーガー算術を含む分離論理が決定不能であることを明らかにしたが、その正確な計算複雑性について明らかにすることが考えられる。また、プレスバーガー算術とリストを含む一階述語論理においては、現時点では証明のスケッチのみを与えているため、正確な証明を与えること、またそのユースケースについて明らかにすることが考えられる。
|
