## 1 Introduction  
Timed automata [1] have been one of the most popular formal models to specify and verify real-time systems. The main purpose of timed automata language inclusion checking [2] is to check whether the system model and the specification model (which represents the properties that the system needs to satisfy) have the relation of language inclusion. It can also be described as whether the system behaviors satisfy a certain property under the time constraints. There are already some studies that apply the theories and methods of timed automata to real-time systems, such as modeling and verification of cyber physical systems [3, 4], networked systems [5], the security of smart cities [6, 7], etc. However, most of them use verification based on reachability or temporal logics (such as TLTL, TCTL). There is no thorough method for timed automata language inclusion checking that can be applied to real-life systems. Formal modeling of real-time systems is an error-prone job. Usually the developers or testers are not familiar with formal modeling methods; therefore, they experience obstacles in describing the properties that the system should satisfy using timed automata. On the other hand, in order to verify the system correctness, the model checking tools must use the system models and property models as inputs. The property patterns can be used to close the gap between the users and the model checking tools [8]. Currently, there is a lack of study on property patterns which can be applied in language inclusion checking of timed automata. Current approaches often allow one to construct a system model which can be automatically transformed from other high-level languages to the language supported by a model checker. However, they do not illustrate how to specify the properties to be verified. On this basis, we propose a set of commonly used property patterns described by timed automata. It provides a guidance to users to model the properties for language inclusion checking. Due to the infinity of the time points, it is impossible to directly search the state space for timed automata. Therefore, verification of timed automata (for instance, reachability) can be solved by using the region graph [1]. However, verification based on region graphs is inefficient. Reference [9] proposed the zone-based method to efficiently check the safety and liveness properties. The verification tools for real-time systems often use zone graphs, such as PAT [10] and UPPAAL [11]. Our previous work [2] first gave a method based on zone abstraction to solve the language inclusion problem of timed automata. The method constructs a synchronous product (which can be seen as the generation of the state space) of two timed automata and then converts the language inclusion checking into a reachability problem on the synchronous product. During this process, the timed automata need to be determinized. In real-life systems, the system models are often complicated and contain a large amount of events, while the property models only need to pay attention to the sequences and time limits of a few events. If a property model must have the same set of events as the system model due to the definition of language inclusion, it will bring great difficulties to the property modeling. On the other hand, the algorithm will often not stop because the determinization of the timed automata is undecidable. Therefore, we improve the algorithm, so that it only needs to consider the concerned events in the property models in critical steps. This improvement makes the algorithm feasible in reality. The main contributions of this paper are as follows. Firstly, we summarize commonly used property patterns of timed automata, including: Absence, Universality, Existence, Response, Precedence, Chain and Occurrence times. Secondly, an improved language inclusion checking algorithm of timed automata is given, which does not need to consider the events not in the property models in critical steps.