The main thesis of this dissertation is the research for possibilities of applying process mining techniques on event log data to synthesize formal process model from the behavioural patterns recorded in the log. In the theoretical part of the thesis, the theoretical foundations and formal definitions of the most important terms are given, additionally, the theoretical assumptions of the research are described. Furthermore, an overview of relevant related research in the area of process mining is provided. In this dissertation, a process mining method for process synthesis, analysis and repair is proposed and described in detail. The proposed method is composed of data preparation, process discovery, analysis and repair of the discovered process model. Process synthesis method is based on Inductive machine learning algorithms and techniques. Starting from raw event log data, through several automated model transformations, the proposed process synthesis method discovers the process model in labelled transition system notation. The approach described in this dissertation is based on inductive machine learning that is realized through a combinatorial approach of inductive programming (ILP) and model transformations. Model checking is used to analyse and evaluate results of the proposed method. Accordingly, evaluation of the method for process synthesis, analysis and repair was performed by simulations and verifications in the Spin model checker. As a case study actual event log data obtained from a hotel’s Property Management System (PMS) were used for process mining. Verification was performed on a representative process model under six different specifications defined. The verification confirmed that the resulting process model complies to the given specifications. The results obtained from discovered process models evaluation confirmed the efficiency of the proposed approach, furthermore, process models discovered by applying the process synthesis method are in line with reality. Additionally, in this thesis a conformance checking technique is proposed. By applying the proposed technique, the process model is executed so that for each sequence of events it is checked whether the given automaton (process model) contains a word from the input data (sequence of events). Accordingly, the conformance of the model and log is measured from the classification point of view in the context of the process mining quality measures. The vast majority of the research in the process mining field is related to algorithms for process discovery, and still, there are a small number of techniques and tools for process repair. A process repair method based on counterexamples is proposed in this dissertation. The process repair was performed on a case study in the Smart Parking Internet of Things (IoT) system, where the event data obtained from the parking sensor log were used.