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 (LTLf). In this paper, we present two solutions for checking LTLf 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.