Two Solutions for Checking LTLf Properties in Event Logs Tedi Ibershimi1,βˆ— , Diellsimeone Xhemalaj1 , Anti Alman2 , Ivan Donadello1 and Fabrizio Maria Maggi1 1 Free University of Bozen-Bolzano, Bolzano, Italy 2 University of Tartu, Tartu, Estonia Abstract Conformance checking is an important task in process mining that checks whether a case of a business process is compliant or not with a process model. Process models in conformance checking can be expressed by using the procedural paradigm (e.g., through BPMN models or Petri nets) or the declarative one (e.g., through Declare models). Declarative process modeling languages represent the process behavior using temporal logic constraints mainly expressed with Linear Temporal Logic on finite traces (LTL 𝑓 ). In this paper, we present two solutions for checking LTL 𝑓 temporal properties over the traces in an event log. The two solutions have been implemented in the RuM Java toolkit (equipped with a Graphical User Interface) and in the Declare4Py Python library. We also preliminary evaluate the time performance of both implementations showing that the execution times are reasonable for sufficiently complex checking tasks. Keywords Linear Temporal Logic, Conformance Checking, Log Filtering 1. Introduction Process mining [1] focuses on the analysis of business processes based on event logs that contain information about process executions. An important component in process mining is a process model. Traditional process models follow the procedural paradigm and are suitable for representing predictable and stable business processes through an explicit specification of the allowed behaviors. The procedural paradigm is well suited for business processes where all possible executions are relatively similar to each other. A shortcoming of the procedural paradigm is the difficulty of representing processes that have high variability among all possible executions as each variation needs to be explicitly accounted for, thus leading to high complexity in the process models [2]. In contrast, declarative process models can be more easily used to manage this type of processes since they are expressed through a set of constraints that state what the process behavior must not contradict, thus enabling the compact representation of multiple allowed process executions. ICPM Doctoral Consortium and Demo Track 2023, October 23-27, Rome, Italy βˆ— Corresponding author. Envelope-Open tibershimi@unibz.it (T. Ibershimi); dxhemalaj@unibz.it (D. Xhemalaj); anti.alman@ut.ee (A. Alman); ivan.donadello@unibz.it (I. Donadello); maggi@inf.unibz.it (F. M. Maggi) Orcid 0000-0002-5647-6249 (A. Alman); 0000-0002-0701-5729 (I. Donadello); 0000-0002-9089-6896 (F. M. Maggi) Β© 2023 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). CEUR Workshop Proceedings http://ceur-ws.org ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org) 1 CEUR ceur-ws.org Workshop ISSN 1613-0073 Proceedings Tedi Ibershimi et al. CEUR Workshop Proceedings 1–4 An important task in process mining is conformance checking, whose goal is to find discrep- ancies between a process model and the actual executed process as recorded in an event log. In this paper, we consider the verification of an LTL 𝑓 model 𝑀 (i.e., a set of LTL 𝑓 constraints) with respect to a log 𝐿 containing traces each being a sequence of events (activity executions). LTL 𝑓 checking verifies whether each trace in 𝐿 satisfies all constraints in 𝑀. The presented LTL 𝑓 checking tools provide a list of patterns that have been shown to be particularly useful in the literature [3, 4]. In particular, each pattern is represented as an LTL 𝑓 template, i.e., a formula with placeholders to be substituted by concrete activities to obtain a specific constraint. The family of simple LTL 𝑓 patterns (hereafter called SLTL𝑓 ) were first provided in [3], whereas the Declare patterns were first introduced in [4]. The checkers also support Branched Declare (hereafter called B-Declare) in which Declare templates are 𝑛 instantiated with disjunctions of activities π‘Ž = ⋁𝑖=1 π‘Žπ‘– . The LTL 𝑓 checkers have been implemented in the RuM Java toolkit [5] and the Declare4Py Python library [6]. These tools can be used for checking LTL 𝑓 formulas in the traces of an event log, but can also be used as advanced log filters to produce sub-logs that are compliant (or non-compliant) with some given LTL 𝑓 properties. We conducted empirical experiments and measured the execution times for performing the checking with RuM and Declare4Py. The findings of these experiments demonstrate that both solutions can execute complex tasks in reasonable time. 2. Tool description We present here a Java solution and a Python solution for checking LTL 𝑓 properties in event logs. The Java solution is provided in the form of a GUI-based functionality implemented in RuM. RuM is purposely designed to provide an easy, intuitive and user-friendly interface, making it suitable to be used by both process mining experts and non-experts [5]. The tool’s graphical interface plays an important role in supporting the use of SLTL𝑓 and Declare for conformance checking and log filtering, by providing options to build chains of filters, modify them, instantiate constraints from templates, import and export filter configurations, analyze the checking results and the corresponding statistics, export compliant and non-compliant traces in different sub-logs. The verification of the LTL 𝑓 formulas in RuM is based on the tree-based search presented in [3]. The graphical user interface represents the real novelty of the Java solution because it provides a user experience that is not provided by any existing tool for LTL 𝑓 checking. Another distinguishing feature of this solution resides in the possibility to check B-Declare constraints, which is not provided in other solutions. Finally, it is also important to note that all LTL 𝑓 properties that can be checked in RuM are treated as filters that can be combined with standard log filters (e.g., on trace durations, on attribute values, or on timestamps) to extract traces with specific characteristics from an event log. The Python solution is provided in the Declare4Py API. It is intended to be used by re- searchers willing to integrate this functionality in new tools, to perform large experimentations as well to perform Machine Learning related tasks. Declare4Py represents the first Python API able to perform conformance checking based on SLTL𝑓 and (B-)Declare constraints. This 2 Tedi Ibershimi et al. CEUR Workshop Proceedings 1–4 solution uses finite state automata for LTL 𝑓 checking built from the input formulas through a C++ engine1 . Furthermore, it also performs parallel executions that partition the event log into sub-logs that are assigned to different threads running in parallel. 3. Tool Maturity The execution times of the LTL 𝑓 checkers were measured through a series of experiments performed using event logs extracted from four datasets widely used in the literature. These logs, available in the well-known XES standard,2 have the characteristics shown in Table 1 and are identified with labels D1, D2, D3, and D4. Table 1 Statistics of the datasets used in the experiments. Event log # traces # events repairexample.xes (D1) 500 5725 sepsiscases.xes (D2) 1000 4307 teleclaim.xes (D3) 2500 32962 road-traffic-fine-management-process.xes (D4) 5000 36095 The experiments were conducted by applying the SLTL𝑓 and the B-Declare patterns to the event logs. In the case of B-Declare, the template parameters were replaced by the disjunction of two and five activities (randomly chosen in each log). The experiments were performed five times and the average time values were computed. All experiments were performed on a MacBook Pro machine equipped with an Apple M1 processor with 8 cores. The obtained results are illustrated in Table 2. The results show that, in RuM, the execution times grow linearly with the number of traces and the number of constraints in the reference model. This type of behavior was expected since larger logs and a higher number of constraints inherently require more processing time. In Declare4Py, we can observe mostly the same behavior apart from some cases in which the execution times remain constant. This is due to the fact that, in RuM, both the results of checking all constraints together and of checking each individual constraint are provided. Instead, Declare4Py only shows the results obtained by checking all constraints together. Consequently, in the Java solution, the system will always perform the check of all constraints on all traces. Instead, in Declare4Py, when a trace does not satisfy a constraint, that trace is not checked anymore. Therefore, if at some point all traces in the log do not satisfy the constraints checked so far, checking the other constraints do not increases the execution time since there are no traces to be evaluated. The execution times for Declare4Py are generally higher wrt. RuM. This is due to the fact that the Python solution first builds automata from the input constraints and afterwards performs the checking. Since the automata construction is exponential in the formula [7], this adds an overhead in Declare4Py. 1 https://github.com/whitemech/lydia 2 https://www.xes-standard.org/openxes/start 3 Tedi Ibershimi et al. CEUR Workshop Proceedings 1–4 Table 2 Execution times (in seconds). RuM Declare4Py # constraints D1 D2 D3 D4 D1 D2 D3 D4 SLTL𝑓 5 0.39 1.04 1.79 4.77 0.62 2.55 0.59 5.89 10 0.61 1.43 3.26 7.98 0.59 2.63 0.60 6.82 15 0.83 2.42 5.12 11.07 0.63 2.25 0.59 6.82 20 1.04 2.79 6.02 12.89 0.59 2.13 0.57 6.54 2B-Declare 5 0.78 0.93 1.81 3.26 2.25 4.68 9.10 5.20 10 0.82 1.87 3.32 6.39 2.29 7.43 9.12 5.31 15 1.04 2.76 4.58 9.69 2.18 7.68 9.13 5.25 20 1.23 3.22 5.96 12.25 2.32 7.11 9.34 5.17 5B-Declare 5 0.44 1.07 2.11 4.03 1.44 5.40 7.18 16.92 10 0.86 2.31 3.64 7.56 1.46 5.32 7.30 17.64 15 1.26 2.99 5.39 10.98 1.54 5.35 7.22 17.63 20 1.57 4.10 6.97 15.13 1.44 5.35 7.33 17.64 4. Screencasts and websites The source code of RuM is available at https://bitbucket.org/doorless1634/thesis/src/tedi-thesis/ and the source code of Declare4Py can be found at https://github.com/ivanDonadello/ Declare4Py/. In the latter repository, several Jupiter notebook-based tutorials are available explaining different LTL 𝑓 checking use cases. The video presentation of this paper can be accessed at https://www.youtube.com/watch?v=4wy3C1EfYJw. References [1] W. M. P. van der Aalst, Process Mining - Data Science in Action, Springer, 2016. [2] C. Di Ciccio, A. Marrella, A. Russo, Knowledge-intensive processes: Characteristics, re- quirements and analysis of contemporary approaches, J. Data Semant. 4 (2015) 29–57. [3] W. M. P. van der Aalst, H. T. de Beer, B. F. van Dongen, Process mining and verification of properties: An approach based on temporal logic, in: OTM Conferences (1), volume 3760 of Lecture Notes in Computer Science, Springer, 2005, pp. 130–147. [4] M. Pesic, H. Schonenberg, W. M. P. van der Aalst, DECLARE: Full support for loosely- structured processes, in: EDOC, IEEE Computer Society, 2007, pp. 287–300. [5] A. Alman, C. Di Ciccio, D. Haas, F. M. Maggi, A. Nolte, Rule mining with RuM, in: 2nd International Conference on Process Mining, ICPM 2020, 2020, pp. 121–128. [6] I. Donadello, F. Riva, F. M. Maggi, A. Shikhizada, Declare4Py: A python library for declara- tive process mining, in: BPM (PhD/Demos), volume 3216 of CEUR Workshop Proceedings, CEUR-WS.org, 2022, pp. 117–121. [7] G. De Giacomo, M. Y. Vardi, Linear temporal logic and linear dynamic logic on finite traces, in: IJCAI, IJCAI/AAAI, 2013, pp. 854–860. 4