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)\subseteq 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_j$ to $M$, with containment $L(M)\subseteq L(M_j)$ and monotone convergence $L(M_j) \rightarrow 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.
Information and Computation 118(1):142-157, 1995. Preliminary version appeared in Proceedings of the Fourth Conference on Computer-Aided Verification (CAV 1992), LNCS 663.