The system verification of timed automata based on simulation graph

In order to improve the property verification´s efficiency and accuracy of timed automata, it is helpful and necessary to analysis and research the timed behavior of the graphs in model checking. In this paper, based-on the simulation graph, we check the language emptiness of a timed automaton to verify whether the relevant real time system satisfies the desired property. The specific work has three steps: the first is to describe the desired property as a timed Büchi automaton, and synchronize it with its timed system model to get their product automaton which is a timed Büchi automaton; the next is to use some successor operator to get the product automata´s simulation graph; the last is to check the emptiness of lasso paths on this simulation graph to verify the property satisfaction of the timed system.