@article{Möller_Ruess_Sorea_2001, title={Predicate Abstraction for Dense Real-Time Systems}, volume={8}, url={https://tidsskrift.dk/brics/article/view/21704}, DOI={10.7146/brics.v8i44.21704}, abstractNote={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.}, number={44}, journal={BRICS Report Series}, author={Möller, M. Oliver and Ruess, Harald and Sorea, Maria}, year={2001}, month={Nov.} }