=Paper=
{{Paper
|id=Vol-3648/paper_5986
|storemode=property
|title=RuM and Declare4Py: Two Solutions for Checking LTLf Properties in Event Logs
|pdfUrl=https://ceur-ws.org/Vol-3648/paper_5986.pdf
|volume=Vol-3648
|authors=Tedi Ibershimi,Diellsimeone Xhemalaj,Anti Alman,Ivan Donadello,Fabrizio Maria Maggi
|dblpUrl=https://dblp.org/rec/conf/icpm/IbershimiXADM23
}}
==RuM and Declare4Py: Two Solutions for Checking LTLf Properties in Event Logs==
https://ceur-ws.org/Vol-3648/paper_5986.pdf
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