Lazy Approximation for Dense Real-Time Systems

We propose an effective and complete method for verifying safety and properties of timed systems, which is based on predicate abstraction for g finite abstractions of timed automata and TCTL formulas, finite-state CTL model checking, and successive refinement of finite-state abstractions. Startsome coarse abstraction of the given timed automaton and the TCTL we define a finite sequence of refined abstractions that converges to the raph 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 inlly refining the current abstraction. Without sacrificing completeness, this algorithm usually does not require computing the complete region graph to odel-checking problems. Abstraction refinement terminates quickly, as a multitude of spurious...

• Type: Conference
• Year: 2004
• Where: FORMATS
• Authors: Maria Sorea
• Keywords: Abstraction, Abstraction Predicates, FORMATS 2004, Symbolic Counterexamples