## 1 Introduction  
With the increasing demand for new functionalities in software, developers often release multiple updates to meet the relevant needs. However, software is frequently released without standard documentation, which leads to the software specification becoming outdated [1]. Moreover, software specification mining requires the expertise of professional developers, since it is a task that requires highly specialized skills to analyze the log documents. Nevertheless, specification mining is necessary as it enables us to identify abnormal system behavior by analyzing system logs. In specification mining, the linear-time temporal logic (LTL) formula and finite-state automaton (FSA) model are generally used to represent software specifications. Many methods have been proposed to extract system behavior specifications, which allows developers to make informed decisions about the behavior of the system [2; 3; 4]. [PERSON] et al. proposed a static technique to mine software specifications directly from the system source code without executing the system [5], but it is not applicable to large-scale systems. [PERSON] et al. proposed an approach to efficiently mine specifications expressed as temporal logic formulas from the execution traces of a system [6]. However, the quality of the mined specifications is not perfect. For instance, if the methods in the input execution traces frequently occur in a particular order or the amount of input traces is too small, the FSAs inferred by k-tails [7] and many other tools are often not generalized and overfitted to the input execution traces. To solve this problem, [PERSON] et al. proposeddeep specification mining (DSM) [8; 9], which combines an long short-term memory (LSTM) neural network [10] with the K-means algorithm [11] to mine finite-state automators (FSAs). LSTM is used in DSM because LSTM is better at learning long-term dependencies and is scalable for long sequences. DSM leverages deep learning techniques to effectively extract the specifications of large-scale systems. It also utilizes clustering algorithms to generate FSAs that more concisely capture the specifications of the systems. However, DSM still faces challenges such as the problem of incorrect merging among states in FSAs generated by clustering feature values and random parameter selection in the clustering process. To address the above-mentioned issues, we improve DSM by generating FSAs with the ordering points to identify the clustering structure (OPTICS) clustering algorithm [12], and refining the FSAs based on model checking to improve the quality of the FSAs. The proposed specification mining approach can briefly be described as follows:  
1. DSM is employed to generate the feature values of states in the traces of the program;
2. The OPTICS clustering algorithm first generates a reachability plot based on the feature values. Then, the range of the clustering radius is determined according to the reachability plot, and several suitable radii are selected within this range to cluster the feature values to obtain the FSAs;
3. A model selection algorithm is used to select the FSA with the highest F-measure from the generated FSAs. Specifically, the F-measure is defined in Section 3.2;
4. Texada [6] is employed to generate LTL properties specifying the desired behaviors of the system. Then, model checking of the FSA is performed to verify whether the selected FSA satisfies these properties. If not, we refine the FSA by adding and deleting the corresponding states and transitions in it according to the type of the property which the FSA violates, so that the traces that violate the property are removed from the FSA. The three main contributions of this paper are as follows:  
1. We propose a specification mining approach based on the OPTICS clustering algorithm and model checking. Specifically, during the generation of FSAs, we employ the OPTICS clustering algorithm to improve the clustering effect and solve the parameter setting problem so that the parameters can be intuitively set.