TY - JOUR
AU - MÃ¶ller, M. Oliver
AU - Ruess, Harald
AU - Sorea, Maria
PY - 2001/11/04
Y2 - 2024/04/25
TI - Predicate Abstraction for Dense Real-Time Systems
JF - BRICS Report Series
JA - BRICS
VL - 8
IS - 44
SE - Articles
DO - 10.7146/brics.v8i44.21704
UR - https://tidsskrift.dk/brics/article/view/21704
SP -
AB - 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 <em>basis</em>, 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.<br /> <br />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.
ER -