Predicate Abstraction for Dense Real-Time Systems

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 S |= # for a timed automaton S 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 S validates # i# 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