Efficient Verification Of Timed Systems Using Backward Reachability Analysis
TR-2002-11, Author: Jesper Møller
Jesper Møller February 2002
Abstract
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.
Technical report TR-2002-11 in IT University Technical Report Series, February 2002.
Available as
PDF.