Yes, Matilda! Abstraction can Replace Deduction, even for Computational Models which are BAD (Buchi Automata with Data)

Amir Pnueli

Weizmann Institute of Science. Joint work (in progress) with Y. Kesten and M. Vardi


In the KIT workshop on Hybrid Systems (Grenoble Oct., 1998), we introduced the method of Verification by Finitary Abstraction (VFA). By this method, in order to verify that an infinite-state system S satisfies the temporal property f, one abstracts S into a finite-state system S^A and abstracts f into a finite-state (propositional temporal formula f^A, verifies S^A |= f^A by model checking, and then infers that the original property f holds over the original system S. In the talk, we presented a recipe for ensuring that the method is sound (safe) for all LTL properties f. We also conjectured with high probability that the method is also complete, namely, whenever S |= f, there exists an abstraction mapping \alpha such that S^{\a} |= f^{\a}. We formulated this conjecture by asking "Can abstraction replace deduction?"

Since then, we have confirmed this conjecture and have shown that the VFA method is indeed complete. A paper with these results have been submitted to LICS99.

Moshe Vardi raised the question whether it is possible to reformulate the VFA method and obtain similar completeness results within the automata-theoretic framework. The topic of this talk is a positive answer to his question.

To start with, we had to find out what is the automata-theoretic version of a deductive system (assumed to be applicable to infinite-state systems), which we have to replace. This led to the computational model BAD (Buchi Automata with Data), which is a Buchi (finite-state) automaton, equipped with additional state variables that can range over infinite domains, and transition relations (appearing as edge labels) referring and modifying these state variables. Then we proposed a single deductive rule which is sound and (relatively) complete for establishing the emptiness of a (potentially infinite-state) BAD automaton, a problem to which all verification problems can be reduced.

Having constructed the deductive method we wished to replace, we immediately proceed to formulate the appropriate notion of abstraction which is a particular type of a homomorphism, and show that it is sound for Verification by Finitary Abstraction. Next, we utilize the availability of the single complete deductive rule in order to establish the completeness of the VFA method for the BAD models of computation.