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., throughDeclare 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 checkinLgTL temporal properties over the traces in an event log. The two solutions have been implemented in thReuM Java toolkit (equipped with a Graphical User Interface) and in thDeeclare4Py Python library. We also preliminary evaluate the time performance of both implementations showing that the execution times are reasonable for suficiently complex checking tasks.
CEUR ceur-ws.org
Process mining [
An important task in process mining is conformance checking, whose goal is to find discrepancies between a process model and the actual executed process as recorded einveannt log. In this paper, we consider the verification of anLTL model (i.e., a set ofLTL constraints) with respect to a lo g containing traces each being a sequence of events (activity executionLsT).L checking verifies whether each trace i n satisfies all constraints in .
The presentedLTL checking tools provide a list of patterns that have been shown to be
particularly useful in the literatu3r,e4][. In particular, each pattern is represented asLaTLn
template, i.e., a formula with placeholders to be substituted by concrete activities to obtain
a specific constraint. The family of simpleLTL patterns (hereafter calledSLTL ) were first
provided in [
instantiated with disjunctions of activitie s=
The LTL checkers have been implemented in thReuM Java toolkit 5[] and the Declare4Py Python library 6[]. These tools can be used for checkinLgTL 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 givenLTL properties. We conducted empirical experiments and measured the execution times for performing the checking wiRthuM and Declare4Py. The ifndings of these experiments demonstrate that both solutions can execute complex tasks in reasonable time.
We present here a Java solution and a Python solution for checkLinTgL 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-expert5s].[ The tool’s graphical interface plays an important role in supporting the usSeLTofL 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 diferent sub-logs. The verification of the LTL formulas inRuM is based on the tree-based search presented in3][. 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 forLTL 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 alLlTL properties that can be checked iRnuM 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 theDeclare4Py API. It is intended to be used by researchers willing to integrate this functionality in new tools, to perform large experimentations as well to perform Machine Learning related tasDkesc.lare4Py represents the first Python API able to perform conformance checking based oSLnTL and (B-)Declare constraints. This solution uses finite state automata forLTL 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 diferent threads running in parallel.
The execution times of theLTL 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 standa2rhda,ve the characteristics shown in Tabl1eand are identified with labels D1, D2, D3, and D4.
The experiments were conducted by applying thSeLTL and the B-Declare patterns to the event logs. In the case ofB-Declare, the template parameters were replaced by the disjunction of two and five activities (randomly chosen in each log). The experiments were performed ifve 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 Tab2l.e
The results show that, inRuM, 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, iRnuM, 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, iDneclare4Py, 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 forDeclare4Py are generally higher wrRtu.M. 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 formu7]l,ath[is adds an overhead inDeclare4Py. 1https://github.com/whitemech/lydia 2https://www.xes-standard.org/openxes/start
RuM # constraints D1 D2 D3 D4
The source code ofRuM is available ahtttps://bitbucket.org/doorless1634/thesis/src/tedi-thesis/ and the source code ofDeclare4Py can be found at https://github.com/ivanDonadello/ Declare4Py./ In the latter repository, several Jupiter notebook-based tutorials are available explaining diferent LTL checking use cases. The video presentation of this paper can be accessed athttps://www.youtube.com/watch?v=4wy3C1EfYJw.