## Timing Verification by Successive Approximation

*Rajeev Alur, Alon Itai, Robert P. Kurshan, and
Mihalis Yannakakis*
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.