Lazy Approximation for Dense Real-Time Systems

9 years 9 months ago
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...
Maria Sorea
Added 01 Jul 2010
Updated 01 Jul 2010
Type Conference
Year 2004
Authors Maria Sorea
Comments (0)