Efficient Verification Of Timed Systems Using Backward Reachability Analysis

In this paper we demonstrate that symbolic verification of real-time systems based on backward reachability analysis is generally more efficient than verification based on forward reachability analysis. Symbolic verification of real-time systems consists of computing the least fixpoint of a functional that given a set of states phi returns the states that are reachable from phi (forward reachability), or that can reach phi (backward reachability). The key observation is that the symbolic operations in the fixpoint computation can be simplified substantially when performing backward reachability analysis. In particular, we show that resetting clocks and making discrete state changes can be performed as substitutions instead of existential quantifications over reals and Booleans, respectively. Experimentally we find that backward reachability analysis is more efficient than forward reachability analysis.