A full symbolic compositional reachability analysis of timed automata based on BDD

In General, a complex real-time system is made up of multiple concurrent members of timed automata. To verify the safety and liveness of real-time system, model checking always use reachability analysis to accomplish. The existing reachability analysis algorithm can be divided into two types: semi- symbolic based on difference bounded matrices (DBM) or equivalent time region map and the full-symbolic method based on BDD structure. Because the both method split the symbol correlation of expression of state transition space and clock constraints, they are hard to be applied to a large case study. A heuristic full-symbol compositional reachability analysis method based on BDD structure is proposed in this paper, which can unified to express state transition space and clock constraints. This analysis method chooses new heuristic algorithm for on-the-fly timed automata combination which can verify reachability and satisfaction of compositional state simultaneously, and can reduce the time complexity and space complexity. Finally, a specific case is analyzed by this algorithm.