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.

Online Copy

	© 2004 Springer-Verlag.
	Paper is available as Postscript (310 KB) or gzip'ed Postscript (115 KB)

BibTeX Entry

@InProceedings{Sorea:FTRTFT04, author = "Maria Sorea", title = "{Lazy Approximation for Dense Real-Time Systems}", year = 2004, booktitle = "Proc. of the Joint Conference Formal Modelling and Analysis of Timed Systems (FORMATS), Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT)", editor = "", pages = "", series = "Lecture Notes in Computer Science", volume = "", publisher = "Springer-Verlag", month = sep }