Predicate Abstraction for Dense Real-Time Systems

(M. Oliver Möller, Maria Sora, and Harald Rueß)

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 mu-calculus
formulas without a next-step operator.  Then, we recast the model checking
problem S |= phi for a timed automaton S and a mu-calculus formula phi 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 phi iff the corresponding finite abstraction
validates this formula phi.  Now, the abstracted system can be checked using
familiar mu-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 mu-calculus model checking attempts can be used
to heuristically choose a small set of new abstraction predicates for refining
the abstraction.