TY - JOUR AU - Möller, M. Oliver AU - Ruess, Harald AU - Sorea, Maria PY - 2001/11/04 Y2 - 2024/03/28 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 -