A Study of Optimization Techniques about Reachability in Timed Automata
时间自动机可达性分析中的状态空间约减技术综述

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