Lazy Approximation for Dense Real-Time Systems

We propose an effective and complete method for verifying safety and liveness properties of timed systems, which is based on predicate abstraction for computing finite abstractions of timed automata and TCTL formulas, finite-state CTL model checking, and successive refinement of finite-state abstractions. Starting with some coarse abstraction of the given timed automaton and the TCTL formula we define a finite sequence of refined abstractions that converges to the region graph of the real-time system. In each step, new abstraction predicates are selected nondeterministically from a finite, predetermined basis of abstraction predicates. Symbolic counterexamples from failed model-checking attempts are used to heuristically choose a small set of new abstraction predicates for incrementally refining the current abstraction. Without sacrificing completeness, this algorithm usually does not require computing the complete region graph to decide model-checking problems. Abstraction refinement terminates quickly, as a multitude of spurious counterexamples is eliminated in every refinement step through the use of symbolic counterexamples for TCTL.