@TechReport{BRICS-RS-01-44,
author = "M.~Oliver M{\"o}ller and Harald Rue{\ss} and Maria Sorea",
title = {Predicate Abstraction for Dense Real-Time Systems},
institution = "{BRICS}",
year = 2001,
type = "Research Series",
number = "RS-01-44",
address = "Department of Computer Science, University of Aarhus",
OPTkey = "",
month = nov,
OPTnote = "",
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.",
OPTlinkhtmlabs ="",
OPTlinkdvi = "",
OPTlinkps = "",
OPTlinkpdf = "",
OPTannote = ""
}