Abstract: Timed automaton is a useful modeling tool for real-time systems. To check whether a system can reach a specific state, the teachability analysis algorithms explore the state space of timed automata by enumeration of symbolic states. Since clocks are used

Key words: Real-time system, Timed automata, State space explosion, Reachability analysis