• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

2021 Fiscal Year Research-status Report

Discovering formal business process models by process mining

Research Project

Project/Area Number 21K11756
Research InstitutionNagasaki University

Principal Investigator

伊藤 宗平  長崎大学, 情報データ科学部, 准教授 (50708005)

Project Period (FY) 2021-04-01 – 2025-03-31
Keywordsプロセスマイニング / 形式手法 / モデル検査 / 機械学習
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

時間オートマトンによるプロセスモデルの発見手法において、従来のプロセスマイニング手法によりアクティビティの順序を表す有限オートマトンモデルを発見し、そのモデル上での分岐点に対応するイベントの属性値に関する情報をイベントログから抽出し、次に生じるアクティビティを予測するモデルを機械学習により学習する手法を考案した。この手法では分岐先のアクティビティ名を目的変数、その時点のイベントログが含む属性値を目的変数とした分類問題として定式化した。実際に決定木学習、ロジスティック回帰分析を用いて学習を試みた。さらに、目的変数を次の時点のアクティビティ名とするのではなく、特定の属性値として、その属性値に関する不等式で分岐条件を発見する間接的な分類アプローチも試みた。ここでは重回帰分析を行い2つのクラスに分類することを試みたが、一方のクラスは高精度に分類することができたものの、他方のクラスへの分類は精度が低く、改良の余地があることが分かった。
時間オートマトンをプロセスモデルとしたときに、属性値を考慮した適合性検査手法についてもプロトタイプとなる手法を考案した。ここでは遷移条件として a<x<b の形の不等式を考え、変数 x の値が範囲外であるにもかかわらず遷移が起こった場合の「逸脱度」を数式で定量化し、直線的な時間オートマトンに対するイベントログの適合度検査アルゴリズムを実装した。さらに、分岐やループなどの複雑な構造を持つ時間オートマトンの適合性検査を行うため、モデルと実行列の最適アライメントを計算するアルゴリズムを与えた。
線形時相論理に基づく宣言的なプロセスモデルの検証のため、より効率的に検証することのできるサブ言語FLTLで元の論理式を近似する手法を考案した。

Strategy for Future Research Activity

時間オートマトンによるプロセスモデルにおける分岐条件発見について、より精度良く分類するための手法について検討していく。そのために適切な目的変数の選択や、SVMやニューラルネットワークなどによる非線形なモデルによる学習手法などについて試みる。
時間オートマトンによるプロセスモデルの適合性検査において、分岐やループを含んだ一般的な制御構造を持つプロセスモデルに対しても属性値を使用した適合性検査を行う手法を与え、実装する。現在のところ遷移条件(ガード)に対する逸脱度のみを定量化しているが、これを一般化し時間オートマトンのロケーション上の不変条件(インバリアント)に対しても同様の定量化を行う。
線形時相論理に基づく宣言的なプロセスモデル検証の効率化においては、現在のところDwyerの仕様記述パターンと呼ばれるパターンに対して近似式を与える手法を開発した。現時点ではDwyerのパターンの一部のみ近似式を考案したのみであるため、他のパターンにも適切な近似式を与える。

Causes of Carryover

2021年度購入予定だった高性能計算用サーバを以下の理由により購入していない。2021年度では、ニューラルネットワーク学習アルゴリズムなどのGPUによる高速化が可能な学習アルゴリズムを使用しておらず、決定木学習や回帰分析などの単純な学習アルゴリズムを試みていたため購入しなかった。
また、旅費についてもパンデミックのため予定していたヨーロッパの共同研究者との打ち合わせを見送ったため海外渡航費・滞在費を支出しなかった。
以上の理由により次年度使用額が発生した。次年度は計算用サーバの購入に使用する。

  • Research Products

    (2 results)

All 2021

All Journal Article (2 results) (of which Peer Reviewed: 2 results)

  • [Journal Article] 近似によるリアクティブシステムの仕様検証効率化2021

    • Author(s)
      伊藤宗平, 辻優磨
    • Journal Title

      ソフトウェア工学の基礎

      Volume: 28 Pages: 33-38

    • Peer Reviewed
  • [Journal Article] Efficient Realizability Checking by Modularization of LTL Specifications2021

    • Author(s)
      Sohei Ito, Kenji Osari, Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki
    • Journal Title

      The Computer Journal

      Volume: bxab116 Pages: -

    • DOI

      10.1093/comjnl/bxab116

    • Peer Reviewed

URL: 

Published: 2022-12-28  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi