Abstract: The reachability analysis algorithm explores the state space of a timed automaton by enumeration of symbolic states. Each symbolic state consists of a location and a time zone which are conjunctions of automatic formulae in the form x-y≤（〈）n. Sometimes th

Key words: Timed automata, Model checking, Symbolic state,Time zone