First of all, the paper presents the basic definition and the symbols of timed automaton. Second realizes the construction of region automata through equivalence class, but the space complexity is the exponential blowup in the number of state in the construction algorithm of region automata. To get a better average space complexity, improves on it And then analyzes the time constraint of region automata, gets a new method to construct region automaton. Ameliorates both the time complexity and the space complexity Third, introduces the new development of timed automaton that is event-recording automata, event-predicting and event-clock automata. And then researches the property and the relation of language it given, proposes some interesting conclusion. At last gives an instance of verification. |