Predicate Abstraction for Dense Real-Time Systems1 1This research was supported by the National Science Foundation under grants CCR-00-82560 and CCR-00-86096 and by NASA Langley Research Center under contract B09060051 and Cooperative Agreement NCC-1-399 with Honeywell Minneapolis. Most of this research has been conducted while the first author was visiting SRI International, July/August 2001.

TLDR

Predicate abstraction for timed automata is typically prohibitively expensive, similar to the region graph construction for timed automata. The paper proposes predicate abstraction to verify a broad range of safety and liveness properties in dense real‑time systems. The authors define a restricted semantics equivalent to the standard one, recast timed automaton model checking as predicate abstraction, and iteratively refine a finite bisimulation using counterexamples to obtain a strongly preserving abstraction that can be checked with μ‑calculus model checking. They show that if the abstraction predicates form a basis, the abstraction is strongly preserving, so the timed automaton satisfies a μ‑calculus formula exactly when its finite abstraction does.

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 μ-calculus formulas without a next-step operator. Then, we recast the model checking problem S ⊨ ϕ for a timed automaton S and a μ-calculus formula ϕ in terms of predicate abstraction. Whenever a set of abstraction predicates forms a so-called basis, the resulting abstraction is strongly preserving in the sense that S validates ϕ iff the corresponding finite abstraction validates this formula ϕ. Now, the abstracted system can be checked using familiar μ-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 μ-calculus model checking attempts can be used to heuristically choose a small set of new abstraction predicates for refining the abstraction.