TIMING VERIFICATION BY SUCCESSIVE APPROXIMATION

We present an algorithm for verifying that a model M with timing constraints satisfies a given temporal property T. The model M is given as a parallel composition of omega-automata P-i, where each automaton P-i is constrained by bounds on delays. The property T is given as an omega-automaton as well, and the verification problem is posed as a language inclusion question L(M) subset of or equal to L(T). In constructing the composition M of the constrained automata P-i, one needs to rule out the behaviors that are inconsistent with the delay bounds, and this step is (provably) computationally expensive. We propose an iterative solution which involves generating successive approximations M(i) to M, with containment L(M) subset of or equal to L(M(j)) and monotone convergence L(M(j)) --> L(M) within a bounded number of steps. As the succession progresses, the approximations M(j) become more complex. At any step of the iteration one may get a proof or a counter-example to the original language inclusion question. The described algorithm is implemented into the verifier Cospan. We illustrate the benefits of our strategy through some examples. (C) 1995 Academic Press, Inc.