Timing verification by successive approximation

Abstract

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 composition of ω-antomata Pi, where ench automaton Pi is constrained by the bounds on delays. The property T is given as an ω-automaton as well, and the verification problem is posed as a language inclusion question L(M) ⊆ L(T). In constructing the composition M of the constrained automata Pi, 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 Mj to M, with containment L(M) ⊆ L(Mi) and monotone convergence L(Mi) → L(M) within a bounded number of steps. As the succession progresses, the Mj become more complex, but at auy step of the iteration one may get a proof or a counter-example to the original language inclusion question. We first construct M0, the composition of the Pi ignoring the delay constraints, and try to prove the language inclusion L(M0) ⊆ L(T) If this succeeds, then L(M) ⊆ L(M0) ⊆ L(T) If this fails, we can find x ϵ L(M0)\L(T) of the form x = σlσω We give an algorithm to check for consistency of x with respect to the delay bounds of M: the time complexity of this check is linear in the length of, σ'σ and cubic in the number of automata. If x is consistent with all the delay constraints of M, then x provides a counter-example to L(M) ⊆ L(T) Otherwise, we identify an "optimal" set of delay constraints D inconsistent with x. We generate an automaton PD which accepts only those behaviors that are consistent with the delay constraints in the set D. Then we add PD as a restriction to M0, forming M1, and iterate the algorithm. In the worst case, the number of iterations needed is exponential in the number of delay constraints. Experience suggests that in typical cases, however, only a few delay constraints are material to the verification of any specific property T. Thus, resolution of the question L(M) ⊆ L(T) may be possible after only a few iterations of the algorithm, resulting in feasible language inclusion tests. This algorithm is being implemented into the verifier COSPAN at AT&T Bell Laboratories.