Title: Predicate Abstraction for Dense Real-Time Systems
Authors: M. Oliver Möller, Harald Rueß, Maria Sorea
Number of pages: 27 + cover
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 ${\cal S} \models \varphi$ for a timed automaton ${\cal S}$ and a
$\mu$-calculus formula $\varphi$ in terms of predicate abstraction. Whenever
a set of abstraction predicates forms a so-called {\em basis}, the resulting
abstraction is strongly preserving in the sense that ${\cal S}$ validates
$\varphi$ iff the corresponding finite abstraction validates this formula
$\varphi$. 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.