Generating LTL Formulas for Process Mining by Example of Trace

Abstract

Process mining enables efficient and exhaustive analysis of business processes based on event data. Process mining tools such as linear temporal logic (LTL) Checker allow users to verify temporal properties of business processes for traces by providing a description based on LTL. However, it is difficult for many users to understand and use LTL-based mathematical notation. Therefore, there is a need for a method to describe temporal properties even for those who are not familiar with mathematical notation. Several methods have been proposed to automatically generate logical expressions to address these issues, but there are still problems related to the data format and the limited scope of the expressions that can be described. In this study, we proposed a method based on the satisfiability problem (SAT) for event logs in eXtensible Event Stream format used in process mining, and it is verified how well it can automatically generate temporal properties in business processes. We conducted experiments using two types of event logs to demonstrate the effectiveness of the proposed method.

Received: 27 November 2023 | Revised: 23 January 2024 | Accepted: 2 February 2024 

Conflicts of Interest

The authors declare that they have no conflicts of interest to this work. 

Data Availability Statement

The data that support the findings of this study are openly available in [GitHub] at https://github.com/ivan-gavran/samples2LTL, https://github.com/gaelbernard/sampling；in [Prom Tools] at http://promtools.org/doku.php and in [4TU.ResearchData]  at https://data.4tu.nl/. The data are also available from the corresponding author Hiroki Horita   (hiroki.horita.is@vc.ibaraki.ac.jp), upon reasonable request.