Lazy Reachability Checking for Timed Automata Using Interpolants

To solve the reachability problem for timed automata, model checkers usually apply forward search and zone abstraction. To ensure efficiency and termination, the computed zones are generalized using maximal constants obtained from guards either by static analysis or lazily for a given path. In this paper, we propose a lazy method based on zone abstraction that, instead of the constants in guards, considers the constraints themselves. The method is a combination of forward search, backward search and interpolation over zones: if the zone abstraction is too coarse, we propagate a zone representing bad states backwards using backward search, and use interpolation to extract a relevant zone to strengthen the current abstraction. We propose two refinement strategies in this framework, and evaluate our method on the usual benchmark models for timed automata. Our experiments show that the proposed method compares favorably to known methods based on efficient lazy non-convex abstractions.