Predicate Abstraction for Dense Real-Time Systems
M. Oliver Möller
November 2001 |

## Abstract:
We propose predicate abstraction as a means for verifying a
rich class of safety and liveness properties for dense real-time systems.
First, we define a restricted semantics of timed systems which is
observationally equivalent to the standard semantics in that it validates the
same set of -calculus formulas without a next-step operator. Then, we
recast the model checking problem
for a timed
automaton and a -calculus formula in terms of
predicate abstraction. Whenever a set of abstraction predicates forms a
so-called
basis, the resulting abstraction is strongly preserving in
the sense that validates iff the corresponding finite
abstraction validates this formula . Now, the abstracted system can
be checked using familiar -calculus model checking.
Like the region graph construction for timed automata, the predicate abstraction algorithm for timed automata usually is prohibitively expensive. In many cases it suffices to compute an approximation of a finite bisimulation by using only a subset of the basis of abstraction predicates. Starting with some coarse abstraction, we define a finite sequence of refined abstractions that converges to a strongly preserving abstraction. In each step, new abstraction predicates are selected nondeterministically from a finite basis. Counterexamples from failed -calculus model checking attempts can be used to heuristically choose a small set of new abstraction predicates for refining the abstraction
Available as |

Last modified: 2003-06-08 by webmaster.