TIMING VERIFICATION BY SUCCESSIVE APPROXIMATION

We present an algorithm for verifying that a model M with timing const raints 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 ome ga-automaton as well, and the verification problem is posed as a langu age inclusion question L(M) subset of or equal to L(T). In constructin g the composition M of the constrained automata P-i, one needs to rule out the behaviors that are inconsistent with the delay bounds, and th is step is (provably) computationally expensive. We propose an iterati ve solution which involves generating successive approximations M(i) t o 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 ou r strategy through some examples. (C) 1995 Academic Press, Inc.