## 1 Introduction  
Modern information systems diligently maintain a record of operational events in the form of an event log. Historically, these system logs served primarily as a reference point to retrospectively trace the sequence of events and identify any potential errors. However, with the rapid progression of technology in today's era, the focus has broadened significantly. The challenge now lies not just in detecting errors but also in deriving valuable insights from these event logs. In the modern era, information systems have become an integral part of various sectors, including business, healthcare, and education, among others. These systems generate a vast number of data, providing a rich source of information for understanding and improving processes. It is necessary to monitor, analyse, and improve a process to keep the business environment running smoothly. However, the complexity and number of these data present significant challenges to extracting meaningful insights. Process mining [1] has emerged as a promising approach to address these challenges. As an intersection between data mining and business process management, process mining is about discovering, monitoring, analysing, and improving real-world business processes through knowledge extraction from event logs provided by information systems [2]. Real-world examples of event logs include loan applications in banking systems [3], an application of a patient's medical billing report in hospital [4], logs used to detect customer behaviour based on logged clicks [5], and there are more examples. Real-world processes are often influenced by a number of unpredictable factors, from machine breakdowns to human decision variability. Process-mining techniques might fall short in capturing these peculiarities, leading to models that are overly simplified or not representative of the actual system behaviour. Formal verification has emerged as an effective strategy to verify process correctness. Formal verification is a method used in computer science to verify and/or analyse the properties of finite-state systems, and it is a powerful technique for verifying concurrent and distributed systems. The work presented by [6] introduces BProVe, a verification framework dedicated to _business process model and notation (BPMN)_. This framework was created to address the lack of formal semantics in BPMN, which creates obstacles for the automated verification of relevant properties. The work in [7] proposes an approach, termed model mining, which facilitates the creation of abstract, concise, and functionally structured models from event logs. In [8], a methodology for conducting temporal analysis on mobile service-based business processes is introduced with a concentrated emphasis on the specification and validation of temporal constraints. Model checking is an often-utilised technique of formal verification that involves the creation of a model of the system, specifying desirable properties in a logical language and then using algorithms to determine whether the model satisfies these properties [9]. According to [10], the model-checking approach model processes as transition systems and express properties as formulas in temporal logic. These properties signify the requirements that a particular process needs to fulfill to be deemed correct. Linear temporal logic (LTL) is one of the languages that allows users to define properties for verification. The objective of model checking is to ascertain whether a process model demonstrates particular desirable behaviour. In some cases where the process model fails to exhibit the necessary behaviour, model-checking techniques provide a counterexample. This assists in identifying the areas of the model that require correction, ensuring that the final model is robust and fit for its intended purpose. The application of model-checking techniques in process mining is a relatively new and promising research area [11]. The integration of these two fields can provide a more robust and comprehensive analysis of operational processes.