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
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]()
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 Available as PostScript, PDF. |