A Full Symbolic Reachability Analysis Algorithm of Timed Automata Based on BDD

Reach ability analysis algorithm is the foundation of model checking. State space explosion is accelerated due to the time constraints of timed automata, therefore, the complexity of reach ability analysis algorithm has increased. The existing timed automata reach ability analysis methods can be divided into two types: the first type is the state space traversal algorithm based on equivalent time region map or difference bounded matrices (DBM) using a semi-symbol time constraints structure, the other is a state space traversal method based on BDD structure using full-symbol time constraints. Unfortunately, both types of methods split the symbol correlation of state transition expression and time constraints expression, therefore they are difficult to be applied into a large case study. A full-symbol reach ability analysis method based on BDD structure is proposed in this article, state transition space of timed automata and time constraints are expressed under the same BDD structure to avoid the loss of correlation and to analyze the reach ability of states and satisfiablity of time constraints. The presented method in this paper helps to achieve full-symbol reach ability analysis of timed automata, which would lay a solid foundation for full-symbolic model checking of time system. Finally, a specific case is analyzed by this algorithm.