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 PostScript(gzip'ed), PostScript, PDF, and BibTeX.